Cosmology Early Universe Alpha Over Pi Gt

A certified bracket on dark energy

The dark-energy fraction of the universe, written Ω_Λ, is the share of the cosmic energy budget that drives the accelerated expansion. Planck satellite data from 2018 put it at 0.6889 with an uncertainty of ±0.0056. The Recognition Science framework's cosmology module derives a value of 11/16 − α/π, where α is the measured fine-structure constant, about 1/137. That expression evaluates to roughly 0.6852.

The lemma alpha_over_pi_gt is one half of a certified numeric bracket. It proves, in a machine-checked library of formal theorems, that α/π is greater than 0.002316. Its companion lemma alpha_over_pi_lt proves the same ratio is less than 0.002324. Together they force Ω_Λ to lie strictly between 0.6851 and 0.6852. The bracket is a theorem: the proof is checked by the library's kernel, and it relies on the standard axioms of logic plus the measured value of α.

That narrow window matters because it is testable. Planck's measured value, 0.6889 ± 0.0056, overlaps the derived bracket, though the central values differ by about 0.0037, roughly two-thirds of the measurement's uncertainty. The agreement is not exact, but the derivation uses no fitted parameter for dark energy. The only external input is the fine-structure constant, which enters as a measurement, not as a construction.

What the lemma does not claim is just as important. It does not derive the fine-structure constant itself; that remains an open problem. It does not prove that the dark-energy fraction is exactly 0.6852, only that it lies in the stated interval. And it does not resolve the cosmological constant problem in the sense of explaining why the vacuum energy is small. The framework's account is different: it says the cosmological constant is not the vacuum energy of quantum field theory at all, but a fraction of ledger modes, so the famous 10^120 discrepancy dissolves by redefinition rather than by calculation.

private lemma alpha_over_pi_gt :
    (0.002316 : ℝ) < Constants.ExternalAnchors.alpha_CODATA / Real.pi := by
  have hpi_pos := Real.pi_pos
  have hpi_hi : Real.pi < (3.15 : ℝ) := Real.pi_lt_d2
  have hlit : (0.002316 : ℝ) * 3.15 < Constants.ExternalAnchors.alpha_CODATA := by
    unfold Constants.ExternalAnchors.alpha_CODATA; norm_num
  rw [lt_div_iff₀ hpi_pos]
  nlinarith

/-- A certified numeric bracket on Ω_Λ.

    This module carried no numeric bound at all before 2026-07-27, only positivity and
    subunitarity, and that absence is precisely why the `alphaLock` substitution
    survived: nothing here could be placed against a measurement, so a value 0.06 away
    from Planck violated nothing that was stated. -/
theorem omega_lambda_bracket :
    (0.6851 : ℝ) < omega_lambda ∧ omega_lambda < 0.6852 := by
  unfold omega_lambda
  have h1 := alpha_over_pi_lt
  have h2 := alpha_over_pi_gt
  constructor <;> linarith

/-- Ω_Λ = 11/16 − α/π, with α the measured fine-structure constant.

    The value 11/16 = 0.6875 comes from the fraction of ledger modes that are in the
    vacuum (unexcited) state in the 8-tick cycle. That mode count is where the content
    of this prediction lives. The correction −α/π accounts for the small perturbation
    from matter-coupled modes.

    α enters as a measurement and not as a construction. Its value is a free boundary
    datum in RS, and the first-order constructed value is excluded by measurement, so
    the canonical reading is `ExternalAnchors.alpha_CODATA`.
    `Cosmology.OmegaLambdaDerivation` takes the same input and says so explicitly.

    Corrected 2026-07-27. This read `11/16 - alphaLock / π` until then.
    `alphaLock = (1 − 1/φ)/2 ≈ 0.191` is the information-limited-gravity kernel
    exponent, not the fine-structure constant ≈ 0.0073, and its own module header has
    said so since 2026-07-06. The substitution put this observable at 0.6267 against
    Planck's 0.6889 ± 0.0056, more than ten standard deviations out. It was never a
    competing derivation of dark energy; it was the wrong constant in the α slot. The
    excluded expression survives under its own name as
    `Cosmology.PrecisionExposure.omega_lambda_alphaLock`, so the defect cannot return
    silently. -/
noncomputable def omega_lambda : ℝ :=
  11/16 - Constants.ExternalAnchors.alpha_CODATA / Real.pi

What this page does not claim

The fine-structure constant α is derived by the framework; it is only used as a measured input. The dark-energy fraction is exactly 0.6852; the theorem only certifies a strict interval. The cosmological constant problem is resolved by explaining why vacuum energy is small; the framework redefines the observable instead.

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