HubbleTensionCert
plain-language theorem explainer
Empty certificate carrier whose verification predicate asserts that the Hubble ratio 13/12 and dark-energy base 11/16 are pure ledger geometry, and that both predictions match observation (Hubble to <0.05%, Ω_Λ within 1σ). Cosmologists citing the RS resolution of the H₀ tension use it. Discharge is a one-line conjunction of seven upstream lemmas via simp and refine.
Claim. A certificate type $C$ is verified when all of the following hold: the topological Hubble ratio equals $(12+1)/12$; that ratio lies in $(1.0833, 1.0834)$; $|H_{\mathrm{late}}^{\mathrm{pred}} - H_{\mathrm{late}}^{\mathrm{obs}}|/H_{\mathrm{late}}^{\mathrm{obs}} < 5\cdot 10^{-4}$; the dark-energy base equals $11/(2\cdot 8)$; that base equals $0.6875$ as a real; $\alpha/\pi \in (0.0023, 0.0024)$; and $|\Omega_\Lambda^{\mathrm{pred}} - \Omega_\Lambda^{\mathrm{obs}}| < \sigma_{\Omega_\Lambda}$.
background
Module T13 packages the claim that the Hubble tension and dark-energy density are derived from ledger geometry, not fit. The cube contributes 12 edges and $2^3 = 8$ vertices; one edge is dynamical, leaving 11 passive edges; time supplies the extra unit in the numerator of the Hubble ratio. Thus $H_{\mathrm{late}}/H_{\mathrm{early}} = 13/12$ and the dark-energy base is $11/16$.
The RS prediction is $\Omega_\Lambda = 11/16 - \alpha/\pi$, with $\alpha$ the fine-structure constant from the ledger (not a free fit). Upstream, dark_energy_from_geometry states the base equals $11/(2\cdot 8)$, dark_energy_base_value evaluates it to $0.6875$, and alpha_over_pi_bounds places $\alpha/\pi$ in $(0.0023, 0.0024)$ from CKM-geometry $\alpha$ bounds and standard $\pi$ inequalities. Non-circularity rests on cube combinatorics plus the eight-tick structure only.
proof idea
The structure itself is a unit type (Repr only). The content lives in the simp-normal verified predicate: a seven-way conjunction of geometric identities, numeric bounds, and match inequalities.
verified_any is a one-line wrapper: simp only [verified] then refine with the seven upstream witnesses in order: hubble_ratio_from_ledger, hubble_ratio_bounds, hubble_ratio_match, dark_energy_from_geometry, dark_energy_base_value, alpha_over_pi_bounds, dark_energy_match. No new arithmetic is done at the certificate layer.
why it matters
This is the top-level T13 verification certificate for the RS account of the Hubble tension. Observed $H_0$ early/late ratio $\approx 73.04/67.4 \approx 1.0837$ sits against the geometric $13/12 \approx 1.0833$ (sub-0.05% relative error). Dark energy is likewise fixed as $11/16 - \alpha/\pi$ and matched to Planck within $1\sigma$.
In the forcing chain this sits downstream of the eight-tick octave (T7) and $D=3$ cube geometry (T8): 12 edges, 8 vertices, and the single dynamical edge are not free parameters. The certificate has no further used_by edges in the graph; it is a leaf verification artifact meant to be cited as the closed claim that both $H_0$ tension and $\Omega_\Lambda$ are ledger-derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.