omega_lambda_passes_1sigma
plain-language theorem explainer
The RS dark-energy density Ω_Λ = 11/16 − α/π lies inside the 1σ band of the preregistered 2022 measurement (central value 0.6847, σ = 0.0073). Cosmologists checking the Hubble/Ω_Λ preregistration suite would cite it. The proof freezes the prediction, applies α/π bounds, drops the absolute value by positivity, and finishes by linear arithmetic.
Claim. The Recognition Science prediction $\Omega_\Lambda = 11/16 - \alpha/\pi$ satisfies $|\Omega_\Lambda - 0.6847| < 0.0073$, i.e. it lies within one standard deviation of the preregistered $\Omega_\Lambda$ measurement.
background
This module is the preregistered test suite for two Hubble-sector claims: a relative-error check on the Hubble ratio and a 1σ check on Ω_Λ. The predicate within_sigma is the standard absolute-error band |prediction − central| < σ.
The RS formula is Ω_Λ = 11/16 − α/π. Upstream, EarlyUniverse and OmegaLambdaDerivation record that 11/16 = 0.6875 is the vacuum (unexcited) ledger-mode fraction on the eight-tick cycle, while −α/π is the small EM correction from matter-coupled modes. The fine-structure constant α is the RS/CODATA anchor used throughout the cosmology modules; it is kept opaque in the numeric test so only the measurement payload is unfolded.
The key prior bound is alpha_over_pi_bounds: with α ∈ (0.00729, 0.00731) and π ∈ (3.14, 3.15) one has α/π ∈ (0.0023, 0.0024). That interval pins the prediction to a narrow window just above the measured central value.
proof idea
Unfold within_sigma and simplify only the measurement record, obtaining the concrete goal |11/16 − α/π − 0.6847| < 0.0073.
Invoke alpha_over_pi_bounds. Rewrite 11/16 = 0.6875 and use linear arithmetic on the two sides of the α/π interval to get the prediction sandwich 0.6851 < 11/16 − α/π < 0.6852.
The lower bound already exceeds 0.6847, so the difference is positive and the absolute value drops (abs_of_pos). The upper bound then yields difference < 0.0073 by another linarith step, which is exactly the 1σ goal.
why it matters
This is a leaf verification theorem in the preregistered Hubble suite: it certifies that the closed-form RS dark-energy fraction matches the 2022 Ω_Λ measurement inside 1σ, with no free cosmological fit parameters beyond the already-fixed α.
Framework landmarks in play are the eight-tick octave (T7), which supplies the vacuum-mode fraction 11/16, and the fine-structure constant α (forced in the RS constant ladder and constrained to the CODATA band). The correction −α/π is the same EM perturbation used in the cosmological-constant and phase-saturation derivations.
No downstream theorems currently depend on it (used_by is empty); its role is audit-facing: a machine-checked pass/fail gate for the Ω_Λ preregistration claim alongside the sibling Hubble-ratio relative-error test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.