cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single EOS Deep-4 certificate: diagonal vanishing, non-negativity for positive mass/energy, and a strictly positive canonical threshold. Cosmologists citing the RS vacuum equation-of-state (w = −1) use this bundle as the structural witness. The body is a pure structure inhabitant that wires three already-proved lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero ratio against itself vanishes, $\mathrm{cost}(r,r)=0$ for $r\neq 0$; (ii) for positive mass and energy the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
RS Cosmology (session 3) is marked as a structural theorem with zero sorry and zero axioms. The headline claim is that the vacuum equation of state is exactly $w=-1$; any DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify the framework. Present DESI BAO numbers ($w_0\approx -0.95$, $w_a\approx -0.27$) show only mild tension.
The domain cost is the local cost functional on mass/energy pairs used to police the vacuum sector. Its diagonal vanishing and non-negativity mirror the global J-cost non-negativity theorem from ObserverForcing ("the cost of any recognition event is non-negative"), specialized to the cosmology domain. The canonical threshold is the positive cutoff that separates allowed vacuum configurations from disallowed ones.
The certificate structure simply records these three Prop-valued fields so downstream cosmology lemmas can assume a single inhabited witness rather than three separate hypotheses.
proof idea
One-line structure inhabitant. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of the domain cost, non-negativity of the domain cost on the positive orthant, and positivity of the canonical threshold. No new arithmetic is performed; the definition only packages those results.
why it matters
This certificate is the structural witness that the RS vacuum sector is well-posed: cost vanishes on equilibrium ratios, never goes negative, and sits above a positive threshold. That package underwrites the module-level claim that $w=-1$ exactly, which is the sharp cosmological prediction of Recognition Science. The module doc states the falsifier explicitly: a $2\sigma$ DESI Y3 departure from $w=-1$ kills the framework. No downstream users are recorded yet; the immediate sibling cert_inhabited is the natural consumer that turns the definition into an existence fact for later forcing or EOS lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.