hubble_resolution_converges
plain-language theorem explainer
The theorem shows that the ILG-corrected Hubble parameter applied to the Planck CMB value of 67.4 km/s/Mpc yields a late-time value within 0.5 of the SH0ES local measurement 73.5. Cosmologists studying the Hubble tension would cite it for a quantitative match inside the Recognition Science setting. The proof bounds phi^{-5} between 0.09 and 0.091 using the golden-ratio recurrence and then verifies the absolute-difference inequality by direct comparison and gcongr.
Claim. Let $H_early = 67.4$ and $H_{late,obs} = 73.5$. Then $|H_early · (1 + φ^{-5}) - H_{late,obs}| < 0.5$, where $φ$ denotes the golden ratio satisfying $φ^2 = φ + 1$.
background
The module formalizes Induced Light Gravity corrections to the FRW metric and shows how the recognition lag constant resolves the Hubble tension. HubbleParameterILG is defined as the early-time Hubble value multiplied by (1 + cLagLock). cLagLock is the locked constant φ^{-5}. Upstream lemmas supply the necessary identities: phi_sq_eq states φ² = φ + 1, while phi_lt_onePointSixTwo gives the tight bound φ < 1.62.
proof idea
The tactic proof unfolds HubbleParameterILG, simplifies with cLagLock, then establishes the interval 0.09 < φ^{-5} < 0.091 by deriving φ^5 = 5φ + 3 from repeated application of phi_sq_eq and phi_lt_onePointSixTwo. It finishes by rewriting the target inequality as abs_lt and discharging both sides with gcongr plus norm_num comparisons against the explicit numerical bounds.
why it matters
This declaration supplies the quantitative resolution of the Hubble tension inside the ILG framework, matching the prediction H_late = H_early · (1 + φ^{-5}) to the observed values. It directly implements the C_lag correction described in the module doc-comment and rests on the Recognition Science constants c = 1 and ħ = φ^{-5}. No downstream theorems are listed, leaving open whether the same lag factor appears in other cosmological observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.