cert_inhabited
plain-language theorem explainer
The structural certificate for Recognition J-cost symmetry is inhabited: domain cost vanishes on equal nonzero arguments, is nonnegative on positive reals, and the canonical threshold is positive. Anyone needing a single witness packing those three facts cites this. The proof is a one-line term that hands the existing certificate value to Nonempty.
Claim. The type of certificates packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) $\mathrm{canonicalThreshold}>0$, is nonempty.
background
Module RS_MTH_Structural_007 records the ratio symmetry of Recognition cost: $J(x)=J(1/x)$. Status is structural theorem (zero sorry, zero axiom). The local cost object is domainCost, a real bivariate function used as the working stand-in for the J-cost on positive scales; the module also fixes a positive real canonicalThreshold.
The certificate structure bundles three elementary properties already proved as siblings: diagonal vanishing (domainCost r r = 0 for $r\neq 0$), nonnegativity on the positive quadrant, and positivity of the threshold. Those three fields are exactly the data a downstream consumer needs to treat the module as a closed structural unit without reopening the cost definitions.
proof idea
One-line term proof. The sibling value cert already assembles an inhabitant of the certificate structure from the three proved field lemmas. The theorem is simply ⟨cert⟩, i.e. the standard introduction rule for Nonempty.
why it matters
Gives a single inhabited certificate object for Structural Module 7 (J-cost ratio symmetry). In the Recognition forcing chain this sits under the T5 J-uniqueness landmark: $J(x)=(x+x^{-1})/2-1$ is forced and is visibly invariant under $x\mapsto 1/x$, which is the content the module packages. No downstream users are recorded yet; the certificate is the export surface other mathematics or physics modules can import when they need diagonal vanishing, nonnegativity, and a positive threshold without depending on the internal cost construction. Closes the module as a self-contained structural unit with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.