Finite verification does not entail the universal

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.

So a finite verification does not entail the unbounded claim: here is a property verified at a thousand consecutive points whose universal statement is FALSE. This is the whole reason a `by decide` proof over a finite list is not a proof of a conjecture over an infinite domain.

Proposition

((List.range 1000).all holdsBelowAThousand = true) ∧ (holdsBelowAThousand 1000 = false)

Proof

By by 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--finite_verification_does_not_entail_the_universal

Proved in the same file

• Verified at every point below the bound
• And false at the bound
• A bigger bound proves no more
• What a finite check does establish
• The clay files quantify over finite lists

All machine-checked theorems