The theorem of the paper

The declarations here assemble the preceding modules into the unconditional existence theorem of the paper “A 4AP-free permutation of the positive integers”. For the closest match to the displayed theorem in the paper, see exists_fourAPFree_positive_permutation, which uses positive integers both as positions and as values, and an arbitrary nonzero integer difference. Each existential statement below uses the explicit, verified construction.

theorem FourAP.exists_fourAPFree_permutation : ∃ (f : ℕ ≃ ℕ), SequenceAPFree ⇑f

The main theorem before the final shift: a permutation of ℕ₀ with no four-term arithmetic progression in increasing positions.

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

The main theorem after adding one to every value, retaining zero-based positions for compatibility with Lean lists and sequences.

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

The theorem of the paper. There exists a permutation of the positive integers containing no subsequence a, a+r, a+2r, a+3r with r ≠ 0 in ℤ.

A Lean equivalence supplies both injectivity and surjectivity: no value is repeated or omitted. The indices here are positive integers, matching the paper's convention a₁ a₂ …. Negative common differences are included.