The clay files quantify over finite lists

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

The corpus's Clay-named theorems quantify over finite lists of this size — nine points for the Riemann functional equation, seven for BSD. Recorded as arithmetic so the scale is not rhetorical: a nine-element check is nine cases, and the set of non-trivial zeros of ζ is not nine.

Proposition

[(-4 : Int), -2, -1, 0, 1, 2, 3, 4, 6].length = 9 ∧ [(-2 : Int), -1, 0, 1, 2, 3, 4].length = 7

Proof

By decide in decidability.lean. The kernel reduces the proposition and reports no axiom dependency.

Sources and identifiers

• Lean source · src/pair/formal/proofs/decidability.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778
• Deposit record · decidability--the_clay_files_quantify_over_finite_lists

Proved in the same file

• Verified at every point below the bound
• And false at the bound
• Finite verification does not entail the universal
• A bigger bound proves no more
• What a finite check does establish

All machine-checked theorems