cert
plain-language theorem explainer
Inhabited certificate packing three structural facts for the RS cosmology Hubble-tension module: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the module-3 RS_PASS (H0_local/H0_CMB band containing SH0ES) uses this object. The definition is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero real against itself is zero; (ii) for positive mass and energy arguments the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
RS Cosmology Module 3 treats the Hubble tension as a recognition-cost comparison: the local-to-CMB ratio $H_{0,\mathrm{local}}/H_{0,\mathrm{CMB}}$ is required to lie in $(1.075,1.091)$, which contains the SH0ES central value $1.0837$. The module is marked structural (zero sorry, zero axiom) and reports RS_PASS once the cost and threshold facts are in hand.
The certificate structure demands three properties of the module's domain cost and canonical threshold. Domain cost is the recognition cost specialized to the cosmology comparison variables; it inherits nonnegativity from the global J-cost (the unique cost forced by the Recognition Composition Law). The upstream result cost_nonneg states that every recognition event has nonnegative cost, via $J$-cost nonnegativity at positive state. The canonical threshold is the positive cutoff used as the pass gate for the ratio band.
proof idea
Pure structure instance, not a tactic proof. The three fields of the certificate are filled by the sibling lemmas already proved in the same module: diagonal vanishing of domain cost, nonnegativity of domain cost for positive arguments, and positivity of the canonical threshold. No further rewriting or arithmetic is performed at this site.
why it matters
This definition is the inhabited witness that Module 3's structural hypotheses hold, so the Hubble-tension band claim can be cited as an RS_PASS structural theorem. It sits at the end of the local cost/threshold chain (domain cost lemmas plus canonical-threshold positivity) and packages them for any downstream cosmology consumer. In the broader framework it is an application layer on top of J-cost nonnegativity (T5 uniqueness of $J$), not a new forcing step. The used-by graph is currently empty; the immediate consumer is the module's own pass report and any later aggregator that requires an RSCosmo003Cert value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.