A computable permutation from safe stages

This file gives the effective version of the last proof and the computability remark in the paper “A 4AP-free permutation of the positive integers”. Given computable increasing safe words P n containing all integers below n, both directions of the resulting permutation are computable:

• To find the value at position i, read position i in P (i + 1).
• To find the position of a value t, find t in P (t + 1).

These bounds are sufficient, but not necessarily efficient. The theorem permutationOfSafeStages_eq_getElem justifies the more efficient prescription in the paper's remark: stop at any stage long enough to contain the position. Neither direction of the equivalence uses a choice of preimage.

def FourAP.SequenceAPFree (f : ℕ → ℕ) : Prop

The conclusion of the paper for a sequence indexed by ℕ: no four entries at increasing positions form a nonconstant arithmetic progression. Because IsAP4 uses equations rather than natural subtraction, decreasing arithmetic progressions are excluded as well.

Equations

• FourAP.SequenceAPFree f = ∀ ⦃i j k l : ℕ⦄, i < j → j < k → k < l → ¬FourAP.IsAP4 (f i) (f j) (f k) (f l)

theorem FourAP.safeStages_prefix (P : ℕ → List ℕ) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) {m n : ℕ} (hmn : m ≤ n) : P m <+: P n

Once one stage is a prefix of its successor, it is a prefix of every later stage. This is the “No entry, once placed, is ever moved” assertion in the final proof of the paper.

theorem FourAP.safeStages_length (P : ℕ → List ℕ) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) (n : ℕ) : n ≤ (P n).length

Exhaustive targets give a concrete length bound: a word containing 0, …, n-1 has at least n entries. Thus every requested position can be reached after a bounded number of stages in the computability remark.

theorem FourAP.safeStages_value_eq_getElem (P : ℕ → List ℕ) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) (n i : ℕ) (hi : i < (P n).length) : (P (i + 1)).getD i 0 = (P n)[i]

Reading a position at the bounded stage i + 1 gives the same value as reading it at any stage where it is already present. This is the finite-stage stabilization argument underlying the computational procedure in the remark.

theorem FourAP.safeStages_idxOf_eq (P : ℕ → List ℕ) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) (n t : ℕ) (ht : t ∈ P n) : List.idxOf t (P (t + 1)) = List.idxOf t (P n)

A value has the same position in every stage in which it occurs. This is the inverse form of the paper's assertion that placed entries never move, and makes the inverse permutation computable without choosing preimages.

def FourAP.permutationOfSafeStages (R : ℕ → ℕ → Prop) (P : ℕ → List ℕ) (hsafe : ∀ (n : ℕ), Safe R (P n)) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) : ℕ ≃ ℕ

The actual computable equivalence constructed by the final proof of the paper from computable safe stages. Its forward map reads a bounded stage, and its inverse searches a bounded finite word; the proofs below verify that these explicitly given maps are mutually inverse.

Equations

• FourAP.permutationOfSafeStages R P hsafe hstep hcover = { toFun := fun (i : ℕ) => (P (i + 1)).getD i 0, invFun := fun (t : ℕ) => List.idxOf t (P (t + 1)), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FourAP.permutationOfSafeStages_apply (R : ℕ → ℕ → Prop) (P : ℕ → List ℕ) (hsafe : ∀ (n : ℕ), Safe R (P n)) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) (i : ℕ) : (permutationOfSafeStages R P hsafe hstep hcover) i = (P (i + 1)).getD i 0

The bounded evaluation rule for the forward permutation in the paper's computability remark. Coverage proves that the default value is never used.

@[simp]

theorem FourAP.permutationOfSafeStages_symm_apply (R : ℕ → ℕ → Prop) (P : ℕ → List ℕ) (hsafe : ∀ (n : ℕ), Safe R (P n)) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) (t : ℕ) : (permutationOfSafeStages R P hsafe hstep hcover).symm t = List.idxOf t (P (t + 1))

The inverse permutation is a finite search in the stage that is guaranteed to contain the value. This strengthens the computability remark by supplying an explicit inverse as well as an explicit forward map.

theorem FourAP.permutationOfSafeStages_eq_getElem (R : ℕ → ℕ → Prop) (P : ℕ → List ℕ) (hsafe : ∀ (n : ℕ), Safe R (P n)) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) (n i : ℕ) (hi : i < (P n).length) : (permutationOfSafeStages R P hsafe hstep hcover) i = (P n)[i]

The precise stopping rule from the paper's remark: the value at position i can be read from any finite stage whose length is greater than i. Later stages have exactly the same entry at that position.

theorem FourAP.permutationOfSafeStages_apFree (R : ℕ → ℕ → Prop) (P : ℕ → List ℕ) (hsafe : ∀ (n : ℕ), Safe R (P n)) (hstep : ∀ (n : ℕ), P n <+: P (n + 1)) (hcover : ∀ (n t : ℕ), t < n → t ∈ P n) : SequenceAPFree ⇑(permutationOfSafeStages R P hsafe hstep hcover)

The finite-stage contradiction in the last proof of the paper, applied to the explicitly computable permutation. All four entries of a hypothetical progression lie in a single safe stage, where their positions give the same three comparisons in the completion.