Lemma 2: the executable extension of a safe word

This file formalizes the Extension Lemma in the paper “A 4AP-free permutation of the positive integers”. The recursive function extendAlgorithm follows the choices in the paper's proof: extend the even part first, then extend the odd part to cover the required initial interval, and append the odd suffix before the even suffix. In the base case, list the union of the old word and the target set in reverse binary order.

The recursion terminates because each parity projection has a strictly smaller largest entry. extendAlgorithm_spec proves its safety, prefix preservation, and target coverage in one induction. The paper's existential Lemma 2 is the immediate corollary safe_extend.

def FourAP.parityTarget (p : ℕ) (T : Finset ℕ) : Finset ℕ

The normalized parity-p elements of the target set in Lemma 2. For p = 0 this divides the even targets by two; for p = 1 it sends an odd target t to (t-1)/2, equivalently t/2 in natural-number division.

Equations

• FourAP.parityTarget p T = Finset.image (fun (t : ℕ) => t / 2) ({t ∈ T | t % 2 = p})

theorem FourAP.div_mem_parityTarget {p t : ℕ} {T : Finset ℕ} (ht : t ∈ T) (hp : t % 2 = p) : t / 2 ∈ parityTarget p T

Every target of the selected parity contributes its normalized value, as required by the recursive calls in Lemma 2.

theorem FourAP.parityWord_max_lt {P : List ℕ} {p : ℕ} (hp : p < 2) (hm : 0 < P.toFinset.sup id) : (parityWord p P).toFinset.sup id < P.toFinset.sup id

The induction measure in Lemma 2 decreases after either parity projection, provided the old word has a positive largest entry.

def FourAP.reverseWordExecutable (T : Finset ℕ) : List ℕ

An insertion-sort implementation of the reverse listing in Lemma 1. It is extensionally identical to reverseWord; using structural insertion sort also allows the displayed numerical example to reduce in Lean's kernel.

Equations

• FourAP.reverseWordExecutable T = Quot.liftOn T.val (List.insertionSort FourAP.reverseBitsLE) FourAP.reverseWordExecutable._proof_1

@[simp]

theorem FourAP.reverseWordExecutable_eq (T : Finset ℕ) : reverseWordExecutable T = reverseWord T

The executable reverse listing is the same canonical word as in Lemma 1; the choice of sorting algorithm does not change the paper's construction.

@[irreducible]

def FourAP.extendAlgorithm (P : List ℕ) (T : Finset ℕ) : List ℕ

An executable form of Lemma 2 (Extension), using exactly the choices in its proof. E and O are normalized suffixes, so the final maps restore their original parity. In the base case the union of prefix and target is listed without repetition in reverse ◁ order, as in Lemma 1.

Equations

• One or more equations did not get rendered due to their size.

def FourAP.ExtensionResult (P : List ℕ) (T : Finset ℕ) (Q : List ℕ) : Prop

The specification asserted in Lemma 2: a safe extension, preserving the old prefix and containing every prescribed target. This predicate packages the three conclusions without hiding the actual output word.

Equations

• FourAP.ExtensionResult P T Q = (FourAP.Safe FourAP.bits Q ∧ P <+: Q ∧ ∀ t ∈ T, t ∈ Q)

theorem FourAP.prefix_append_drop {P Q : List ℕ} (h : P <+: Q) : P ++ List.drop P.length Q = Q

Splitting off the newly appended suffix recovers the entire extension. This is the list identity used when the paper introduces E and O.

theorem FourAP.extendAlgorithm_spec (P : List ℕ) (T : Finset ℕ) (hP : Safe bits P) : ExtensionResult P T (extendAlgorithm P T)

Correctness of the executable Extension Lemma. This follows the paper's induction literally; safe_splice contains its odd-before-even argument.

theorem FourAP.safe_extend (P : List ℕ) (hP : Safe bits P) (T : Finset ℕ) : ∃ (Q : List ℕ), Safe bits Q ∧ P <+: Q ∧ ∀ t ∈ T, t ∈ Q

Lemma 2 (Extension) of the paper. Every safe finite word is an initial segment of a safe finite word containing any prescribed finite target set. The witness is the executable word constructed and verified above.