Joining the odd and even extensions

This file formalizes the middle part of the proof of Lemma 2 in the paper “A 4AP-free permutation of the positive integers”: after extending the two parity words, put the new odd entries before the new even entries.

The suffixes O and E in the statements below are normalized: their entries are rescaled by x ↦ 2x+1 and x ↦ 2x when appended to the old word P. The guard on the odd target set is exactly the paper's requirement that all normalized odd entries below h have been included.

theorem FourAP.completion_append_before {R : ℕ → ℕ → Prop} {A B : List ℕ} {y x : ℕ} (hy : y ∈ A) (hx : x ∉ A) : Completion R (A ++ B) y x

Putting further entries after a finite word preserves the fact that each entry of that word precedes each entry outside it. This is the comparison between the new odd block and the new even block in Lemma 2.

theorem FourAP.safe_splice {P E O : List ℕ} (hP : Safe bits P) (hE : Safe bits (parityWord 0 P ++ E)) (hO : Safe bits (parityWord 1 P ++ O)) (h : ℕ) (hbound : ∀ e ∈ E, 2 * e ≤ h) (hcover : ∀ k < h, k ∈ parityWord 1 P ++ O) : Safe bits (P ++ List.map (fun (x : ℕ) => 2 * x + 1) O ++ List.map (fun (x : ℕ) => 2 * x + 0) E)

Lemma 2, construction of Q = P O E and its safety.

The two recursive calls have already provided safe extensions of P₀ and P₁. The even bound h determines how many odd entries must be included. First we identify the parity restrictions of the new completion, then prove the odd-before-even comparison displayed as equation (2) in the paper. The final arithmetic-progression contradiction is safe_of_parity_and_guard.