RSCOSStructural002Cert
plain-language theorem explainer
A certificate packing three structural facts for the cosmology J-cost layer: the domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Cosmology and recognition-cost arguments cite it as the typed bundle of those inequalities. It is a pure structure definition; inhabitants are built by wiring the sibling lemmas.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e>0$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
This module sits in the cosmology structural layer of Recognition Science. The local setting is the RS J-cost at the golden ratio: $J(\varphi)=\varphi-3/2\approx 0.11803$, treated as the recognition cost of the self-similar fixed point forced earlier in the chain (T5–T6).
Domain cost is the real-valued cost assigned to a pair of positive scale parameters (mass-like and energy-like, or measure and expectation). The diagonal vanishing $C(r,r)=0$ encodes perfect match: no recognition defect when the two arguments agree. Non-negativity is the continuum shadow of the foundation fact that every recognition event has non-negative cost (upstream cost_nonneg: "The cost of any recognition event is non-negative").
The canonical threshold is the positive cutoff used downstream to separate negligible from reportable cost; positivity keeps the comparison well-posed.
proof idea
No proof body: the declaration is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that witness.
why it matters
The structure is the typed interface for Structural Module 2 in cosmology. Downstream, cert assembles a concrete inhabitant from the three sibling lemmas, and cert_inhabited records that the certificate type is nonempty, closing the module's structural claim (0 sorry, 0 axiom).
In the broader framework it packages the elementary cost axioms needed before one talks about the golden-ratio minimum $J(\varphi)=\varphi-3/2$ as a physical recognition cost. It does not itself force $\varphi$ or the eight-tick octave; those live in the T5–T7 forcing chain. It supplies the cost-positivity and threshold hygiene that later cosmology certificates can assume without re-proving the foundation inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.