yangMillsGap_finiteReduction
plain-language theorem explainer
The Yang–Mills mass-gap audit admits a finite-certificate reduction: every legitimate configuration and every pathology is witnessed by some finite certificate under the audit completion. Anyone assembling the hard-problem audit headline cites this instance. The proof is a one-line wrapper of the generic problem-audit finite-reduction theorem.
Claim. The Yang–Mills gap problem audit has a finite-certificate reduction: for every legitimate datum $d$ there exists a finite certificate $c$ that certifies $d$, and for every pathology $d$ there likewise exists a finite certificate $c$ that certifies $d$.
background
In the quantized-proof layer, a continuum hard problem is packaged as a ProblemAudit: a triple of types (nominal objects, data, certificates) together with predicates for legitimate data and pathologies, plus a completion map that turns certificates into claims about data. The key property is finite-certificate reduction: both the legitimate class and the pathology class must descend to finite certificates under that completion.
Concretely, HasFiniteReduction A asserts
$(\forall d,, A.\mathrm{legitimate}, d \to \exists c,, A.\mathrm{completion}.\mathrm{certifies}, c, d)$
and the same for pathologies. The Yang–Mills gap audit is the identity certificate audit on the Yang–Mills gap certificate type: nominal objects, data, and certificates coincide, so the completion is the identity witness map.
The module collects four such application stubs (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic cycles). Each is an audit schema, not a solution of the underlying continuum problem.
proof idea
One-line wrapper. Apply the generic theorem problemAudit_finiteReduction to the Yang–Mills gap audit. That theorem itself is just the finite-certificate transfer lemma specialized to the audit’s completion, legitimate predicate, pathology predicate, and the two conservativity hypotheses already stored on the audit record. No Yang–Mills-specific algebra is invoked.
why it matters
Feeds the hard-problem audit headline, which packages the four finite-reduction theorems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge) as a single conjunction. The headline’s doc-comment is explicit: these are audit schemas with concrete finite certificate inventories, not solutions of the continuum problems.
Inside Recognition Science this sits in the Primitive Recognition Calculus layer: continuum Millennium-type questions are forced into a common finite-certificate interface so that later forcing-chain or ledger arguments can treat them uniformly. It does not touch T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$) directly; it only supplies the audit side-condition those later arguments may assume when they specialize to gauge-gap data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.