yangMillsAnalyticAudit
plain-language theorem explainer
Packages the Yang–Mills mass-gap stub as a problem audit: finite certificates (plaquette ledger, excitation-gap witness, zero-mode obstruction), an analytic display record, and legitimate/pathology predicates that are identically true and conservative for the completion map. Downstream headline theorems cite it to assert a finite-reduction interface exists. The body is pure structure assembly from prebuilt completion and conservativity witnesses.
Claim. The Yang–Mills mass-gap analytic audit is the problem-audit record whose certificate type is the finite inventory $\{\text{plaquette ledger},\ \text{excitation-gap witness},\ \text{zero-mode obstruction}\}$, whose display type carries a certificate together with plaquette resolution, excitation level, and a display payload, whose completion sends each certificate $c$ to the default display $\langle c,0,0,\text{connection}\rangle$ certified by $c=d.\mathrm{cert}$, and whose legitimate and pathology predicates are both identically $\top$ and conservative for that completion.
background
This module builds domain-specific analytic audits for four hard-problem stubs (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic). Each audit is an instance of ProblemAudit: a finite certificate type, a display type, a completion map from certificates to displays, and legitimate/pathology predicates required to be conservative for that completion.
For Yang–Mills the certificate inventory is three constructors: finite plaquette ledger, excitation-gap witness, and zero-mode obstruction witness. The analytic display record adds natural-number parameters (plaquette resolution, excitation level) and a display-payload tag. The completion used here is the trivial default embedding that stamps resolution and level to zero and tags a connection display, with certification predicate $c = d.\mathrm{cert}$.
Legitimate and pathology predicates on displays are both defined as $\top$. Conservativity then reduces to recovering the certificate field of any display, which is immediate from the display structure.
proof idea
Definitional structure fill-in, not a tactic proof. The completion field is the prebuilt default map yangMillsAnalyticCompletion. Legitimate and pathology are the constant-true predicates. The two conservativity fields are the left and right conjuncts of yangMillsAnalytic_conservative, whose proof is constructor <;> intro d _ <;> exact ⟨d.cert, rfl⟩: for any display, the certificate component witnesses certification under the completion.
why it matters
Feeds domain_specific_analytic_audits_headline, which asserts that the four hard-problem stubs each admit a named analytic audit with HasFiniteReduction. The headline doc is explicit: the reductions still do not solve the problems; they fix the exact display interface that future analytic proofs must refine.
In the Recognition stack this is scaffolding for a Millennium-style mass-gap claim inside the primitive recognition calculus, not a derivation from the forcing chain (T0–T8), RCL, or the $\phi$-ladder mass formula. It only freezes the certificate vocabulary (plaquette ledger, excitation gap, zero-mode obstruction) so later work can attach real analytic content without changing the audit API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.