cert_inhabited
plain-language theorem explainer
The certificate bundle for RS cosmology structural claim 7 is inhabited: there exists a witness that domain cost vanishes on equal arguments, stays nonnegative for positive masses and energies, and that the canonical threshold is strictly positive. Cosmology and cost-functional workers cite it to discharge Nonempty obligations when wiring the J-ratio symmetry package. Proof is a one-constructor term that packages the already-built certificate.
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_COS_Structural_007 records the structural fact that Recognition Science J-cost is ratio-symmetric: $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 ratio arguments incur zero excess cost and the cost stays nonnegative off the diagonal.
The certificate structure packages three elementary properties of the local domain-cost functional: vanishing when the two arguments coincide and are nonzero, nonnegativity for positive mass and energy arguments, and positivity of a fixed canonical threshold used as a comparison scale. These are the minimal algebraic facts needed before any cosmological application of the symmetry.
Upstream, the structure itself is the only dependency; the module imports Constants and Cost so that domain cost and the threshold are the same objects used elsewhere in the monolith.
proof idea
One-line term proof. The certificate value cert already inhabits the structure, so ⟨cert⟩ is a term of type Nonempty RSCOSStructural007Cert. No tactics, no further lemmas.
why it matters
Closes the structural package for cosmology module 7: once the certificate is known to be inhabited, downstream cosmology developments can assume J-ratio symmetry, diagonal vanishing, and a positive threshold without re-proving the three field obligations. The module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom), so this inhabitation is the final gate that the cost side of the forcing chain (T5 J-uniqueness and the Recognition Composition Law) is available in cosmological arguments. No downstream users are wired yet in the graph; the lemma is the export point for later RS cosmology layers that need a clean Nonempty hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.