YangMillsAnalyticDisplay
plain-language theorem explainer
Bundles a Yang–Mills mass-gap certificate with two discrete resolution parameters and a display-payload tag into one analytic display record. Downstream audit and completion maps treat this as the display type for the Yang–Mills bridge. Pure structure definition: four fields, no proof obligations.
Claim. An analytic display for the Yang–Mills mass-gap bridge is a 4-tuple $(c, r, \ell, \tau)$ where $c$ is a finite gap certificate (plaquette ledger, excitation-gap witness, or zero-mode obstruction), $r,\ell\in\mathbb{N}$ are plaquette resolution and excitation level, and $\tau$ is a display tag (connection, excitation, or zero-mode).
background
The module HardProblemCertificateAudits packages finite certificate inventories and display records for several hard-problem bridges (primes, Navier–Stokes, Yang–Mills, Hodge). For Yang–Mills the certificate type is a three-constructor inductive: finite plaquette ledger, excitation-gap witness, or zero-mode obstruction witness. The display payload is a parallel three-tag inductive: connection, excitation, or zero-mode.
This structure is the domain-specific analytic display that pairs one such certificate with two natural-number resolution parameters and one payload tag. It sits in the same pattern as the Hilbert-display completion layer, where $F_{RS}$ amplitudes are rendered as finite Hilbert vectors; here the rendering is certificate-level rather than amplitude-level. Upstream finite-dimensional Hamiltonian emergence (matrix exponentials on the 8-tick register) supplies the operator setting in which a mass gap is meaningful without infinite-dimensional Stone theory.
proof idea
No proof body. The declaration is a plain structure with four fields and a derived Repr instance. Field types are the in-module inductives YangMillsGapCert and YangMillsDisplayPayload plus ℕ twice. Downstream, yangMillsAnalyticCompletion builds a default display by packing a certificate with zeros and the connection tag.
why it matters
Gives the display type parameter of the Yang–Mills analytic ProblemAudit and its Completion. The completion map sends each gap certificate to a default display; legitimacy and pathology predicates are currently trivial (True). Parent consumers are yangMillsAnalyticAudit, yangMillsAnalyticCompletion, YangMillsAnalyticLegitimate, and YangMillsAnalyticPathology.
In the Recognition framework this is scaffolding for a finite, certificate-driven reading of the Yang–Mills mass gap on the recognition register (eight-tick octave, finite-dimensional Hamiltonian), not a continuum continuum-limit existence proof. It does not yet encode the Clay mass-gap statement; it only standardizes how certificates are displayed for audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.