cert_inhabited
plain-language theorem explainer
The module-9 forcing certificate is inhabited: a single witness packs diagonal vanishing of domain cost, its nonnegativity on positive arguments, and positivity of the canonical threshold. Foundation auditors cite this to discharge the existence obligation for J-cost ratio symmetry. Proof is a one-line term packaging the prebuilt certificate.
Claim. The type of certificates packing (i) vanishing of domain cost on equal nonzero reals, (ii) nonnegativity of domain cost for positive mass and energy, and (iii) strict positivity of the canonical threshold, is nonempty.
background
Foundation module 9 records the structural fact that recognition cost is ratio-symmetric: $J(x)=J(1/x)$. Status is a structural theorem (zero sorry, zero axioms). The local certificate structure packages three elementary properties used in that argument.
Domain cost is the in-module cost on pairs of real arguments. Its diagonal vanishing ($\mathrm{cost}(r,r)=0$ for $r\neq 0$) and nonnegativity on positive mass/energy are the algebraic content supporting ratio symmetry. The canonical threshold is a strictly positive real cutoff appearing alongside those facts.
The certificate structure is exactly the triple of those three propositions; inhabitation means a concrete witness for all three exists in the module.
proof idea
One-line term proof. The preexisting sibling witness cert (of certificate type) is injected into Nonempty by the anonymous constructor. No tactics and no further lemmas are applied.
why it matters
Closes the existence side of Foundation module 9 on J-cost ratio symmetry. That symmetry is the first algebraic identity feeding the T5 J-uniqueness strand of the forcing chain, where $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is forced. The module is marked structural with zero sorry and zero axioms. No downstream dependents are recorded in this mirror snapshot; the declaration is the terminal existence stamp for the module's certificate bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.