IndisputableMonolith.Verification.OmegaLambdaPlanckLikelihood

   1import Mathlib
   2import IndisputableMonolith.Cosmology.OmegaLambdaDerivation
   3import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   4
   5/-!
   6# ΩΛ Planck Likelihood Attachment
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   9
  10This module upgrades the §7 ΩΛ falsifier-register row from a dataset
  11attachment to a dataset-specific likelihood-style Lean certificate.
  12
  13The underlying prediction comes from
  14`Cosmology.OmegaLambdaDerivation`:
  15
  16* `omega_lambda = 11/16 - α/π`
  17* `0.683 < omega_lambda ∧ omega_lambda < 0.686`
  18* `|omega_lambda - omega_lambda_planck2018| < 2 * omega_lambda_planck_err`
  19
  20The dataset record comes from
  21`Verification.FalsifierRegisterDatasets.omegaLambdaAttachment`:
  22
  23* Planck 2018 TT,TE,EE+lowE+lensing
  24* `ΩΛ = 0.6889 ± 0.0056`
  25* currently sensitive to the RS interval at the two-sigma consistency level
  26
  27This is a consistency test, not empirical confirmation.
  28Zero `sorry`. Zero new RS-specific axioms.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Verification
  33namespace OmegaLambdaPlanckLikelihood
  34
  35open IndisputableMonolith.Cosmology.OmegaLambdaDerivation
  36open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  37
  38noncomputable section
  39
  40/-! ## §1. Dataset constants and residual -/
  41
  42/-- Planck 2018 central value for ΩΛ. -/
  43def planckOmegaLambdaCentral : ℝ := omega_lambda_planck2018
  44
  45/-- Planck 2018 one-sigma uncertainty for ΩΛ. -/
  46def planckOmegaLambdaSigma : ℝ := omega_lambda_planck_err
  47
  48/-- Absolute residual between the RS prediction and the Planck 2018 central value. -/
  49def omegaLambdaPlanckResidual : ℝ :=
  50  |omega_lambda - planckOmegaLambdaCentral|
  51
  52/-- Two-sigma Planck tolerance. -/
  53def planckOmegaLambdaTwoSigma : ℝ :=
  54  2 * planckOmegaLambdaSigma
  55
  56theorem planckOmegaLambdaSigma_pos : 0 < planckOmegaLambdaSigma := by
  57  unfold planckOmegaLambdaSigma omega_lambda_planck_err
  58  norm_num
  59
  60theorem planckOmegaLambdaTwoSigma_pos : 0 < planckOmegaLambdaTwoSigma := by
  61  unfold planckOmegaLambdaTwoSigma
  62  exact mul_pos (by norm_num) planckOmegaLambdaSigma_pos
  63
  64/-! ## §2. Lean likelihood-style consistency certificate -/
  65
  66/-- RS ΩΛ lies within Planck 2018's two-sigma band. -/
  67theorem omegaLambda_residual_lt_two_sigma :
  68    omegaLambdaPlanckResidual < planckOmegaLambdaTwoSigma := by
  69  unfold omegaLambdaPlanckResidual planckOmegaLambdaTwoSigma planckOmegaLambdaCentral
  70    planckOmegaLambdaSigma
  71  exact rs_consistent_with_planck
  72
  73/-- Interval form of the same two-sigma consistency statement. -/
  74theorem omegaLambda_in_planck_two_sigma_interval :
  75    planckOmegaLambdaCentral - planckOmegaLambdaTwoSigma < omega_lambda ∧
  76      omega_lambda < planckOmegaLambdaCentral + planckOmegaLambdaTwoSigma := by
  77  have h := omegaLambda_residual_lt_two_sigma
  78  unfold omegaLambdaPlanckResidual at h
  79  rw [abs_lt] at h
  80  unfold planckOmegaLambdaCentral planckOmegaLambdaTwoSigma planckOmegaLambdaSigma at h ⊢
  81  constructor <;> linarith
  82
  83/-- The Planck dataset attachment row is positive-sensitivity and currently sensitive. -/
  84theorem omegaLambda_dataset_attachment_active :
  85    HasPositiveSensitivity omegaLambdaAttachment ∧
  86    HasPositiveTargetScale omegaLambdaAttachment ∧
  87    omegaLambdaAttachment.currentlySensitive = true :=
  88  ⟨omegaLambda_sensitivity_pos, omegaLambda_target_pos, rfl⟩
  89
  90/-! ## §3. Master cert -/
  91
  92structure OmegaLambdaPlanckLikelihoodCert where
  93  sigma_pos : 0 < planckOmegaLambdaSigma
  94  two_sigma_pos : 0 < planckOmegaLambdaTwoSigma
  95  residual_lt_two_sigma :
  96    omegaLambdaPlanckResidual < planckOmegaLambdaTwoSigma
  97  interval_form :
  98    planckOmegaLambdaCentral - planckOmegaLambdaTwoSigma < omega_lambda ∧
  99      omega_lambda < planckOmegaLambdaCentral + planckOmegaLambdaTwoSigma
 100  dataset_active :
 101    HasPositiveSensitivity omegaLambdaAttachment ∧
 102    HasPositiveTargetScale omegaLambdaAttachment ∧
 103    omegaLambdaAttachment.currentlySensitive = true
 104
 105def omegaLambdaPlanckLikelihoodCert : OmegaLambdaPlanckLikelihoodCert where
 106  sigma_pos := planckOmegaLambdaSigma_pos
 107  two_sigma_pos := planckOmegaLambdaTwoSigma_pos
 108  residual_lt_two_sigma := omegaLambda_residual_lt_two_sigma
 109  interval_form := omegaLambda_in_planck_two_sigma_interval
 110  dataset_active := omegaLambda_dataset_attachment_active
 111
 112theorem omegaLambdaPlanckLikelihoodCert_inhabited :
 113    Nonempty OmegaLambdaPlanckLikelihoodCert :=
 114  ⟨omegaLambdaPlanckLikelihoodCert⟩
 115
 116/-- One-statement ΩΛ likelihood attachment theorem. -/
 117theorem omega_lambda_planck_likelihood_one_statement :
 118    (omegaLambdaPlanckResidual < planckOmegaLambdaTwoSigma) ∧
 119    (planckOmegaLambdaCentral - planckOmegaLambdaTwoSigma < omega_lambda ∧
 120      omega_lambda < planckOmegaLambdaCentral + planckOmegaLambdaTwoSigma) ∧
 121    (omegaLambdaAttachment.currentlySensitive = true) ∧
 122    Nonempty OmegaLambdaPlanckLikelihoodCert :=
 123  ⟨omegaLambda_residual_lt_two_sigma,
 124   omegaLambda_in_planck_two_sigma_interval,
 125   rfl,
 126   omegaLambdaPlanckLikelihoodCert_inhabited⟩
 127
 128end
 129
 130end OmegaLambdaPlanckLikelihood
 131end Verification
 132end IndisputableMonolith
 133