cert
plain-language theorem explainer
Packages three structural facts about the cosmology domain cost into a single certificate: it vanishes on the diagonal, stays nonnegative for positive model and evidence, and the canonical threshold is positive. Cosmologists deriving the Planck H_0 from the phi-ladder cite this bundle. The definition is a pure structure instance wiring three 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
The module derives a structural identification of the Planck Hubble constant $H_0 = 67.4,\mathrm{km/s/Mpc}$ inside Recognition Science: $H_0 = \varphi^k / \tau_{\mathrm{universe}}$ with $\tau_{\mathrm{universe}} = 13.8,\mathrm{Gyr}$, evaluated at a Planck rung near $\varphi^{67}$. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on model/evidence pairs used in that derivation. It inherits nonnegativity from the global J-cost of recognition events: ObserverForcing records that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states. The certificate structure simply names the three properties the Hubble argument needs: diagonal vanishing, nonnegativity, and a positive canonical threshold.
proof idea
One-line structure instance. The three fields of HubblePrecise2Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra algebra is performed at this site; the definition only packages those proofs.
why it matters
Gives a single named inhabitant of the Hubble-precise certificate so downstream cosmology lemmas can assume diagonal vanishing, cost nonnegativity, and a positive threshold without re-proving each fact. It sits inside the structural (sorry-free) derivation of $H_0$ from the phi-ladder and the universe age, consistent with the RS constants and the forcing chain that fixes $\varphi$ (T6) and the J-cost (T5). No used-by edges are recorded yet; the sibling cert_inhabited is the natural consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.