And false at the bound

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked 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.

AND FALSE. The very next case refutes it.

Proposition

holdsBelowAThousand 1000 = false

Proof

By decide in decidability.lean. Checked by the Lean kernel: it depends on no axiom.

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--and_false_at_the_bound

Proved in the same file

• Verified at every point below the bound
• Finite verification does not entail the universal
• A bigger bound proves no more
• What a finite check does establish
• The clay files quantify over finite lists

All machine-checked theorems