cert
plain-language theorem explainer
Certificate packing three structural facts for RS Physics Module 5: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Cited by anyone using the module's QCD one-loop count-law setup (b_0 = 7 from D = 3). Proof is a structure inhabitant wiring three sibling lemmas.
Claim. There is a certificate asserting that the domain cost $C$ satisfies $C(r,r)=0$ for every $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $\tau$ obeys $\tau>0$.
background
Physics RS Module 5 treats the QCD one-loop coefficient as forced by the count law: $b_0=7=2^D-1$ once spatial dimension is $D=3$. Status is structural (zero sorry, zero axiom).
The domain cost $C(m,e)$ is the module's local cost on a mass/energy pair. The canonical threshold is the positive cutoff used to gate comparisons in that cost landscape. The certificate structure bundles exactly three properties needed before count-law statements: diagonal vanishing, nonnegativity on the positive quadrant, and threshold positivity.
Upstream, recognition-event cost nonnegativity (from ObserverForcing: "the cost of any recognition event is non-negative") underwrites the domain-cost nonnegativity sibling used here.
proof idea
Definitional structure inhabitant, not a tactic proof. The three fields of the certificate are filled by the sibling lemmas: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further rewriting.
why it matters
Gives the inhabited certificate that lets Module 5 claim structural-theorem status for the count-law identification $b_0^{\mathrm{QCD}}=7=2^D-1$. That identification sits on the forcing chain landmark T8 ($D=3$ spatial dimensions) and the eight-tick/octave counting that produces $2^D-1$.
No downstream dependents appear in the graph yet; the declaration is the module-level witness itself. It does not re-prove $D=3$ or the beta-function algebra; it only packages the cost/threshold hygiene those arguments assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.