cert_inhabited
plain-language theorem explainer
The certificate packing three structural cost properties (vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold) is nonempty. Anyone citing the RS structural module on J-cost, the golden ratio, and forced dimension uses this as the existence witness. The proof is a one-line term that packages the already-built certificate instance.
Claim. There exists a certificate asserting that the domain cost vanishes on the diagonal ($\mathrm{cost}(r,r)=0$ for $r\neq 0$), is nonnegative for positive mass and energy arguments, and that the canonical threshold is strictly positive.
background
This module packages the first RS structural prediction: the cost functional takes the form $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$), the golden ratio $\varphi$ is forced as the self-similar fixed point, and spatial dimension $D=3$ is forced. Status is a pure structural theorem (no sorry, no axioms).
The certificate structure bundles three elementary facts about the domain cost and the canonical threshold: cost vanishes when the two arguments coincide and are nonzero; cost is nonnegative whenever both arguments are positive; and the canonical threshold is strictly positive. Those three fields are exactly the data a downstream consumer needs to treat the structural package as inhabited.
Upstream, the structure itself is the only dependency. Sibling lemmas establish each field separately (diagonal vanishing, nonnegativity, threshold positivity) before they are assembled into a single certificate value.
proof idea
Term-mode one-liner. The proof is the anonymous constructor $\langle\mathrm{cert}\rangle$, which inhabits $\mathrm{Nonempty}$ by supplying the already-constructed certificate value whose three fields have been filled by the sibling lemmas on diagonal vanishing, nonnegativity, and threshold positivity. No tactics, no further rewriting.
why it matters
In the Recognition Science forcing chain this module records the structural core: T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$), T6 $\varphi$ as self-similar fixed point, and T8 $D=3$. The inhabited certificate is the Lean-side existence witness that those cost and threshold properties hold simultaneously, so any later development that needs a single package of structural hypotheses can take this nonempty type rather than re-proving the three fields.
No downstream consumers are wired yet in the graph; the declaration closes the module's certificate layer so that later structural or physical theorems can import a single inhabited object rather than three separate lemmas. It does not itself derive $\varphi$ or $D=3$; it only certifies the cost-side scaffolding those derivations rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.