RSCosmo003Cert
plain-language theorem explainer
Certificate bundle for Cosmology Module 3 (Hubble tension): diagonal vanishing of the domain cost, nonnegativity on positive arguments, and positivity of the canonical threshold. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure structure definition packing three Prop fields; no proof body.
Claim. A Module-3 cosmology certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module RS_Cosmo_Module_003 treats the Hubble tension as a Recognition Science structural claim: the ratio $H_{0,\mathrm{local}}/H_{0,\mathrm{CMB}}$ is forced into the open interval $(1.075,1.091)$, which contains the SH0ES value $1.0837$. Status is a structural theorem (zero sorry, zero axiom).
The domain cost $C$ is the module-local cost on pairs of positive reals (built from the global $J$-cost of Recognition Science). Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J$-cost nonnegativity. The canonical threshold is the positive cutoff used to gate the Module-3 pass condition against that cost.
This structure does not compute the Hubble band; it only packages the three cost/threshold side-conditions the certificate must carry.
proof idea
No proof: the declaration is a structure with three Prop-valued fields. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that inhabitant.
why it matters
Gives the typed interface for the Module-3 cosmology certificate. Downstream, cert supplies a concrete term of this type, and cert_inhabited proves Nonempty RSCosmo003Cert, closing the structural theorem advertised in the module doc (Hubble ratio band with SH0ES inside, RS_PASS).
In the broader RS stack this sits under the cost calculus forced by the Recognition Composition Law and $J$-uniqueness (T5): nonnegative cost with a unique minimum on the diagonal is the same pattern used for recognition events. The threshold positivity field is the local gate that lets the module claim a pass without reopening the global forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.