Cosmology Hubble Tension Bound Empirical Central

The empirical central value

The Hubble constant H₀ sets the present-day expansion rate of the universe. Two families of measurements disagree about its value. Late-time measurements, such as SH0ES and Pantheon+, use nearby distance ladders and give a higher rate. Early-time measurements, such as the Planck satellite's study of the cosmic microwave background, infer the rate from the early universe and give a lower one. The disagreement is persistent and sits at roughly the 5σ level, meaning it is far larger than the reported errors of either method would suggest. This is the Hubble tension.

Within the Recognition Science framework, the ratio of the late-time to early-time H₀ values is the quantity of interest. The framework's model predicts this ratio should fall in a narrow band from 1.075 to 1.091. The declaration empiricalCentral records the value 1.083, which is the central empirical estimate of this ratio from the SH0ES and Planck data. The framework's library proves this value lies strictly inside the predicted band. That proof is a formal theorem, checked by a machine, with no unproved assumptions: it establishes only that 1.075 is less than 1.083 and 1.083 is less than 1.091.

The declaration does not claim that the empirical value 1.083 was derived from first principles. It is a measurement, not a prediction. The band (1.075, 1.091) is the prediction; the value 1.083 is the observed fact that happens to fall inside it. The framework also defines a falsifier predicate: a future joint measurement that places the ratio below 1.059 (the lower bound minus the band width) would falsify the framework's explanation. The consistency and falsification conditions are mutually exclusive, a fact also proved in the library. The declaration's role is to fix the empirical anchor against which the prediction is checked, not to prove the prediction itself.

The practical consequence is a clear, checkable target. The framework's account of the Hubble tension survives only as long as future measurements keep the late-to-early ratio inside (1.075, 1.091). The empirical central value 1.083 is the current best estimate, and it sits comfortably inside. What the framework offers is not a new measurement but a specific, falsifiable band that the next generation of cosmology data will either support or rule out.

/-- The empirical SH0ES/Planck central value, well inside the band. -/
def empiricalCentral : ℝ := 1.083

/-- The empirical central value sits strictly inside the band. -/
theorem empiricalCentral_in_band :
    hubbleRatioLower < empiricalCentral ∧ empiricalCentral < hubbleRatioUpper := by
  unfold hubbleRatioLower hubbleRatioUpper empiricalCentral
  refine ⟨?lo, ?hi⟩ <;> norm_num

/-- Consistency and falsification are mutually exclusive. -/
theorem consistency_excludes_falsification {h0 : ℝ} :
    ¬ (IsConsistentWithRS h0 ∧ IsFalsifier h0) := by
  rintro ⟨⟨h_lo, _⟩, h_excl⟩
  unfold IsFalsifier at h_excl
  unfold hubbleRatioLower hubbleRatioUpper at *
  linarith

What this page does not claim

The value 1.083 is a measurement, not a prediction derived from the framework's axioms. The framework does not predict the absolute value of the Hubble constant, only the ratio between the two measurement families. The band (1.075, 1.091) is not a statement about the true value of the ratio, only about where the framework's model says it should be found.

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/Cosmology/HubbleTensionBound.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: