cert
plain-language theorem explainer
Packages three elementary cost properties into the Module-8 certificate record used for the structural Strong-CP claim. Anyone citing the QCD θ=0 argument from eight-tick uniqueness needs this inhabited certificate. The definition is a pure field assembly: diagonal vanishing, nonnegativity, and positive threshold are plugged in from sibling lemmas.
Claim. There is a certificate record asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS physics stack treats the Strong CP problem as a structural consequence of eight-tick uniqueness: the QCD vacuum angle is forced to $\theta=0$ rather than tuned. Status is a structural theorem (no sorry, no axioms).
The certificate structure bundles three cost facts about a real bivariate domain cost: it is zero when both arguments agree and nonzero, it is nonnegative on the positive quadrant, and a fixed canonical threshold is positive. These are the minimal positivity and normalization conditions needed before any threshold comparison or vacuum-selection argument can run.
Upstream, nonnegativity of recognition cost is already known in the observer-forcing layer: every recognition event has cost $\ge 0$, via nonnegativity of the $J$-cost on positive states. The module specializes that idea to the domain-cost function used here.
proof idea
One-line structure inhabitant. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positives), and canonicalThreshold_pos (strict positivity of the threshold). No further tactic work; the definition is pure assembly of already-proved facts.
why it matters
This is the concrete certificate object for Physics Module 8, whose module claim is that QCD $\theta=0$ follows from eight-tick uniqueness (forcing-chain landmark T7: the period-$2^3$ octave). Without an inhabited certificate of cost normalization and threshold positivity, the structural Strong-CP argument has nothing to attach to.
No downstream consumers are wired in the current graph, so the immediate role is local: close the Module-8 certificate interface and support cert_inhabited. In the broader RS stack it sits under the same eight-tick / $D=3$ forcing spine that fixes the discrete clock against which CP-odd phases are ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.