cert
plain-language theorem explainer
Packages the three structural hypotheses of Cosmology Module 9 into a single certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is positive. Cosmologists citing the RS baryon-density match Ω_b ≈ J(φ)(1−J(φ))/2 use this bundle. The definition is a pure structure inhabitant that wires three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Cosmology Module 9 is the structural RS account of the baryon density parameter. The module claims the closed-form value $J(\varphi)(1-J(\varphi))/2 \approx 0.052$ sits next to the observed $\Omega_b \approx 0.0493$, and marks the result as a structural theorem (no sorry, no axioms).
Domain cost is the local cost functional on mass–energy pairs used in this module; the certificate demands it vanish when the two arguments coincide (the recognition identity) and stay nonnegative off the diagonal. The canonical threshold is the positive cutoff against which that cost is compared. Upstream, the foundation lemma cost_nonneg already records that every recognition event has nonnegative $J$-cost, which is the global ancestor of the domain-level nonnegativity field.
The certificate structure itself is only a Prop-bundle: three fields, no numerical evaluation of $\Omega_b$.
proof idea
One-line structure inhabitant. The three fields of RSCosmo009Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or tactics; the definition is pure packaging.
why it matters
Module 9 is the RS structural derivation of the baryon density from the $J$-cost at the golden ratio fixed point $\varphi$. The certificate is the single object that witnesses the three cost/threshold axioms the module needs before any numerical comparison with $\Omega_b$ is stated. It sits at the end of the local forcing chain for this module and inherits nonnegativity from the foundation cost law (T5 $J$-uniqueness lineage). No downstream consumers are recorded yet; the inhabited certificate is the export surface for later cosmology assembly theorems that want a single hypothesis package rather than three separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.