The permutation of the positive integers

This file formalizes the final proof and computability remark in the paper “A 4AP-free permutation of the positive integers”. Starting from the empty word, stage n + 1 extends stage n with target {n}. These safe words give an explicit bijection of ℕ, proved 4AP-free by permutationOfSafeStages_apFree. Adding one to each value gives the positive sequence; shifting the positions as well gives the positive permutation in the paper's indexing convention.

The numerical prefixes from the remark are checked separately in its upstream numerical examples module, using the stabilization results proved here.

theorem FourAP.empty_safe : Safe bits []

The initial stage P⁽⁰⁾ = [] in the final proof is safe, since its completion is the 3AP-free binary order.

def FourAP.algorithmStage : ℕ → List ℕ

The singleton-target stages P⁽ⁿ⁾ from the proof of the theorem and the final remark: start empty, then force 0, 1, 2, ... in succession.

Equations

• FourAP.algorithmStage 0 = []
• FourAP.algorithmStage n.succ = FourAP.extendAlgorithm (FourAP.algorithmStage n) {n}

theorem FourAP.algorithmStage_safe (n : ℕ) : Safe bits (algorithmStage n)

Every stage of the executable construction is safe, as asserted in the proof of the main theorem.

theorem FourAP.algorithmStage_prefix (n : ℕ) : algorithmStage n <+: algorithmStage (n + 1)

The executable stages retain every entry already placed (main proof).

theorem FourAP.algorithmStage_covers (n t : ℕ) : t < n → t ∈ algorithmStage n

By stage n, all integers below n have appeared. This supplies the exhaustion statement in the main proof and the termination guarantee in the final remark's procedure for computing any given entry.

def FourAP.explicitPermutation : ℕ ≃ ℕ

The particular computable permutation of ℕ₀ specified by the singleton targets in the final remark. Both this map and its inverse are executable.

Equations

• FourAP.explicitPermutation = FourAP.permutationOfSafeStages FourAP.bits FourAP.algorithmStage FourAP.algorithmStage_safe FourAP.algorithmStage_prefix FourAP.algorithmStage_covers

theorem FourAP.explicitPermutation_apFree : SequenceAPFree ⇑explicitPermutation

The permutation computed in the final remark is 4AP-free. This connects the executable algorithm to the theorem, rather than merely checking examples.

theorem FourAP.explicitPermutation_eq_getElem (n i : ℕ) (hi : i < (algorithmStage n).length) : explicitPermutation i = (algorithmStage n)[i]

The stopping criterion in the final remark: any stage long enough to contain a position already gives the final value at that position.

theorem FourAP.explicitPermutation_prefix (n m : ℕ) (hm : m ≤ (algorithmStage n).length) : List.map (⇑explicitPermutation) (List.range m) = List.take m (algorithmStage n)

Reading a finite initial segment from a sufficiently long stage agrees with the actual infinite permutation. This is the list form of the stopping criterion and justifies the displayed numerical example in the remark.

def FourAP.explicitPositiveSequence : ℕ ≃ ℕ+

Add one to the executable permutation, as in the last sentence of the proof and the second displayed prefix in the final remark. Positions remain zero-based here so the sequence can be read directly using Lean lists.

Equations

• FourAP.explicitPositiveSequence = FourAP.explicitPermutation.trans Equiv.pnatEquivNat.symm

@[simp]

theorem FourAP.explicitPositiveSequence_apply (i : ℕ) : ↑(explicitPositiveSequence i) = explicitPermutation i + 1

The positive sequence is the nonnegative permutation shifted by one, exactly as stated in the paper.

theorem FourAP.explicitPositiveSequence_apFree (i j k l : ℕ) : i < j → j < k → k < l → ∀ (a r : ℤ), r ≠ 0 → ¬(↑↑(explicitPositiveSequence i) = a ∧ ↑↑(explicitPositiveSequence j) = a + r ∧ ↑↑(explicitPositiveSequence k) = a + 2 * r ∧ ↑↑(explicitPositiveSequence l) = a + 3 * r)

The explicit positive sequence avoids every nonconstant four-term AP, including negative integer differences. This is the theorem's conclusion for the particular computable construction in the final remark.

def FourAP.explicitPositivePermutation : ℕ+ ≃ ℕ+

The actual computable permutation of positive integers, with both values and positions indexed by ℕ+, matching the paper's a₁ a₂ … convention.

Equations

• FourAP.explicitPositivePermutation = Equiv.pnatEquivNat.trans FourAP.explicitPositiveSequence

theorem FourAP.explicitPositivePermutation_apFree (i j k l : ℕ+) : i < j → j < k → k < l → ∀ (a r : ℤ), r ≠ 0 → ¬(↑↑(explicitPositivePermutation i) = a ∧ ↑↑(explicitPositivePermutation j) = a + r ∧ ↑↑(explicitPositivePermutation k) = a + 2 * r ∧ ↑↑(explicitPositivePermutation l) = a + 3 * r)

The paper's main theorem for the explicitly constructed positive permutation, now also with positive-integer positions.