Axiom-policy gate
Every shipped declaration is checked, on every build, to depend only on the three standard axioms propext, Classical.choice, Quot.sound. A build fails if any other axiom enters the closure.
The discipline
The GI verification discipline
Geometry Intelligence is not a discovery claim. It is the verification, packaging, provenance and evidence discipline that turns a Lean build into citable, reproducible evidence.
Six gates, applied to every package
ECR battery
Each result is returned as an accepted DECLARATION_CHECK job with zero unused-hypothesis rows, classified (e.g. LIBRARY_SUPPORT). The battery records statement class and whether a result is closing.
Mutation tests
Wrong or weakened statements, and an inserted sorry, must be rejected by the build. This guards against a gate that silently accepts a broken proof.
Non-vacuity
Witnesses are proved in Lean so that the statements are not vacuously true (e.g. zero_solR3, zero_solTorus).
Kernel receipts & two kernels
Key results are checked on Lean's default kernel and on nanoda, an independent re-implementation. Receipts record the axioms and the exit status.
Reproducible rebuilds
Online and offline rebuild profiles, plus a code-aware token scan, let a third party reproduce the build and the PASS lines. Tested platform: Linux x86_64.
Then anchored for the record
Each release is a separate, citable artifact: a DOI (Zenodo), a Wikidata entity, and ORCID attribution to the owner. Receipts and release manifests are hash-pinned. This is the honest, demonstrable capability — stronger than an unsupported discovery claim.
What the discipline does NOT establish
- It does not establish mathematical truth of an open premise; a PASS line authenticates file bytes and the axiom closure, not the truth of a hypothesis.
- It is not independent review. Every check was run by the package builder on a single Linux x86_64 node.
- It does not confirm that a Lean statement transcribes an official problem’s prose.