RSCOSStructural010Cert
plain-language theorem explainer
Certificate structure packaging three structural properties for RS cosmology module 10: the domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is strictly positive. Cosmology and calibration proofs cite it as the typed bundle of those claims. It is a pure structure definition with no proof body; inhabitants supply the field proofs.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{cost}(r,r)=0$; (ii) for all $m,e>0$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module RS_COS_Structural_010 is a cosmology structural layer in Recognition Science. The module doc fixes the calibration stance: the coherence energy $E_{\mathrm{coh}}$ is set once from the electron mass, after which predictions are parameter-free, and the file is marked structural (zero sorry, zero axiom).
The domain cost is a two-argument real cost used for mass/energy comparisons in this layer. Its diagonal vanishing and nonnegativity mirror the global J-cost story: recognition cost is minimized on the identity ratio and never goes negative. Upstream, ObserverForcing records that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states.
The canonical threshold is the positive cutoff against which domain-cost comparisons are judged in the structural claims of this module.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Concrete proofs live in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, which the downstream cert value plugs into the fields.
why it matters
The structure is the typed contract for structural module 10. Downstream, cert builds an explicit inhabitant by wiring the three sibling lemmas into the fields, and cert_inhabited records Nonempty of the certificate type. That pattern lets later cosmology results depend on a single named bundle rather than three loose hypotheses.
In the broader RS forcing picture this sits on the cost side of the foundation (nonnegative J-type cost, identity minimum), specialized to cosmology calibration where $E_{\mathrm{coh}}$ is fixed once. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only packages the local cost/threshold hygiene those later claims assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.