cert_inhabited
plain-language theorem explainer
The module-1 forcing certificate (diagonal vanishing and nonnegativity of domain cost, plus a positive canonical threshold) is inhabited. Anyone wiring the structural RS forcing chain from the J-cost cites this as the existence witness. Proof is a one-line term supplying the prebuilt certificate instance.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($\mathrm{cost}(r,r)=0$ for $r\neq 0$), the domain cost is nonnegative for positive arguments, and the canonical threshold is strictly positive.
background
Module 1 of the RS foundation chain packages the recognition lattice built from the unique cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). The module claims structural status: zero sorry, zero axioms.
The certificate structure bundles three elementary properties of the local domain cost and threshold: diagonal vanishing for nonzero reals, nonnegativity on the positive quadrant, and positivity of the canonical threshold. Those three propositions are the fields of the structure; a concrete inhabitant is assembled earlier in the same module from the corresponding lemmas on domain cost and the threshold constant.
This existence statement is the Nonempty wrapper around that inhabitant, so downstream code can treat the certificate as a pure existence fact rather than naming the concrete value.
proof idea
One-line term proof. The certificate value already constructed in-module is passed as the witness to Nonempty, i.e. the term is exactly the anonymous constructor ⟨cert⟩. No tactics, no further lemmas.
why it matters
Closes the existence obligation for the first structural certificate in the RS forcing-chain modules. The parent module advertises itself as a structural theorem (0 sorry, 0 axiom) whose physical predictions all derive from $J$; inhabiting the certificate is the minimal package that makes those three cost/threshold facts available as a single object.
In the broader forcing chain this sits at the base of the J-cost layer (T5 uniqueness of $J$, Recognition Composition Law). It does not itself force $\varphi$, the eight-tick octave, or $D=3$, but it is the existence gate those later steps assume when they quote module-1 cost identities. No downstream consumers are recorded yet; the declaration is the terminal export of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.