Partial proof for MainTheorem

[aleph-prover-dev]

⚠️ Your proof request could only be partially completed
Some theorems may only have informal proofs available.
Some hard-to-prove facts may have been replaced with axioms.

---

Proven lemmas: 53/56

The main goal is the Skolem–Mahler–Lech-style statement that for any linear recurrence u : ℕ → K over a characteristic-0 field, the zero set {n : ℕ | u n = 0} is a finite union of arithmetic progressions together with a finite exceptional set. Mathematically, the proof has been split into two big parts: first show that the zero set is ultimately periodic, and then package any ultimately periodic subset of ℕ as a finite set ∪ finitely many arithmetic progressions.

That second, combinatorial packaging part is now in place: the lemmas showing eventual periodicity along residue classes, conversion of eventual periodicity into a finite union of arithmetic progressions, and the final top-level packaging theorem are all proved. The recurrence-theoretic reduction is also largely complete: the proof handles the order-0 case, reduces the general case to the positive-order case, passes to the finitely generated field generated by the recurrence data, and then transports the problem into an algebraically closed p-adic setting.

Overall progress is strong: 53 of 60 nodes are proved (with 4 of the 60 being just definitions), so only 3 genuine theorem statements remain open. The remaining work is concentrated in the deepest p-adic analytic part of the argument. One open theorem is an analyticity statement for continuous additive characters on the p-adic unit ball; another is a quantitative lower bound for a nonzero “top block” exponential-polynomial along a fixed arithmetic progression; and the last open theorem is now mostly a glue lemma showing that this dominant top block eventually cannot be cancelled by lower-norm terms.

The interesting strategy is that the proof does not try to attack the zero set directly. Instead, it rewrites recurrence sequences in terms of generalized eigenspaces and exponential-polynomial expressions over PadicAlgCl p, then studies each residue class separately using p-adic analytic interpolation and isolated-zero principles. The main challenge left is quantitative: not just proving that the top block is nonzero infinitely often, but proving an eventual lower bound strong enough to beat the geometrically smaller lower-norm terms. Once that lower-bound theorem is established, the remaining domination step should be short, and the full theorem should follow.

---

Note

High Risk
Large, highly-coupled proof addition that introduces complex p-adic/analytic infrastructure and still contains sorry placeholders, so it may not compile or may weaken soundness assumptions depending on build settings.

Overview
Builds out a substantial Lean development toward the Skolem–Mahler–Lech statement for linear recurrences, adding lemmas that (1) reduce recurrence orbits to exponential-polynomial forms via generalized eigenspace decompositions over PadicAlgCl p, and (2) use p-adic analytic interpolation/isolated-zeros style arguments to get eventual zero/nonzero behavior on each residue class.

Adds the combinatorial packaging from ultimate periodicity to a finite set plus finitely many arithmetic progressions, and updates MainTheorem to finish by proving the zero set is ultimately periodic and then applying this packaging. Three deep analytic/quantitative steps remain as sorry (additive-character analyticity and a lower-bound/dominance argument for same-norm top blocks).

^{Written by Cursor Bugbot for commit b45861b. This will update automatically on new commits. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

[cursor]

Unused duplicate theorem for different coefficient field

Low Severity

linearRecurrence_tupleSucc_iterate (specialized to ℂ_[p]) is never referenced anywhere in the codebase. It proves the identical mathematical statement as linearRecurrence_tupleSucc_iterate_padicAlgCl (specialized to PadicAlgCl p), and only the latter is actually used (in linearRecurrence_exists_residue_eventually_zero_or_nonzero_padicAlgCl). The ℂ_[p] version appears to be a leftover from an earlier approach.

Additional Locations (1)

• FormalQualBench/SkolemMahlerLechTheorem/Main.lean#L315-L341