YangMillsDisplayPayload
plain-language theorem explainer
Three-valued tag type labeling how a Yang–Mills mass-gap certificate is displayed: connection, excitation, or zero-mode. Downstream audit and completion records store one of these tags beside resolution and level data. The declaration is a plain inductive with decidable equality and a default inhabitant (connection).
Claim. There is a finite set of display tags for Yang–Mills mass-gap audits, with three elements: connection display, excitation display, and zero-mode display. Equality of tags is decidable, and the default tag is the connection display.
background
The module HardProblemCertificateAudits packages certificate audits for several hard problems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge). Each problem has a certificate type and a display layer that records how the certificate is presented for inspection.
For Yang–Mills, the certificate is YangMillsGapCert. The analytic display record pairs that certificate with a plaquette resolution, an excitation level, and a display-kind tag. The tag type defined here is that kind field: it only classifies the presentation mode, not the gap itself.
Related foundation material (finite-dimensional Hamiltonian generators on the eight-tick register, self-reference certificates, Regge zero-mode geometry) sits upstream in the broader stack; this inductive does not invoke those theorems. It is pure bookkeeping for the audit API.
proof idea
Definitional, not a proof. Three nullary constructors form an enumeration; Lean derives DecidableEq and Repr. An Inhabited instance picks the connection tag as the canonical default. No lemmas are applied.
why it matters
Feeds the Yang–Mills side of the hard-problem audit layer. YangMillsAnalyticDisplay stores a displayKind of this type; yangMillsAnalyticCompletion builds displays with the connection tag by default; yangMillsCertifiedDisplayAudit runs the generic certified-display audit over certificates tagged by these payloads.
In Recognition Science terms this is scaffolding around a mass-gap certificate, not a derivation of the gap from the forcing chain (T0–T8) or the Recognition Composition Law. It lets the audit machinery distinguish connection-level, excitation-level, and zero-mode presentations when certifying or completing a Yang–Mills gap claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.