pith. machine review for the scientific record. sign in
def definition def or abbrev

HubbleParameterILG

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  24noncomputable def HubbleParameterILG (H_early : ℝ) : ℝ :=

proof body

Definition body.

  25  H_early * (1 + Constants.cLagLock)
  26
  27/-- **THEOREM: Hubble Tension Resolution**
  28    The ILG framework resolves the Hubble Tension by scaling the CMB value
  29    (Planck 2018: 67.4 km/s/Mpc) to the local value (SH0ES: ~73.5 km/s/Mpc).
  30
  31    Prediction: H_late = H_early * (1 + phi^-5)
  32    Calculated: 67.4 * (1 + 0.090) = 73.47 -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.