cert
plain-language theorem explainer
Packages three proved facts about the gap-45 domain cost into a single certificate: diagonal vanishing, non-negativity for positive mass and energy, and a strictly positive canonical threshold. Cosmology workers citing the D=3 self-reference rung (gap 45) use this bundle. The body is a structure constructor wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive mass $m$ and energy $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module treats RS structural gap 45, the identity $D^2(D+2)=9\cdot 5=45$ at spatial dimension $D=3$. That integer is the minimum rung on the $\phi$-ladder at which stable self-reference is available in three dimensions (forcing chain T8).
The certificate structure records three elementary properties of a real-valued domain cost on mass/energy pairs: it vanishes on the diagonal away from zero, stays nonnegative in the positive quadrant, and sits below a fixed positive threshold. Non-negativity of recognition cost is the same qualitative fact as the upstream $J$-cost bound ("the cost of any recognition event is non-negative"), specialized here to the cosmology domain functional.
Local status is structural: zero sorry, zero axioms. The certificate is the named bundle of those three properties.
proof idea
Pure structure construction. The three fields of RSCOSStructural004Cert are filled by the sibling lemmas already proved in-module: diagonal vanishing, domain-cost non-negativity, and positivity of the canonical threshold. No new algebra is done at this site; it is a one-shot inhabitant of the certificate record.
why it matters
Gives the cosmology stack a single named witness that the gap-45 domain cost behaves like a genuine cost (zero on matched pairs, nonnegative, with a positive threshold). That is the structural content of RS_COS module 4: minimum rung for stable self-reference at $D=3$, tying the forcing-chain dimension result (T8) to the $\phi$-ladder rung count $45=D^2(D+2)$.
No downstream consumers are recorded yet; the declaration exists so later cosmology theorems can assume one object rather than three separate lemmas. It closes the structural certificate for this module rather than advancing a dynamical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.