RSCOSStructural009Cert
plain-language theorem explainer
Certificate bundle for Cosmology structural claim 009: the domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Cosmology and forcing-chain auditors cite it as the typed interface that the module's concrete witness must inhabit. It is a pure structure definition with no proof body; inhabitation is discharged downstream by the named field lemmas.
Claim. A certificate consists of three properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e > 0$, the domain cost of $(m,e)$ is non-negative; (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$). Status is structural: zero sorry, zero axiom. The local objects are a real-valued domain cost on pairs of positive scales and a canonical positive threshold used as a comparison cut.
Domain cost is the module's specialization of the recognition cost. Upstream, ObserverForcing records that every recognition event has non-negative cost via $J$-cost non-negativity on positive states, with the identity event at the $J$-minimum $x=1$. The diagonal vanishing field here is the matching statement that equal arguments incur zero domain cost.
The three fields package exactly the inequalities a later cosmology argument needs: zero self-cost, global non-negativity on the positive orthant, and a strictly positive threshold against which costs can be compared.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, non-negativity for positive arguments, positivity of the canonical threshold). Inhabitation is supplied by the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields, and by the one-line theorem cert_inhabited that wraps that witness as Nonempty.
why it matters
The structure is the typed contract for Cosmology structural module 9. Downstream, cert builds an explicit inhabitant and cert_inhabited records non-emptiness, closing the module's structural certificate with no sorry. In the RS forcing narrative (T5 $\phi$-linked $J$-uniqueness, T6 $\phi$ fixed, T7 eight-tick octave, T8 $D=3$), this package isolates the cost and threshold inequalities cosmology needs before quantitative ladder or mass claims. It does not itself force $\phi$ or $D=3$; it only standardizes the cost-side hypotheses those later steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.