Gravity Hubble Tension Delta H0 Value

The Hubble shift

The Hubble constant H₀ measures how fast the universe is expanding today, in kilometers per second per megaparsec. Different ways of measuring it disagree. Observations of the early universe through the cosmic microwave background give about 68.8, while late-universe measurements from nearby galaxies give higher values, around 73 or 74. This mismatch, known as the Hubble tension, has persisted across many independent experiments and is one of the open problems in cosmology.

Within the Recognition Science framework, a machine-checked library of formal theorems contains a declaration called delta_H0_value. It proves that a proposed shift ΔH₀, defined as the difference between a late-time value of 71.8 and an early-universe value of 68.8, equals exactly 3.0 km/s/Mpc. This is a theorem in the sense that it is a formally verified arithmetic consequence of the definitions chosen. The same library also proves that this shift is positive and that the resulting tension metric, a measure of how many standard deviations separate the two values, drops from roughly 4σ to about 1σ.

What the declaration does not do is prove that the shift is real. The value 71.8 comes from a definition, not from a measurement. The library defines H0_ILG as 71.8 and H0_CMB as 68.8, then proves the arithmetic that follows. Whether 71.8 is the correct late-time value is an empirical question, not a formal one. The theorem delta_H0_value is about the consistency of the framework's chosen numbers, not about the actual expansion rate of the universe.

The framework also includes a definition asserting that the sound horizon, a scale set in the early universe, is preserved under its proposed modification. This is a definitional choice, not a derivation from physical principles. The library proves that if the sound horizon under the framework equals the sound horizon under standard cosmology, then such a value exists. That is a logical tautology, not a physical result.

The practical consequence is modest but real. The framework shows that its proposed late-time shift is internally consistent and reduces the statistical tension between early and late universe measurements. It does not show that this shift exists in nature. The gap between a formally verified arithmetic statement and a confirmed physical measurement is the entire distance between the framework's model and the universe it tries to describe.

theorem delta_H0_value : delta_H0 = 3.0 := by
  unfold delta_H0 H0_ILG H0_CMB; norm_num

theorem delta_H0_positive : 0 < delta_H0 := by
  rw [delta_H0_value]; norm_num

/-- The tension between ILG's H₀ and CMB's H₀ is small. -/
theorem ilg_reduces_tension :
    |H0_ILG - H0_CMB| < 2 * Real.sqrt (H0_ILG_sigma ^ 2 + H0_CMB_sigma ^ 2) := by
  unfold H0_ILG H0_CMB H0_ILG_sigma H0_CMB_sigma
  have h : Real.sqrt (1.2 ^ 2 + 1.1 ^ 2) > 1.5 := by
    rw [show (1.2 : ℝ) ^ 2 + 1.1 ^ 2 = 2.65 from by norm_num]
    rw [show (1.5 : ℝ) = Real.sqrt 2.25 from by
      rw [show (2.25 : ℝ) = 1.5 ^ 2 from by norm_num, Real.sqrt_sq (by norm_num : (0:ℝ) ≤ 1.5)]]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  simp only [show (71.8 : ℝ) - 68.8 = 3 from by norm_num, abs_of_pos (by norm_num : (0:ℝ) < 3)]
  linarith

/-- RS/ILG prediction for late-time H₀ (km/s/Mpc). -/
def H0_ILG : ℝ := 71.8

/-- ILG does not modify the sound horizon r_d because:
    1. ILG modifies the late-time source weighting (z < z_recomb)
    2. The sound horizon is set at z ~ 1100 (pre-recombination)
    3. ILG weight w → 1 for large X = k*tau0/a (early universe has large a/small k)

    Therefore r_d(ILG) = r_d(ΛCDM) identically. -/
def sound_horizon_preserved : Prop :=
  ∀ r_d_lcdm : ℝ, 0 < r_d_lcdm →
    ∃ r_d_ilg : ℝ, r_d_ilg = r_d_lcdm

What this page does not claim

The declaration does not prove that the Hubble tension is resolved in the physical universe. The declaration does not establish that 71.8 km/s/Mpc is the measured value of the Hubble constant. The declaration does not derive the sound horizon preservation from physical laws.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/HubbleTension.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: