Implemented
Scope firewall
Keeps three endpoints distinct: a selected scalar system, a selected-group Yang–Mills system, and the theorem for every compact simple group. No silent promotion is permitted.
Neuralgic-point verification
Lean checks the dangerous interfaces.
The aim is not to decorate the manuscript with machine-checked code. It is to formalise the places where a plausible argument can silently change scope, lose an assumption, or promote a local estimate into a theorem it does not imply.
Unconditional proof claimed in Volumes I–III. Independent expert review ongoing. Lean formalisation of selected proof interfaces is in progress.
The limit of formalisation
Lean verifies implications. It does not create analytic truth.
Lean checks selected downstream implications under explicitly encoded hypotheses. It does not replace the analytic arguments in Volumes I–III, and it does not determine independent expert or community acceptance. This is an additional validation track, not a conditional label for the core claim.
Verification packages
Implemented
Spectral compiler
Checks the abstract implication from high-band and core-margin certificates to a positive Hamiltonian spectral gap, including the quantitative gap constant.
Interface formalisation
Continuum extraction
Formalises cofinal row passage, reflected-Gram positivity, dense symmetry extension, and marked nonescape through the exact analytic boundary supplied by the paper.
Interface formalisation
OS reconstruction
Builds the reflected pre-Hilbert structure and checks the route from semigroup decay through spectral measure to the reconstructed Wightman gap.
Planned checker
Exact certificate checker
A small trusted Lean checker for selected rational and finite-computation certificates generated outside Lean.
What this increases confidence in
- The theorem’s quantifiers remain intact
- Conditional dependencies cannot be silently erased
- Spectral and reconstruction implications compose correctly
- Exact finite certificates can be checked by a small trusted kernel
What it does not establish alone
- The truth of an external analytic premise
- The correctness of an informal source theorem
- The manuscript’s full analytic argument by formalisation alone
- Expert or community acceptance of the result