cert
plain-language theorem explainer
Packages three structural facts about the cosmology domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is strictly positive. Cosmology and RS cost-symmetry arguments cite it as the inhabited witness for module 7. The body is a pure structure assembly from three local lemmas.
Claim. There is 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. These encode ratio-symmetry of recognition cost, i.e. the $J$-cost identity $J(x)=J(1/x)$ at the structural level.
background
Module 7 of the RS cosmology structural series records the ratio symmetry of recognition cost: $J(x)=J(1/x)$. In RS units the cost functional is the unique $J$ forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$, which is minimized at $x=1$ and invariant under $x\mapsto 1/x$.
Domain cost is the local cost comparison between a measured scale $m$ and an expected scale $e$. The certificate structure demands three properties: vanishing when $m=e\neq 0$ (perfect match costs nothing), nonnegativity for positive arguments, and a strictly positive canonical threshold used as a comparison yardstick.
Upstream, nonnegativity of recognition-event cost is already proved in ObserverForcing via $J$-cost nonnegativity on positive states. The present module specializes that fact to the cosmology domain-cost wrapper.
proof idea
One-line structure construction. The three fields of RSCOSStructural007Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive $m,e$), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site; the def only packages those proofs into the certificate record.
why it matters
Gives the inhabited structural certificate for RS cosmology module 7, the $J$-cost ratio-symmetry layer. That symmetry is a direct corollary of T5 $J$-uniqueness in the forcing chain: the unique cost solving the Recognition Composition Law satisfies $J(x)=J(1/x)$ identically. Downstream consumers (none linked yet in this graph) would use the certificate to discharge hypotheses that domain cost is a genuine nonnegative defect vanishing on matched scales, before comparing against the positive canonical threshold. Status is structural: zero sorry, zero axioms, pure packaging of already-proved local facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.