RSPhysics005Cert
plain-language theorem explainer
A certificate structure packaging three domain-cost axioms used by Physics Module 5 (QCD one-loop coefficient b_0 = 7 = 2^D-1). It requires the domain cost to vanish on the diagonal, stay non-negative for positive arguments, and that the canonical threshold is positive. Anyone citing the module's structural theorem or its inhabited certificate uses this bundle. The declaration is a pure structure definition; inhabitants are assembled from sibling lemmas.
Claim. A certificate for Physics Module 5 consists of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 5 records the structural claim that the QCD one-loop coefficient satisfies $b_0 = 7 = 2^D - 1$, forced by the Count Law once spatial dimension $D = 3$ is fixed (forcing chain T8). The module is marked structural: zero sorry, zero axioms.
The domain cost is the local cost functional on pairs of positive reals (mass/energy-like arguments) used inside this module; sibling lemmas establish that it vanishes on the diagonal and is nonnegative off it. The canonical threshold is the positive cutoff against which that cost is compared.
Upstream, the foundation result cost_nonneg states that the cost of any recognition event is nonnegative, via nonnegativity of the J-cost $J(x) = (x+x^{-1})/2-1$ for $x>0$. The certificate's nonnegativity field is the domain-level analogue of that fact.
proof idea
No proof body: this is a structure definition with three fields. Inhabitation is deferred to the sibling definition cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The nonempty theorem cert_inhabited is then the one-line wrapper ⟨cert⟩.
why it matters
The structure is the typed interface that Module 5's structural theorem exposes. Downstream, cert builds a concrete inhabitant and cert_inhabited proves Nonempty RSPhysics005Cert, so any later development that needs "Module 5 is certified" can depend on a single inhabited record rather than three loose lemmas.
In the Recognition framework this sits under the D=3 forcing (T8) and the Count Law identity $2^D-1=7$ that fixes the QCD one-loop coefficient. It does not itself derive $b_0$; it packages the cost and threshold hygiene that the module's structural claim relies on. Parent consumers are exactly cert and cert_inhabited in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.