YangMillsGapCert
plain-language theorem explainer
Finite inventory of certificate kinds used to audit a Yang-Mills mass-gap claim in the Recognition calculus. Three tags mark a finite plaquette ledger, an excitation-gap witness, and a zero-mode obstruction witness. Anyone wiring a ProblemAudit or display bridge for the gap cites this enum. It is a bare inductive definition with decidable equality and no proof obligations.
Claim. There is a finite set of certificate labels for the Yang-Mills mass-gap audit, consisting of three kinds: a finite plaquette ledger, an excitation-gap witness, and a zero-mode obstruction witness. Equality of labels is decidable.
background
The module HardProblemCertificateAudits packages Millennium-style hard problems as finite certificate inventories plus audit maps. Each inventory is an inductive enum of witness kinds; audits then check legitimacy, pathology, and completion against those kinds.
For Yang-Mills the physical target is a spectral gap above the vacuum for the pure gauge Hamiltonian. In the Recognition setting the register is finite-dimensional (the eight-tick $C^N$ register), so continuum Stone theory is not required; matrix exponentials and discrete plaquette data suffice. Upstream material on Hamiltonian emergence, self-reference certificates, Regge hinge-aware zero modes, and $J$-cost Ehrhart/posting-layer structure supplies the geometric and cost language those witnesses allude to, without being re-proved here.
Sibling inventories (prime critical line, Navier-Stokes energy, Hodge algebraic) follow the same pattern: a small decidable enum feeding identity and analytic ProblemAudit wrappers.
proof idea
No proof. The declaration is an inductive type with three nullary constructors and derived DecidableEq and Repr instances. There is no tactic block, no sorry, and no reduction to upstream lemmas; the constructors themselves are the certificate vocabulary.
why it matters
This enum is the certificate type parameter for the Yang-Mills audit stack in the same module: the identity audit, the certified-display audit, the analytic display record, the analytic completion map, and the full analytic ProblemAudit. Downstream definitions thread it as both the certificate and (for the identity audit) the display type, so every legitimacy or pathology judgment is indexed by one of the three tags.
In the broader Recognition framework the mass-gap claim sits with other hard-problem certificates that must eventually connect to forced structure (finite eight-tick register, $J$-cost geometry, discrete Hamiltonian generators). The inventory does not close that connection; it only names the witness slots the audit machinery can accept. Parent consumers are the yangMills* audit and display definitions listed above.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.