cert_inhabited
plain-language theorem explainer
The Module-8 physics certificate is inhabited: there exists a witness packing diagonal vanishing of the domain cost, its nonnegativity off the axes, and positivity of the canonical threshold. Anyone citing the structural Strong-CP package for this module uses this existence fact. The proof is a one-line term that hands the already-built certificate to Nonempty.
Claim. There exists a certificate packing three facts: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS physics layer targets the Strong CP problem: QCD $\theta=0$ is forced by eight-tick uniqueness rather than by a dynamical axion. The module status line records a structural theorem with zero sorry and zero axioms.
The certificate structure packages three elementary cost facts used throughout the module. The domain cost $C$ is the local cost functional on positive mass/energy-type coordinates; its diagonal vanishing and off-axis nonnegativity are the usual J-cost sanity conditions specialized to this domain. The canonical threshold is a positive real cutoff against which domain comparisons are made.
Upstream, the structure itself only declares the three fields; the concrete witness cert (a sibling) is what actually fills them from the proved lemmas on domain cost and the threshold.
proof idea
One-line term proof. Nonempty is inhabited by the existing certificate value cert, written as the anonymous constructor ⟨cert⟩. No tactics, no further lemmas: the work of proving the three fields already lives in the construction of that witness.
why it matters
This is the inhabitance gate for the Module-8 certificate. Downstream consumers that need a single named package of cost-diagonal, cost-nonnegativity, and positive threshold can cite Nonempty rather than reassemble the three lemmas. In the broader RS chain it sits under the structural Strong-CP claim: QCD $\theta=0$ from eight-tick uniqueness (T7 period $2^3$), with no axion field required. The module advertises a closed structural theorem; inhabitance of the cert is the small bookkeeping step that makes that package usable as a hypothesis elsewhere. No further used-by edges are recorded yet, so its present role is local packaging inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.