The contradiction at the heart of Lemma 2

The last half of the extension lemma needs only three facts about the new completion: the old prefix remains fixed, each parity restriction is 4AP-free, and the odd-before-even comparison in equation (2) holds. We isolate this argument so that the subsequent recursive construction can be read separately from its safety proof.

theorem FourAP.safe_of_parity_and_guard {P Q : List ℕ} (hP : Safe bits P) (hp : P <+: Q) (hq : Q.Nodup) (hparity : ∀ ⦃a b c d : ℕ⦄, IsAP4 a b c d → a % 2 = b % 2 → Completion bits Q a b → Completion bits Q b c → Completion bits Q c d → False) (hguard : ∀ ⦃x y : ℕ⦄, ¬x ∈ P → ¬y ∈ P → x % 2 = 0 → y % 2 = 1 → y ≤ 2 * x → Completion bits Q y x) : Safe bits Q

Lemma 2, from “Suppose, for a contradiction, that a 4AP ...” to the end. hparity excludes progressions with even common difference. hguard is exactly the displayed odd-before-even property labelled eq:odd-even in the paper.