cert
plain-language theorem explainer
Packages three elementary properties of the cosmology domain cost into a single certificate: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Cosmology modules that need a ready-made witness for these structural facts can cite the certificate. The definition is a pure structure inhabitant that wires three already-proved lemmas into the three fields.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
Module RS_COS_Structural_009 sits in the cosmology layer of the Recognition Science forcing chain (T5 J-uniqueness through T8 forcing $D=3$). It is marked as a structural theorem module: zero sorry, zero axioms.
The domain cost is the local cost functional used on positive real pairs (mass/energy-style arguments). Its diagonal vanishing and nonnegativity are the elementary positivity properties one expects of a J-type cost: the Recognition cost $J$ satisfies $J(1)=0$ and $J\ge 0$, and the domain cost inherits the same shape. The canonical threshold is a fixed positive real used as a comparison scale in the structural claims of this module.
Upstream, nonnegativity of recognition-event cost is already available from ObserverForcing (cost_nonneg: "The cost of any recognition event is non-negative"), via Jcost_nonneg. The three field lemmas packed here are the in-module specializations of those facts to domainCost and canonicalThreshold.
proof idea
One-line structure inhabitant. The three fields of RSCOSStructural009Cert are filled by direct assignment of the three sibling lemmas already proved in the same module: diagonal vanishing (domainCost_at_eq), nonnegativity on the positive quadrant (domainCost_nonneg), and positivity of the threshold (canonicalThreshold_pos). No extra rewriting or case analysis occurs at this site.
why it matters
Gives a single named witness that the domain-cost layer of cosmology structural module 9 is well-formed: cost vanishes on matched arguments, never goes negative, and the threshold scale is positive. Downstream cosmology arguments that quantify over certificates, or that need to discharge the three hypotheses in one step, can take this inhabitant rather than re-proving the three facts.
In the broader RS chain this is housekeeping under the T5–T8 forcing spine (J-uniqueness, phi fixed point, eight-tick octave, $D=3$), not a new physical prediction. No parent theorems currently list it as a dependency (used_by is empty), so its role is local packaging for the structural certificate interface of this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.