cert_inhabited
plain-language theorem explainer
The certificate package for the precise Hubble-constant match from J-cost is inhabited: diagonal vanishing, nonnegativity, and a positive canonical threshold all hold simultaneously. Cosmologists tying RS H_0 = φ^k/τ_universe to the Planck 67.4 km/s/Mpc figure cite this existence fact. The proof is a one-line term witness supplying the concrete certificate.
Claim. There exists a certificate asserting three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$), the domain cost is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
This module is a structural (zero-sorry) derivation of the precise Hubble constant from the phi-ladder. In RS units one writes $H_0=\phi^k/\tau_{\mathrm{universe}}$ with $\tau_{\mathrm{universe}}=13.8,\mathrm{Gyr}$, matching the Planck value $67.4,\mathrm{km/s/Mpc}$ at a Planck-scale rung near $\phi^{67}$.
The certificate structure packages three elementary properties of the domain cost (the local J-cost specialization used here): it is zero when the two arguments coincide and nonzero, it is nonnegative on the positive orthant, and the canonical threshold against which the cost is compared is positive. Those three props are exactly the fields of the certificate.
Upstream, the structure itself is the only dependency; the concrete witness cert (a sibling) already fills the three fields from the corresponding lemmas on domain cost and the threshold.
proof idea
One-line term proof. Nonemptiness of the certificate type is witnessed by the already-constructed concrete certificate value, introduced via the anonymous constructor. No tactics, no further lemmas.
why it matters
Closes the existence side of the structural Hubble-precise package in the Cosmology layer. The module status line marks the whole development as a structural theorem (0 sorry, 0 axiom) linking $H_0$ to a pure phi-ladder ratio against cosmic age. No downstream consumers are wired yet; the inhabited certificate is the natural handle for any later theorem that needs the three cost/threshold facts as a single hypothesis. Framework landmarks in play are the phi fixed point (T6) and the J-cost uniqueness (T5) that underwrite domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.