The language of the paper

This file fixes the conventions used to formalize the paper “A 4AP-free permutation of the positive integers”. The construction takes place in ℕ, which in Lean includes zero. The final theorem shifts the values by one.

An arithmetic progression is expressed using the two equations a + c = 2 * b and b + d = 2 * c. For natural-number entries these equations, together with a ≠ b, are equivalent to having a nonzero integer common difference. Thus decreasing progressions are included throughout.

def FourAP.IsAP4 (a b c d : ℕ) : Prop

Four consecutive terms of a nonconstant arithmetic progression, as in the paper's main theorem. The equations avoid truncated subtraction in ℕ.

Equations

• FourAP.IsAP4 a b c d = (a ≠ b ∧ a + c = 2 * b ∧ b + d = 2 * c)

theorem FourAP.isAP4_iff_integer_progression {a b c d : ℕ} : IsAP4 a b c d ↔ ∃ (r : ℤ), r ≠ 0 ∧ ↑b = ↑a + r ∧ ↑c = ↑a + 2 * r ∧ ↑d = ↑a + 3 * r

The equation-based representation used in this formalization is equivalent to the paper's progression a, a+r, a+2r, a+3r, with a nonzero integer common difference. In particular, decreasing progressions are included.

def FourAP.APFree (R : ℕ → ℕ → Prop) : Prop

The paper's definition of a 4AP-free order, applied to a strict relation. The relation need not be bundled as a linear order for this predicate.

Equations

• FourAP.APFree R = ∀ ⦃a b c d : ℕ⦄, FourAP.IsAP4 a b c d → R a b → R b c → R c d → False

def FourAP.Completion (R : ℕ → ℕ → Prop) (P : List ℕ) (a b : ℕ) : Prop

The completion 𝒞(P) from the paragraph preceding Lemma 1, with an arbitrary background relation R. List.idxOf is the length of the list for a missing entry, so the first disjunct orders the prefix and puts it before the tail.

Equations

• FourAP.Completion R P a b = (List.idxOf a P < List.idxOf b P ∨ ¬a ∈ P ∧ ¬b ∈ P ∧ R a b)

def FourAP.Safe (R : ℕ → ℕ → Prop) (P : List ℕ) : Prop

A safe word in the sense of the paper: a word without repetitions whose completion is 4AP-free. The background order is made explicit here.

Equations

• FourAP.Safe R P = (P.Nodup ∧ FourAP.APFree (FourAP.Completion R P))