cert_inhabited
plain-language theorem explainer
The structural certificate packing diagonal vanishing of domain cost, its nonnegativity for positive arguments, and positivity of the canonical threshold is inhabited. Foundation authors cite it to discharge Nonempty obligations when wiring the golden-ratio J-cost package. Proof is a one-line term witness: the explicit certificate value.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_002 packages the golden-ratio recognition cost: the RS J-cost attains $J(\varphi)=\varphi-3/2\approx 0.11803$ at the self-similar fixed point $\varphi$. Status is structural (zero sorry, zero axiom).
The certificate structure bundles three elementary cost facts used throughout the foundation layer. Domain cost is the local cost functional on pairs of positive reals (imported from Cost); on the diagonal it must vanish, off the diagonal it must stay nonnegative. The canonical threshold is the positive cutoff against which those costs are compared.
Upstream, the structure itself only declares the three fields; inhabitance is what turns the interface into a usable package.
proof idea
One-line term proof. The explicit value cert (built in-module from the three sibling lemmas on diagonal vanishing, nonnegativity, and threshold positivity) is supplied as the witness of Nonempty, via the standard constructor ⟨cert⟩.
why it matters
Closes the inhabitance obligation for Structural Module 2 of the foundation layer, the module that records the J-cost minimum at $\varphi$. In the forcing chain this sits next to T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point): once the cost package is certified nonempty, downstream foundation developments can assume the three cost axioms without re-proving them.
No external used-by edges are recorded yet; the declaration is the module-level seal that the structural theorem is fully witnessed rather than merely stated as a Prop interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.