Encyclopedia Cosmology Cosmology Hubble Tension Alpha Over Pi Bounds

ARTICLE 4 claims 3 theorems 1 model

Cosmology Hubble Tension Alpha Over Pi Bounds

A machine-checked theorem pins a small correction term between 0.0023 and 0.0024, anchoring a dark energy prediction.

Verify this page

The alpha over pi bound

The Hubble tension is the observed mismatch between two ways of measuring how fast the universe expands. Early universe observations, based on the cosmic microwave background, give a rate near 67.4 kilometers per second per megaparsec. Late universe observations, using nearby supernovae and Cepheid variable stars, give a rate near 73.0. The ratio of these two numbers is about 1.0837, and the discrepancy has resisted conventional explanation.

Within the Recognition Science framework, a specific hypothesis addresses this ratio. The framework models the universe as a discrete ledger, a record of events with a fixed geometric structure. The hypothesis proposes that the ratio of late to early expansion equals 13/12, which is 1.0833. This number comes from counting 12 edges of a cube plus one time dimension, divided by the 12 edges alone. The prediction lands within 0.05 percent of the observed ratio.

For the dark energy density, the framework derives a value from geometry. The base term is 11/16, or 0.6875, which comes from a ratio of vertices in a cube. A correction term subtracts alpha divided by pi, where alpha is the fine-structure constant, a dimensionless number near 1/137. The theorem alpha_over_pi_bounds proves that this correction term lies strictly between 0.0023 and 0.0024. This is a formal, machine-checked result in the framework's library of theorems.

Subtracting this correction from the base gives a predicted dark energy density of 0.6852. The measured value from the Planck satellite is 0.6847 with an uncertainty of 0.0073. The difference between prediction and measurement is smaller than the stated uncertainty, so the framework's prediction falls within one sigma of the observation. The theorem dark_energy_match formalizes this agreement.

The alpha_over_pi_bounds theorem does not derive the value of alpha itself. The fine-structure constant enters as an external anchor, a measured input from CODATA, not as a derived quantity. The theorem only bounds the ratio alpha over pi, and that bound depends on the measured value of alpha. The framework does not explain why alpha has the value it does; that remains an open question. The theorem also does not prove that the dark energy prediction is correct, only that it is consistent with current measurements within the stated uncertainty.

THEOREM alpha_over_pi_bounds · IndisputableMonolith/Cosmology/HubbleTension.lean
alpha_over_pi_bounds · IndisputableMonolith/Cosmology/HubbleTension.lean:117 
/-- Bounds on alpha/pi needed for dark energy proof.

    With measured α = 7.2973525643e-3 and pi ∈ (3.14, 3.15):
    α/π ∈ (0.00729/3.15, 0.00731/3.14) ⊂ (0.0023, 0.0024). -/
theorem alpha_over_pi_bounds :
    (0.0023 : ℝ) < Constants.ExternalAnchors.alpha_CODATA / Real.pi ∧
      Constants.ExternalAnchors.alpha_CODATA / Real.pi < (0.0024 : ℝ) := by
  have h_alpha_lower : (0.00729 : ℝ) < Constants.ExternalAnchors.alpha_CODATA := by
    unfold Constants.ExternalAnchors.alpha_CODATA; norm_num
  have h_alpha_upper : Constants.ExternalAnchors.alpha_CODATA < (0.00731 : ℝ) := by
    unfold Constants.ExternalAnchors.alpha_CODATA; norm_num
  have h_pi_lower : (3.14 : ℝ) < Real.pi := by linarith [Real.pi_gt_d6]
  have h_pi_upper : Real.pi < (3.15 : ℝ) := by linarith [Real.pi_lt_d6]
  have h_alpha_pos : 0 < Constants.ExternalAnchors.alpha_CODATA :=
    lt_trans (by norm_num) h_alpha_lower
  have h_pi_pos : 0 < Real.pi := Real.pi_pos
  constructor
  · -- Lower bound: 0.0023 < α/π
    calc (0.0023 : ℝ) < 0.00729 / 3.15 := by norm_num
      _ < Constants.ExternalAnchors.alpha_CODATA / 3.15 := by
          apply div_lt_div_of_pos_right h_alpha_lower
          norm_num
      _ < Constants.ExternalAnchors.alpha_CODATA / Real.pi := by
          apply div_lt_div_of_pos_left h_alpha_pos h_pi_pos
          exact h_pi_upper
  · -- Upper bound: α/π < 0.0024
    calc Constants.ExternalAnchors.alpha_CODATA / Real.pi
          < Constants.ExternalAnchors.alpha_CODATA / 3.14 := by
          apply div_lt_div_of_pos_left h_alpha_pos (by norm_num) h_pi_lower
      _ < 0.00731 / 3.14 := by
          apply div_lt_div_of_pos_right h_alpha_upper
          norm_num
      _ < (0.0024 : ℝ) := by norm_num
MODEL hubble_ratio_topo · IndisputableMonolith/Cosmology/HubbleTension.lean
hubble_ratio_topo · IndisputableMonolith/Cosmology/HubbleTension.lean:55 
/-- The Hubble Ratio 13/12. -/
def hubble_ratio_topo : ℚ := 13 / 12
THEOREM hubble_ratio_match · IndisputableMonolith/Cosmology/HubbleTension.lean
hubble_ratio_match · IndisputableMonolith/Cosmology/HubbleTension.lean:99 
/-- 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
THEOREM dark_energy_match · IndisputableMonolith/Cosmology/HubbleTension.lean
dark_energy_match · IndisputableMonolith/Cosmology/HubbleTension.lean:151 
/-- 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 framework derives the value of the fine-structure constant alpha. The dark energy prediction is proven correct, only consistent with current data. The 13/12 ratio is proven to be the only possible explanation for the Hubble tension.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND