Cosmology Hubble Tension Hubble Ratio Match

The Hubble ratio match

The Hubble tension is the observed discrepancy between two ways of measuring the universe's expansion rate. Early-universe measurements, based on the cosmic microwave background, give a rate near 67.4 kilometers per second per megaparsec. Late-universe measurements, using local distance ladders, give a rate near 73.0. The ratio of these two numbers is about 1.0837, and the disagreement between the two methods is one of the open problems in modern cosmology.

In Recognition Science, the framework's library contains a ledger, a discrete record of events, whose geometry has 12 edges plus one time dimension. The framework models the Hubble ratio as the ratio of the dynamic ledger (12 edges plus time) to the static ledger (12 edges), which is exactly 13/12, or 1.0833. The declaration hubble_ratio_match is a theorem in the machine-checked library of formal theorems. It proves that the predicted late-universe rate, computed as the early rate times 13/12, differs from the measured late rate by less than 0.05 percent. The measured values used are 73.04 for the late rate and 67.4 for the early rate, both defined as constants in the library.

The theorem does not prove that the Hubble tension is resolved. It proves a numerical agreement: the ratio 13/12 matches the observed ratio to within 0.05 percent. The framework's library also contains a related theorem about dark energy density, but that is a separate claim. The hubble_ratio_match theorem itself only establishes the arithmetic fact about the ratio. It does not explain why the early and late measurements differ, nor does it derive the measured values from first principles. The measured values are inputs, not outputs.

What the theorem does establish is that a simple rational ratio, derived from the ledger geometry, lands within a narrow band of the observed ratio. The prediction is 1.0833; the observation is about 1.0837. The match is 0.03 percent. This is a precise, checkable statement: the absolute difference between the predicted and measured late rates, divided by the measured rate, is less than 0.0005. The library proves this inequality with exact arithmetic, not with statistical fitting. The framework's contribution is the ratio itself, not the measurements.

The honest reading is that the framework offers a geometric story for why the ratio might be 13/12, and the theorem confirms that this ratio sits close to the observed one. It does not claim to resolve the tension, to explain the physics of the discrepancy, or to predict the Hubble constant from scratch. The theorem is a consistency check, not a derivation of cosmology. The measured values remain external inputs, and the framework's claim is that its geometry produces a ratio that matches them closely.

/-- The Hubble Ratio matches observation to within 0.05%.

    pred = 67.4 * (13/12) = 73.0166...
    obs  = 73.04
    |pred - obs| / obs = |73.0166 - 73.04| / 73.04 = 0.00032 < 0.0005 ✓

    This is now PROVEN, not axiomatized. -/
theorem hubble_ratio_match :
    abs (H_late_pred - H_late_exp) / H_late_exp < 0.0005 := by
  simp only [H_late_pred, H_late_exp, H_early_exp, hubble_ratio_topo]
  norm_num

/-- The Hubble Ratio matches observation to within 0.05%.

    pred = 67.4 * (13/12) = 73.0166...
    obs  = 73.04
    |pred - obs| / obs = |73.0166 - 73.04| / 73.04 = 0.00032 < 0.0005 ✓

    This is now PROVEN, not axiomatized. -/
theorem hubble_ratio_match :
    abs (H_late_pred - H_late_exp) / H_late_exp < 0.0005 := by
  simp only [H_late_pred, H_late_exp, H_early_exp, hubble_ratio_topo]
  norm_num

/-- The Hubble Ratio 13/12. -/
def hubble_ratio_topo : ℚ := 13 / 12

/-- The Hubble ratio 13/12 derives from ledger edge count (12) + time dimension (1). -/
theorem hubble_ratio_from_ledger :
    hubble_ratio_topo = (12 + 1) / 12 := by
  simp only [hubble_ratio_topo]
  norm_num

def H_late_exp : ℝ := 73.04

def H_early_exp : ℝ := 67.4

def H_late_exp : ℝ := 73.04

def H_early_exp : ℝ := 67.4

What this page does not claim

This theorem does not resolve the Hubble tension or explain why the early and late measurements differ. This theorem does not derive the measured Hubble rates from first principles; the values 67.4 and 73.04 are external inputs. This theorem does not make any claim about the dark energy density, which is a separate theorem in the same module.

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/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: