cert_inhabited
plain-language theorem explainer
The certificate bundle for Recognition-cost ratio symmetry is inhabited: there exists a witness that domain cost vanishes on equal arguments, stays nonnegative for positive inputs, and that the canonical threshold is positive. Foundation auditors cite it to discharge the structural package for J-cost symmetry J(x)=J(1/x). The proof is a one-line term that packages the concrete certificate as a Nonempty witness.
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_007 packages the structural fact that Recognition cost is ratio-symmetric: the J-cost satisfies $J(x)=J(1/x)$. In RS-native units the cost is built from the unique T5 functional $J(x)=(x+x^{-1})/2-1$, so equal measure and expectation yield zero cost and the cost never goes negative on the positive cone.
The certificate structure collects three elementary properties of the local domain-cost functional: diagonal vanishing off zero, nonnegativity for positive arguments, and positivity of a fixed canonical threshold used as a comparison scale. These are the minimal algebraic checks that the cost is a genuine defect relative to perfect match.
Upstream, the structure itself is the only dependency; the concrete inhabitant cert is assembled in-module from the sibling lemmas that prove each field.
proof idea
One-line term proof. The inhabitant is obtained by packaging the already-constructed concrete certificate as a Nonempty witness via the anonymous constructor ⟨cert⟩. No further tactics or lemmas are invoked.
why it matters
This declaration closes the structural package for Foundation module 7: once the certificate type is known to be inhabited, downstream foundation code may assume ratio symmetry of Recognition cost without re-proving diagonal vanishing, nonnegativity, or threshold positivity. It sits inside the STRUCTURAL THEOREM layer (0 sorry, 0 axiom) that underwrites the J-uniqueness forcing step T5 and the Recognition Composition Law, both of which treat $J(x)=J(1/x)$ as primitive. No further used-by edges are recorded yet; the lemma is the terminal inhabitance stamp for the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.