H_late_pred_value
plain-language theorem explainer
The theorem shows that the predicted late-universe Hubble constant lies strictly between 73.01 and 73.02. Cosmologists resolving the Hubble tension would cite this to confirm that the topological ratio 13/12 applied to the early value 67.4 reproduces the observed late measurement to 0.03 percent. The proof is a direct algebraic reduction that substitutes the defining expressions and evaluates the inequality numerically.
Claim. The predicted late Hubble constant $H_ {late}^{pred}$ satisfies $73.01 < H_{late}^{pred} < 73.02$, where $H_{late}^{pred} = 67.4 times (13/12)$.
background
The module formalizes the Hubble tension via the Dual Metric Hypothesis, which sets the late-to-early ratio equal to 13/12. This ratio encodes the dynamic ledger (12 edges plus one time dimension) versus the static ledger (12 edges). The early value is fixed at 67.4 and the predicted late value is their product. Upstream definitions fix the early expansion rate at 67.4 and the topological ratio at the rational 13/12.
proof idea
The proof is a term-mode reduction that applies simp to unfold the predicted late value, the early value, and the topological ratio, then invokes norm_num to discharge the numerical bounds.
why it matters
This supplies the concrete bound used by the downstream theorem H_late_precision_bounds, which certifies the 0.03 percent match. It realizes the T13 claim in the module documentation on the Hubble Tension and Dark Energy, where the dual metric hypothesis is introduced. In the Recognition framework the result connects simplicial ledger geometry to cosmological observables through the ratio 13/12.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.