Cosmology Hubble Tension

The dual metric hypothesis

The Hubble tension is the observed discrepancy between two measurements of the universe's expansion rate, the Hubble constant. Measurements of the early universe, using the cosmic microwave background, yield a rate near 67.4 kilometers per second per megaparsec. Measurements of the late universe, using local distance ladders like Cepheid variables, yield a rate near 73.0. The difference, about 8 percent, is a standing problem in cosmology because both methods claim high precision.

Recognition Science, a framework that derives physical structure from a discrete record of events called a ledger, offers a specific ratio. The framework models the universe's geometry as a ledger with 12 edges plus one time dimension, against a static ledger with 12 edges. The hypothesis states that the ratio of the late to early Hubble constants equals (12 + 1)/12, or 13/12 ≈ 1.0833. The observed ratio, 73.04/67.4, is about 1.0837. The match is within 0.03 percent, and the framework's machine-checked library of formal theorems proves the prediction falls within 0.05 percent of the measured value.

The same module derives the dark energy density, Ω_Λ, from the fractional volume of a passive field geometry relative to the vertex basis of a cube (Q₃). The base value is 11/16 = 0.6875, with a correction term α/π ≈ 0.0023. The prediction is 0.6852, and the Planck measurement is 0.6847 ± 0.0073. The framework proves this prediction lies within one standard deviation of the measurement.

These results are empirical checks, not forced theorems. The framework's contribution is a geometric origin for the ratio, not a derivation of the Hubble constant itself. The ratio 13/12 is a definitional choice, and the match to observation is a measured agreement. The dark energy correction uses the fine-structure constant as an external anchor, not as a derived quantity.

What this establishes is a candidate explanation for the Hubble tension's size. If the ledger's edge count sets the expansion ratio, the tension is not a measurement error but a geometric signature. The framework's library proves the arithmetic consistency of this signature, and the agreement with current data is within the stated tolerances.

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

def H_late_exp : ℝ := 73.04

/-- 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 Dark Energy base 11/16 derives from passive edges (11) over 2*vertices (16). -/
theorem dark_energy_from_geometry :
    dark_energy_base = 11 / (2 * 8) := by
  simp only [dark_energy_base]
  norm_num

/-- Dark Energy matches observation to within 1 sigma.

    Omega_L_pred = 11/16 - α_CODATA/π ≈ 0.6875 - 0.00232 ≈ 0.6852
    Omega_L_exp = 0.6847
    Omega_L_err = 0.0073
    |0.6852 - 0.6847| ≈ 0.0005 < 0.0073 ✓

    Proof: From alpha/pi bounds, we establish the match. -/
theorem dark_energy_match :
    abs (Omega_L_pred - Omega_L_exp) < Omega_L_err := by
  have h_ap := alpha_over_pi_bounds
  simp only [Omega_L_pred, Omega_L_exp, Omega_L_err, dark_energy_base]
  -- Omega_L_pred = 11/16 - α_CODATA/π
  -- With α/π ∈ (0.0023, 0.0024):
  -- Omega_L_pred ∈ (0.6875 - 0.0024, 0.6875 - 0.0023) = (0.6851, 0.6852)
  -- |Omega_L_pred - 0.6847| ≤ max(|0.6851 - 0.6847|, |0.6852 - 0.6847|)
  --                        = max(0.0004, 0.0005) = 0.0005 < 0.0073 ✓
  have h_pred_lower :
      (0.6851 : ℝ) <
        (11 : ℝ) / 16 - Constants.ExternalAnchors.alpha_CODATA / Real.pi := by
    have h1 : Constants.ExternalAnchors.alpha_CODATA / Real.pi < (0.0024 : ℝ) := h_ap.2
    have h2 : (11 : ℝ) / 16 = (0.6875 : ℝ) := by norm_num
    linarith
  have h_pred_upper :
      (11 : ℝ) / 16 - Constants.ExternalAnchors.alpha_CODATA / Real.pi <
        (0.6852 : ℝ) := by
    have h1 : (0.0023 : ℝ) < Constants.ExternalAnchors.alpha_CODATA / Real.pi := h_ap.1
    have h2 : (11 : ℝ) / 16 = (0.6875 : ℝ) := by norm_num
    linarith
  rw [abs_lt]
  constructor <;> linarith

What this page does not claim

The Hubble constant itself is not derived, only the ratio between early and late measurements. The fine-structure constant is used as an external anchor, not derived within the framework. The framework does not claim the Hubble tension is resolved, only that a geometric ratio matches current data.

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: