RSCosmo009Cert
plain-language theorem explainer
Certificate packing three structural facts for RS cosmology module 9 (baryon density): domain cost vanishes on the diagonal, is non-negative for positive arguments, and the canonical threshold is positive. Cited by anyone invoking the inhabited Module-9 cert behind Ω_b ≈ J(φ)(1−J(φ))/2. Pure interface structure; witnesses are sibling lemmas, not proved here.
Claim. A Module-9 certificate is a triple of statements: (i) for every nonzero real $r$, the domain cost at equal arguments vanishes; (ii) whenever $m>0$ and $e>0$, the domain cost of $(m,e)$ is non-negative; (iii) the canonical threshold is strictly positive.
background
Cosmology RS Module 9 is the structural baryon-density slot: it records that $J(\phi)(1-J(\phi))/2 \approx 0.052$ sits next to the observed $\Omega_b \approx 0.0493$, with status STRUCTURAL (0 sorry, 0 axiom). The local cost object is a two-argument domain cost on reals (mass/energy-like coordinates), and a positive canonical threshold is the cutoff used by the module.
The certificate does not recompute $\Omega_b$; it only packages the algebraic hygiene required before that match is quoted: diagonal vanishing, non-negativity off the diagonal for positive inputs, and threshold positivity. Upstream, ObserverForcing records that every recognition event has non-negative cost via the J-cost non-negativity lemma ("The cost of any recognition event is non-negative").
proof idea
No proof body: this is a structure definition whose three fields are Prop-valued obligations. Inhabitation is separate. The downstream cert definition fills the fields by wiring sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then packages that witness as Nonempty RSCosmo009Cert.
why it matters
Gives the typed bundle that cert and cert_inhabited inhabit, so Module 9 can be cited as a nonempty structural certificate rather than a loose collection of lemmas. Downstream, cert is the concrete witness and cert_inhabited closes the nonempty claim for the module.
In the broader RS stack this sits under the cosmology layer that uses the forced J-cost (T5) and $\phi$ as the self-similar fixed point (T6): the baryon-density expression is built from $J(\phi)$. It does not itself force $J$ or $\phi$; it only certifies the cost/threshold side-conditions the module needs before quoting the $\Omega_b$ structural match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.