cert_inhabited
plain-language theorem explainer
The Module 5 physics certificate is inhabited: a witness exists packing diagonal vanishing of domain cost, its nonnegativity for positive arguments, and positivity of the canonical threshold. Anyone treating the QCD one-loop coefficient b_0 = 7 = 2^D-1 as a closed structural fact would cite this. The proof is a one-line term that injects the prebuilt certificate into Nonempty.
Claim. The type of certificates asserting (i) domain cost vanishes on equal nonzero real arguments, (ii) domain cost is nonnegative for positive mass and energy, and (iii) the canonical threshold is strictly positive, is nonempty.
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 step T8). Status is structural: zero sorry, zero axiom.
The certificate structure packages three elementary analytic facts used in that argument. Domain cost is the local cost comparison between mass and energy scales; it must vanish when the two arguments coincide (and are nonzero) and stay nonnegative when both are positive. The canonical threshold must be strictly positive so any comparison against it is well-posed.
Those three fields are exactly the content of the certificate type whose inhabitation is asserted here.
proof idea
One-line term proof. The module already builds a concrete certificate value whose three fields discharge diagonal vanishing, nonnegativity, and threshold positivity. The proof simply wraps that value in the anonymous constructor of Nonempty, producing a witness with no further lemmas or tactics.
why it matters
Inhabitation closes the structural certificate for Module 5, so downstream code can treat the $b_0 = 7$ package as available without rebuilding the three component proofs. The module sits under the Count Law identity $2^D - 1$ with $D = 3$ forced by T8 of the unified forcing chain; together with the eight-tick octave (T7) this pins the one-loop QCD coefficient as a pure counting fact rather than a free parameter. No further parent theorems currently depend on this inhabitation edge, but it is the standard Nonempty gate that any later consumer of the Module 5 certificate would open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.