RSCOSStructural007Cert
plain-language theorem explainer
Certificate bundling three structural properties of the cosmology domain cost: it vanishes when both arguments equal any nonzero real, it is nonnegative on positive reals, and the canonical threshold is strictly positive. Cosmology proofs cite the inhabited instance rather than this shell. Pure structure definition; the three field obligations are discharged by sibling lemmas in the same module.
Claim. A certificate consisting of three facts: (i) for every nonzero real $r$, the domain cost of $r$ against itself is zero; (ii) for all positive reals $m,e$, the domain cost of $m$ against $e$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_007 records the ratio symmetry of Recognition Science cost: the J-cost satisfies $J(x)=J(1/x)$, so recognition cost depends only on the magnitude of the ratio, not its orientation. In RS-native units the cost is built from $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain.
The local domainCost is the cosmology-facing specialization of that cost on a pair of positive scale parameters (mass-like and energy-like, or two rung values). The sibling canonicalThreshold is the positive cutoff used to separate negligible from reportable domain cost. Upstream, cost_nonneg in ObserverForcing already states that every recognition event has nonnegative cost, via Jcost_nonneg on a positive state.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The Nonempty theorem is then the one-line constructor ⟨cert⟩.
why it matters
Gives the typed interface for Structural Module 7 (J-cost ratio symmetry) so downstream cosmology code can depend on a single certificate rather than three free-floating lemmas. The parent cert supplies the concrete witness; cert_inhabited exports Nonempty for any consumer that only needs existence. Ties directly to the Recognition Composition Law and T5 J-uniqueness: vanishing on the diagonal is the $J(1)=0$ minimum, nonnegativity is the global cost lower bound, and a positive threshold is the gate for structural claims that compare domain cost against a fixed cutoff. Status line of the module: structural theorem, zero sorry, zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.