Tagewerk XII

Problem 16 positive side proved — arithmetic sequences are self-ordered (kernel-verified)

Cahen–Fontana–Frisch–Glaz Problem 16 (Chabert) asks for the natural self-ordered integer sequences. A sequence a is self-ordered when its factorial D_n = ∏_{k<n}(aₙ − aₖ) divides P(m,n) = ∏_{k<n}(aₘ − aₖ) for all m and n. This is an infinite condition, so our earlier census could only refute it or give bounded evidence for the positive cases. Here we cross that line and PROVE the positive side, in the Lean 4.31 kernel, for an entire class. First, the identity sequence aₙ = n is self-ordered: its factorial is D_n = ∏_{k<n}(n − k) = n!, and n! divides the product of any n consecutive integers ∏_{k<n}(m − k) — the standard factorial-divides-descending-factorial fact, with the case m < n handled by a zero factor in the product. Second, and generally, EVERY arithmetic sequence aₙ = α + βn is self-ordered: each factor (α+βx) − (α+βk) equals β(x − k), so both D_n and P(m,n) factor as βⁿ times the identity factorial; the shared βⁿ cancels and the claim reduces to the identity case. Corollaries instantiate the census's self-ordered arithmetic sequences — n, 2n, and 3 + 5n — as theorems, upgrading them from 'self-ordered up to N = 30 (evidence)' to proofs. And the harder geometric case is now closed too: every geometric sequence aₙ = qⁿ (q an integer) is self-ordered. Factoring qⁿ − qᵏ = qᵏ(q^{n−k} − 1) reduces the divisibility to the fact that the Gaussian binomial coefficient is an integer; since Mathlib has no Gaussian binomials, they are built from scratch (a ℤ-valued q-Pascal recurrence, with the product identity proved by induction). All seven theorems depend only on the standard axioms (propext, Classical.choice, Quot.sound); the proofs are complete, with no compiler-trusted shortcuts. Together with the census refutations (n³, n⁴, factorial, Fibonacci, primes), Problem 16 now has a certified negative side and two proved positive classes — arithmetic and geometric. LLMs propose nothing that counts here; the Lean kernel decides every step. (The mechanical route — a hosted Goedel-Prover — timed out on the geometric goal, which was then closed by hand with the q-factorial machinery, recorded honestly.)