HubbleParameterILG
plain-language theorem explainer
The definition supplies the ILG-corrected Hubble parameter by scaling an early-time input with the locked recognition lag. Cosmologists addressing the Hubble tension would cite this scaling when reconciling CMB-derived values with local measurements. The definition is a direct multiplication that inserts the constant C_lag = phi^{-5} derived from the recognition framework.
Claim. $H_ {phys} = H_{early} (1 + C_{lag})$ where $C_{lag} = phi^{-5}$ and $phi$ is the self-similar fixed point.
background
The module formalizes Induced Light Gravity corrections to the FRW metric and demonstrates how the recognition lag resolves the Hubble tension. The upstream cLagLock definition supplies the canonical value $C_{lock} = phi^{-5}$. The CPM.LawOfExistence.Constants structure bundles related recognition constants while the various Resolution structures record status of related conjectures.
proof idea
This definition is a one-line wrapper that multiplies the input H_early by (1 + cLagLock) from the Constants module.
why it matters
This definition is used by the theorem hubble_resolution_converges to demonstrate numerical agreement between scaled CMB and local values. It supplies the explicit ILG correction step inside the cosmology module and connects to the phi-ladder constants where phi^{-5} appears as hbar in native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.