HubblePrecise2Cert
plain-language theorem explainer
Certificate structure bundling three properties of the domain cost and canonical threshold used in the RS derivation of the precise Hubble constant from the phi-ladder. Cosmology proofs that inhabit or discharge the H_0 structural claim cite it. Pure structure definition: three Prop fields, no proof body.
Claim. A Hubble-precise certificate is a triple of properties: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative on positive arguments, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
The module derives the Planck value $H_0=67.4,\mathrm{km/s/Mpc}$ as a structural identity $H_0=\varphi^k/\tau_{\mathrm{universe}}$ with $\tau_{\mathrm{universe}}=13.8,\mathrm{Gyr}$, evaluated on the phi-ladder at the Planck rung. Status is structural theorem: zero sorry, zero axiom.
Domain cost is the local cost functional on mass/energy (or scale) pairs that the module uses in place of raw $J$-cost; the certificate demands it vanish when the two arguments coincide and stay nonnegative off the diagonal for positive inputs. Canonical threshold is the positive cutoff against which that cost is compared when fixing the Hubble scale.
Upstream, nonnegativity of recognition-event cost ($0\le e.\mathrm{cost}$) is already forced by $J$-cost nonnegativity on positive states in ObserverForcing; the certificate reuses that pattern at the cosmology layer.
proof idea
No proof body: this is a structure declaration. The three fields are bare propositions (diagonal vanishing of domain cost, nonnegativity of domain cost on positive pairs, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface that the module's concrete certificate and its Nonempty witness discharge. Downstream cert assembles the three sibling lemmas into one inhabitant; cert_inhabited then records Nonempty HubblePrecise2Cert, closing the structural claim that the H_0 identity is certified rather than postulated.
In the RS forcing picture this sits under the phi-ladder mass/scale bookkeeping (T6 self-similar fixed point, rung arithmetic) rather than under T5–T8 uniqueness itself: it packages the cost and threshold hypotheses needed so that $H_0=\varphi^k/\tau_{\mathrm{universe}}$ is a theorem about nonnegative cost minima, not a free fit. No open scaffold remains in this module once cert is defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.