cert
plain-language theorem explainer
A certificate packing three structural facts about the cosmology domain cost: it vanishes on equal arguments, stays nonnegative for positive inputs, and the canonical threshold is strictly positive. Cosmology developments that need a single inhabited witness of these properties cite this bundle. The definition is a structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: the domain cost satisfies $C(r,r)=0$ for every nonzero real $r$; $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold $T$ obeys $T>0$.
background
This module is Cosmology RS Structural Module 2. It records the golden-ratio recognition cost: the RS J-cost attains its characteristic value at $\varphi$, namely $J(\varphi)=\varphi-3/2\approx 0.11803$, and is marked as a structural theorem (zero sorry, zero axiom).
The certificate structure packages three properties of the local domain cost $C$ (built from the RS cost $J$) and of a fixed positive threshold $T$. The first says $C$ vanishes on the diagonal away from zero. The second is nonnegativity for positive mass/energy-style arguments. The third is positivity of $T$.
Upstream, nonnegativity of recognition cost is the standard fact that every recognition event has $J$-cost $\ge 0$ (via $J\ge 0$ on positive reals). The three field proofs are sibling lemmas in this same module.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas: diagonal vanishing of the domain cost, nonnegativity of the domain cost on positive arguments, and positivity of the canonical threshold. No extra tactic work.
why it matters
Gives an inhabited, zero-sorry witness that the cosmology domain cost and threshold satisfy the three structural axioms used in this module. The parent setting is the golden-ratio recognition cost $J(\varphi)=\varphi-3/2$, tying the certificate to the T5/T6 forcing landmarks ($J$-uniqueness and $\varphi$ as self-similar fixed point). No downstream consumers are recorded yet; the companion inhabitedness lemma is the immediate sibling use site. Closes the structural side of RS_COS_Structural_002 without axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.