H_late_pred
plain-language theorem explainer
H_late_pred defines the predicted late-universe Hubble constant as the early value 67.4 scaled by the topological ratio 13/12. Cosmologists examining the Hubble tension would cite this expression when checking geometric predictions against late-time observations. The definition is realized as a direct real-number multiplication of the imported early constant and the 13/12 ratio.
Claim. The predicted late Hubble constant is given by $H_ {late}^{pred} = 67.4 × (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 distinction between a dynamic ledger (twelve edges plus one time dimension) and a static ledger (twelve edges). The early Hubble constant is supplied as the real number 67.4. The topological ratio is the rational 13/12.
proof idea
This definition is a one-line wrapper that multiplies H_early_exp by the cast of hubble_ratio_topo to real numbers.
why it matters
H_late_pred supplies the central expression used by H_late_pred_value to bound the numerical interval (73.01, 73.02), by hubble_ratio_match to prove the relative error is less than 0.0005, and by T13Cert to record the geometric origin of the ratio. It therefore anchors the module's claim that the dual metric hypothesis accounts for the observed tension between early and late measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.