Cosmology Hubble Tension Dark Energy Base Value

The base value

In the Recognition Science framework, recognition (a discrete record of events) leads to a specific geometric model of the universe. From that model, the framework derives a base value for the dark energy density parameter, which cosmologists write as ΩΛ. The declaration dark_energy_base_value is a machine-checked theorem stating that this base value equals the rational number 11/16, or 0.6875 in decimal form. The proof is a simple computation: the framework defines the base value as 11 divided by 16, and the theorem confirms the arithmetic.

The number 11/16 comes from the geometry of a cube. The framework models the universe's passive field geometry using the vertices of a three-dimensional cube, which has 8 vertices. It assigns the number 11 to the passive field's contribution. The base value is then half of 11 divided by 8, written as 11/(2 × 8), which simplifies to 11/16. This is not an empirical measurement; it is a definitional choice within the model, though the framework proves the arithmetic that connects the geometric picture to the rational number.

The full prediction for ΩΛ is not just 11/16. The framework subtracts a small correction term, α/π, where α is the fine-structure constant. This correction is approximately 0.0023, bringing the predicted value to about 0.6852. The framework's library proves that this predicted value falls within the error bar of the Planck satellite's measured value of 0.6847 ± 0.0073. That agreement is a theorem in the library, but it is an empirical check against observation, not a derivation of the measured value itself.

What the declaration does not claim is important. It does not claim that dark energy is understood or that the framework's model is confirmed. It does not claim that the fine-structure constant is derived; the correction term uses the measured value of α as an external input. The theorem only establishes the arithmetic fact that the defined base value equals 0.6875, and the associated theorem shows that the final prediction matches the Planck measurement within one standard deviation. The framework's geometric story about dark energy remains a hypothesis, not a settled physical theory.

/-- Helper: 11/16 numerical value. -/
theorem dark_energy_base_value :
    (dark_energy_base : ℝ) = 0.6875 := by
  simp only [dark_energy_base]
  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 declaration does not claim that the fine-structure constant α is derived; it uses the measured value as an external input. The theorem does not claim that the framework's dark energy model is physically confirmed, only that its arithmetic prediction matches one measurement. The base value 11/16 is not claimed to be a measured quantity; it is a definitional choice within the model.

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: