Verification Omega Lambda Planck Likelihood

The Planck consistency check

The dark energy density, written ΩΛ, is the fraction of the universe's energy budget that drives its accelerated expansion. The Planck 2018 mission, using the cosmic microwave background, measured this fraction as 0.6889 with an uncertainty of 0.0056. In Recognition Science, a derived prediction for ΩΛ is 11/16 minus α/π, which evaluates to a value between 0.683 and 0.686. The question is whether this theoretical number is compatible with what Planck actually saw.

The verification module answers that question with a formal, machine-checked certificate. It defines the absolute difference between the predicted value and the Planck central value, then proves this residual is smaller than twice the Planck uncertainty. In plain terms, the prediction lands within the two-sigma band of the measurement. The certificate also records that the Planck dataset is currently sensitive to the predicted interval, meaning the comparison is meaningful and not vacuous.

This is a consistency test, not empirical confirmation. The module does not claim the prediction is correct because it agrees with data; it claims the prediction is not ruled out at the two-sigma level. The certificate bundles several facts: the uncertainty is positive, the residual is within tolerance, the interval form holds, and the dataset attachment is active. The final one-statement theorem packages all of these into a single checkable assertion.

The practical consequence is that the framework's prediction for dark energy density survives a direct confrontation with the best available cosmological data. It does not prove the framework's broader claims, but it removes a common observational objection. A reader can now see that the prediction is quantitatively consistent with Planck 2018, and can verify that consistency was checked by a machine rather than asserted by hand.

/-- RS ΩΛ lies within Planck 2018's two-sigma band. -/
theorem omegaLambda_residual_lt_two_sigma :
    omegaLambdaPlanckResidual < planckOmegaLambdaTwoSigma := by
  unfold omegaLambdaPlanckResidual planckOmegaLambdaTwoSigma planckOmegaLambdaCentral
    planckOmegaLambdaSigma
  exact rs_consistent_with_planck

/-- Interval form of the same two-sigma consistency statement. -/
theorem omegaLambda_in_planck_two_sigma_interval :
    planckOmegaLambdaCentral - planckOmegaLambdaTwoSigma < omega_lambda ∧
      omega_lambda < planckOmegaLambdaCentral + planckOmegaLambdaTwoSigma := by
  have h := omegaLambda_residual_lt_two_sigma
  unfold omegaLambdaPlanckResidual at h
  rw [abs_lt] at h
  unfold planckOmegaLambdaCentral planckOmegaLambdaTwoSigma planckOmegaLambdaSigma at h ⊢
  constructor <;> linarith

/-- The Planck dataset attachment row is positive-sensitivity and currently sensitive. -/
theorem omegaLambda_dataset_attachment_active :
    HasPositiveSensitivity omegaLambdaAttachment ∧
    HasPositiveTargetScale omegaLambdaAttachment ∧
    omegaLambdaAttachment.currentlySensitive = true :=
  ⟨omegaLambda_sensitivity_pos, omegaLambda_target_pos, rfl⟩

theorem omegaLambdaPlanckLikelihoodCert_inhabited :
    Nonempty OmegaLambdaPlanckLikelihoodCert :=
  ⟨omegaLambdaPlanckLikelihoodCert⟩

What this page does not claim

This module does not prove the prediction is correct, only that it is consistent with Planck 2018 at the two-sigma level. It does not derive the value of α from the framework; the expression uses α as an input. It does not establish that the Planck measurement itself is correct or that the framework's broader claims hold.

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/Verification/OmegaLambdaPlanckLikelihood.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: