Gravity Hubble Tension Delta H0 Positive

The positive shift

The Hubble constant H₀ measures how fast the universe expands today, in kilometers per second per megaparsec. Astronomers have two main ways to measure it. One looks at the early universe, imprinted in the cosmic microwave background, and finds about 68.8. The other looks at nearby galaxies and finds about 71.8. The gap of 3.0 is the Hubble tension: a disagreement too large to be random noise, about 4 to 5 standard deviations under the standard cosmological model.

In Recognition Science, the resolution comes from a modified weighting of late-time sources. The framework's ILG kernel shifts the late-time H₀ upward without touching early-universe physics. The declaration delta_H0_positive is a formal theorem in the machine-checked library of formal theorems. It proves that the shift is positive: 0 < delta_H0, where delta_H0 is defined as H0_ILG minus H0_CMB. A companion theorem pins the value: delta_H0 = 3.0 exactly, by unfolding the two definitions and simplifying.

The positive shift is not an isolated number. The same library proves that the tension metric drops from about 4σ to about 1σ, meaning the discrepancy becomes statistically unremarkable. The sound horizon, a ruler from the early universe, is preserved exactly: the framework defines sound_horizon_preserved as the statement that for any positive r_d from ΛCDM, there exists an r_d from ILG equal to it. The proof is trivial by reflexivity, but the point is structural: the ILG weight tends to 1 at early times, so the early-universe ruler is untouched.

What the declaration does not claim is as important as what it proves. It does not claim that the ILG kernel is the true physical mechanism; that would require observational confirmation beyond the formal framework. It does not claim that the shift is large in absolute terms; 3.0 km/s/Mpc is a modest adjustment. It does not claim that the tension is fully resolved for all measurements; the framework's own numbers are predictions, not measurements. The theorem is a logical statement about definitions, not an empirical result.

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

theorem delta_H0_value : delta_H0 = 3.0 := by
  unfold delta_H0 H0_ILG H0_CMB; 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

theorem sound_horizon_preservation : sound_horizon_preserved :=
  fun r => fun _ => ⟨r, rfl⟩

What this page does not claim

The ILG kernel is the true physical mechanism for the Hubble tension. The shift of 3.0 km/s/Mpc is large in absolute terms. The tension is fully resolved for all measurements, not just the framework's own numbers.

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: