hubbleBand_contains_empirical
plain-language theorem explainer
The theorem confirms that the empirical Hubble tension ratio 1.083 lies inside the open interval (1.075, 1.091) produced by the Z-aging model. Cosmologists examining the late-versus-early H_0 discrepancy would cite the containment when checking consistency of the Recognition Science prediction against SH0ES and Planck data. The proof is a one-line tactic wrapper that unfolds the band definition and resolves the two inequalities by numerical normalization.
Claim. The empirical Hubble ratio 1.083 satisfies $1.075 < 1.083 < 1.091$, where the bounds are supplied by the Hubble ratio band derived from the Z-aging amplitude formula.
background
The module constructs a pipeline that resolves the Hubble tension via Z-complexity aging of the recognition field across cosmic time. The Hubble ratio band is the concrete pair (1.075, 1.091) obtained from the amplitude expression r_H = 1 + (1/φ^5) · c with φ^5 in (11.05, 11.1) and normaliser c ≈ 0.91. Five Z-aging channels (matter density, radiation density, dark energy, curvature, scalar perturbation) each contribute a rung on the φ-ladder inside the five-dimensional configuration space.
proof idea
The proof unfolds the definition of the Hubble ratio band to expose the pair (1.075, 1.091). It then splits the conjunction via constructor and dispatches both strict inequalities with norm_num.
why it matters
This containment fact is assembled into hubbleTensionCert, which packages the full certification that the Z-aging pipeline accounts for the observed tension. The module states that Recognition Science predicts the late/early H_0 ratio lies in (1.075, 1.091) and contains the empirical value 1.083. The result therefore closes the numerical verification step that links the φ-ladder corrections to the measured discrepancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.