Finite safe words

This file formalizes the parity restrictions of 𝒞(P) used in the Extension Lemma, and Lemma 1 (reverse binary order is safe). The two arithmetic-progression equations used below include both increasing and decreasing progressions.

def FourAP.parityWord (p : ℕ) (P : List ℕ) : List ℕ

The words P₀ and P₁ in the Extension Lemma: retain one parity and rescale it by 2x+p ↦ x.

Equations

• FourAP.parityWord p P = List.filterMap (fun (n : ℕ) => if n % 2 = p then some (n / 2) else none) P

@[simp]

theorem FourAP.parityWord_append (p : ℕ) (P Q : List ℕ) : parityWord p (P ++ Q) = parityWord p P ++ parityWord p Q

Parity restriction respects the order of concatenated words, as used when the proof forms the extension Q = P O E.

@[simp]

theorem FourAP.parityWord_cons (p n : ℕ) (P : List ℕ) : parityWord p (n :: P) = if n % 2 = p then n / 2 :: parityWord p P else parityWord p P

The recursive description of the parity-restricted word in Lemma 2.

theorem FourAP.mem_parityWord_iff {p x : ℕ} (hp : p < 2) (P : List ℕ) : x ∈ parityWord p P ↔ 2 * x + p ∈ P

A number occurs in Pₚ exactly when its original, unscaled value occurs in P. This is the membership assertion implicit in the parity split.

theorem FourAP.nodup_parityWord {p : ℕ} (hp : p < 2) {P : List ℕ} (hP : P.Nodup) : (parityWord p P).Nodup

Rescaling one parity preserves distinctness; hence the parity words appearing in the Extension Lemma are again words without repetitions.

theorem FourAP.nodup_of_parityWord {Q : List ℕ} (h0 : (parityWord 0 Q).Nodup) (h1 : (parityWord 1 Q).Nodup) : Q.Nodup

If both parity words have distinct entries, the original word does too. This is the distinctness argument for the new word Q = P O E in Lemma 2.

theorem FourAP.completion_parity {p : ℕ} (hp : p < 2) (P : List ℕ) (a b : ℕ) : Completion bits P (2 * a + p) (2 * b + p) ↔ Completion bits (parityWord p P) a b

Restricting 𝒞(P) to parity p and rescaling gives exactly 𝒞(Pₚ). This formalizes the self-similarity argument in the first inductive paragraph of the Extension Lemma.

theorem FourAP.safe_parity {p : ℕ} (hp : p < 2) {P : List ℕ} (hP : Safe bits P) : Safe bits (parityWord p P)

The parity words of a safe word are safe (Extension Lemma, paragraph beginning “Both P₀ and P₁ are safe”).

@[simp]

theorem FourAP.parityWord_map_same {p : ℕ} (hp : p < 2) (P : List ℕ) : parityWord p (List.map (fun (x : ℕ) => 2 * x + p) P) = P

Normalizing a word already rescaled into parity p recovers the original word, as in the construction of the suffixes E and O.

@[simp]

theorem FourAP.parityWord_map_other {p q : ℕ} (hq : q < 2) (hpq : p ≠ q) (P : List ℕ) : parityWord p (List.map (fun (x : ℕ) => 2 * x + q) P) = []

Projecting a word of the other parity yields the empty word. This justifies separating the new odd and even suffixes of Q = P O E.

theorem FourAP.reverse_bits_of_completion {P : List ℕ} (hs : List.Pairwise (fun (a b : ℕ) => bits b a) P) {a b : ℕ} (hab : Completion bits P a b) (hb : b ∈ P) : bits b a

Inside a word listed in reverse ◁ order, an earlier entry is later in ◁. This is the first comparison used in the two-prefix-term case of Lemma 1.

theorem FourAP.safe_of_reverse_pairwise {P : List ℕ} (hn : P.Nodup) (hs : List.Pairwise (fun (a b : ℕ) => bits b a) P) : Safe bits P

Lemma 1 of the paper. Every finite word of distinct integers listed in reverse ◁ order is safe. The proof separates the cases of at least three, exactly two, and at most one progression term in the finite prefix.

def FourAP.reverseBitsLE (a b : ℕ) : Prop

The non-strict reverse of ◁, used solely for sorting the finite set in Lemma 1 and in the base case of the Extension Lemma.

Equations

• FourAP.reverseBitsLE a b = (a = b ∨ FourAP.bits b a)

@[instance_reducible]

instance FourAP.reverseBitsLEDecidable : DecidableRel reverseBitsLE

The finite sorting relation in Lemma 1 has a computable comparison.

Equations

• FourAP.reverseBitsLEDecidable x✝¹ x✝ = { decide := decide (x✝¹ = x✝) || decide (FourAP.bits x✝ x✝¹), reflects_decide := ⋯ }

instance FourAP.reverseBitsLETrans : IsTrans ℕ reverseBitsLE

Transitivity permits sorting in the reverse order used in Lemma 1.

instance FourAP.reverseBitsLEAntisymm : Std.Antisymm reverseBitsLE

Antisymmetry makes the reverse listing of a finite set unique.

instance FourAP.reverseBitsLETotal : Std.Total reverseBitsLE

Any two integers can be compared when forming the reverse listing.

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

List a finite set in reverse ◁ order, exactly as prescribed in Lemma 1. This definition is computable, using mathlib's finite-set merge sort.

Equations

• FourAP.reverseWord T = T.sort FourAP.reverseBitsLE

@[simp]

theorem FourAP.mem_reverseWord {T : Finset ℕ} {x : ℕ} : x ∈ reverseWord T ↔ x ∈ T

The reverse listing contains each and only each prescribed entry.

theorem FourAP.reverseWord_nodup (T : Finset ℕ) : (reverseWord T).Nodup

The reverse listing contains no repeated entry, as required of a word.

theorem FourAP.reverseWord_pairwise (T : Finset ℕ) : List.Pairwise (fun (a b : ℕ) => bits b a) (reverseWord T)

The reverse listing has the strict reverse order required in Lemma 1.

theorem FourAP.safe_reverseWord (T : Finset ℕ) : Safe bits (reverseWord T)

Lemma 1 specialized to the canonical reverse listing of a finite set.

theorem FourAP.reverseWord_zero_first {T : Finset ℕ} (h0 : 0 ∈ T) : reverseWord T = 0 :: reverseWord (T.erase 0)

If zero belongs to a finite set, its reverse binary listing begins with zero. This is the sorting observation in the base case of Lemma 2.

theorem FourAP.reverseWord_union_prefix {P : List ℕ} (hP : P.Nodup) (hzero : ∀ x ∈ P, x = 0) (T : Finset ℕ) : P <+: reverseWord (P.toFinset ∪ T)

Canonical form of the base-case extension in Lemma 2. Sorting P ∪ T in reverse binary order preserves the old prefix whenever all its entries are zero. This also connects the executable construction to the proof.