Cosmology Bitkernel Shape Forcing Omega Gap Explanation Retired

The retired gap explanation

The cosmological constant is the energy density of empty space, and its measured value from the Planck satellite defines the standard model of cosmology. The Recognition Science framework derives a value for this constant, Ω_Λ = 11/16 − α/π ≈ 0.6852, which sits within 0.66 standard deviations of the Planck central value. The framework also models dark energy through an equation of state, w(z), a function describing how the pressure of dark energy changes with cosmic time. The question was whether this dark-energy model could also explain the small remaining gap between the framework's value and the measured one.

That question is now closed. The theorem omega_gap_explanation_retired proves, in the machine-checked library of formal theorems, that the correction to the cosmological constant from the dark-energy model always moves the effective value downward, away from the Planck measurement, for every allowed amplitude of the model. This is a structural result, not a numerical accident. The theorem also proves that the dark-energy equation of state never drops below −1, meaning the correction can never be positive. Since the shape of the dark-energy model is itself forced by the framework's principles, there is no remaining freedom to flip the direction of the correction. The hypothesis that the framework's dark-energy model explains the gap is therefore retired, not because it was tested and failed, but because it is structurally impossible.

What remains is a sharper prediction. The framework's dark-energy equation of state takes the form w(z) = −1 + δw₀/(1+z), which is exactly the standard CPL parametrization with two parameters, w₀ and wₐ. The theorem proves these parameters lie on a line: wₐ = −(1 + w₀), with w₀ in the range (−1, −0.88). This is a falsifiable prediction. A confirmed measurement of phantom crossing, where w(z) < −1, would falsify the mechanism. A measurement of w₀ above −0.88 would falsify the ceiling. The DESI Y3+ survey, the Roman Space Telescope, and Euclid are the experiments that can test this line.

The honest position is now simple. The bare framework value for the cosmological constant stands on its own, within 0.66 standard deviations of Planck. The dark-energy model is a prediction about the equation of state, not a patch for the cosmological constant. The gap explanation is retired, and the prediction is the line in the (w₀, wₐ) plane.

/-- **RETIREMENT CERTIFICATE.** The "BIT explains the Planck-RS Ω_Λ gap"
hypothesis is structurally dead: under the forced kernel the correction at
any admissible amplitude moves `Ω_Λ_eff` below the bare RS value (certified
quadrature, arc 11), i.e. away from Planck. Bundles the arc-11 findings
with the forced-sign theorem. -/
theorem omega_gap_explanation_retired :
    -- (i) at maximum amplitude the corrected value is below the bare RS value
    omega_lambda_corrected_max_amplitude < CosmologicalConstantDerivation.Omega_Lambda_RS ∧
    -- (ii) and outside Planck 1σ, in the wrong direction
    planck_sigma < |omega_lambda_corrected_max_amplitude - planck_central| ∧
    -- (iii) while the forced kernel pins the deviation sign: w(z) ≥ −1 always
    (∀ dw0 z : ℝ, 0 ≤ dw0 → -1 < z → -1 ≤ w_RS dw0 z) :=
  ⟨max_amplitude_below_bare_interval,
   max_amplitude_outside_one_sigma,
   fun dw0 z h0 hz => no_phantom dw0 z h0 hz⟩

/-- **F1 (sign falsifier): no phantom crossing.** Under the forced kernel
with non-negative amplitude, `w(z) ≥ −1` at every physical redshift. A
confirmed `w < −1` measurement falsifies the BIT mechanism. -/
theorem no_phantom (dw0 z : ℝ) (h0 : 0 ≤ dw0) (hz : -1 < z) :
    -1 ≤ w_RS dw0 z := by
  have h1z : (0 : ℝ) < 1 + z := by linarith
  have : 0 ≤ dw0 / (1 + z) := div_nonneg h0 h1z.le
  unfold w_RS
  linarith

/-- **The forced kernel is exactly CPL** with `w₀ = −1 + δw₀`, `wₐ = −δw₀`. -/
theorem w_RS_is_CPL (dw0 z : ℝ) (hz : -1 < z) :
    w_RS dw0 z = w_CPL (-1 + dw0) (-dw0) z := by
  have h1z : (0 : ℝ) < 1 + z := by linarith
  unfold w_RS w_CPL
  field_simp
  ring

/-- **RS lands on the thawing line** for every amplitude `δw₀`. -/
theorem rs_on_thawing_line (dw0 : ℝ) : OnThawingLine (-1 + dw0) (-dw0) := by
  unfold OnThawingLine
  ring

/-- **The today-value band.** For any positive amplitude up to the
phantom-Carnot ceiling, `w₀ ∈ (−1, −0.88)`. -/
theorem w0_band (dw0 : ℝ) (h0 : 0 < dw0) (hJ : dw0 ≤ Cost.Jcost Constants.phi) :
    -1 < -1 + dw0 ∧ -1 + dw0 < -0.88 := by
  have := jcost_phi_lt_012
  constructor <;> linarith

What this page does not claim

The theorem does not prove the framework's value of Ω_Λ is correct; it only proves the gap explanation is retired. The theorem does not derive the today-amplitude δw₀; that remains an open problem. The theorem does not prove the dark-energy mechanism itself; the BIT mechanism and the single-channel selection are hypotheses.

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