IndisputableMonolith.Verification.DarkEnergyWPlanckLikelihood

   1import Mathlib
   2import IndisputableMonolith.Cosmology.DarkEnergyWofZStructural
   3import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   4
   5/-!
   6# Dark-Energy w0 Planck/BAO/SNe Likelihood Attachment
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   9
  10This module upgrades the §7 dark-energy `w(z)` falsifier row with a
  11dataset-specific likelihood-style certificate.
  12
  13Dataset handle:
  14
  15* Planck 2018 + BAO + SNe constant-w example:
  16  `w0 = -1.03 ± 0.03`.
  17
  18RS structural target:
  19
  20* `w_RS(0) = -1`, from
  21  `Cosmology.DarkEnergyWofZStructural.w_RS_linear_at_zero`.
  22* sub-leading deviations away from zero redshift are suppressed by
  23  `φ⁻⁴⁴ z`, and are far below present `w` precision.
  24
  25The certificate proves three honest facts:
  26
  271. The RS baseline `w_RS(0) = -1` is within one sigma of the constant-w
  28   Planck/BAO/SNe central value (the residual equals the quoted sigma).
  292. The `φ⁻⁴⁴` z-scale target is below current one-sigma `w` precision.
  303. The §7 row remains marked not currently sensitive in the dataset
  31   attachment.
  32
  33This is a constant-w baseline consistency / non-sensitivity test, not a
  34confirmation of the dynamic RS `w(z)` function.
  35Zero `sorry`. Zero new RS-specific axioms.
  36-/
  37
  38namespace IndisputableMonolith
  39namespace Verification
  40namespace DarkEnergyWPlanckLikelihood
  41
  42open IndisputableMonolith.Cosmology.DarkEnergyWofZStructural
  43open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  44
  45noncomputable section
  46
  47/-! ## §1. Dataset constants and residual -/
  48
  49/-- Planck+BAO+SNe constant-w central value. -/
  50def planckW0Central : ℝ := -1.03
  51
  52/-- Planck+BAO+SNe constant-w one-sigma uncertainty. -/
  53def planckW0Sigma : ℝ := 0.03
  54
  55/-- RS structural baseline at z=0. -/
  56def rsW0Baseline : ℝ := w_RS_linear 0
  57
  58/-- RS structural deviation target at z=1, from the dataset attachment. -/
  59def rsW1DeviationTarget : ℝ := darkEnergyWAttachment.rsTargetScale
  60
  61/-- Residual between Planck+BAO+SNe constant-w central value and RS baseline. -/
  62def darkEnergyWResidual : ℝ :=
  63  |planckW0Central - rsW0Baseline|
  64
  65theorem planckW0Sigma_pos : 0 < planckW0Sigma := by
  66  unfold planckW0Sigma
  67  norm_num
  68
  69theorem rsW1DeviationTarget_pos : 0 < rsW1DeviationTarget := by
  70  unfold rsW1DeviationTarget darkEnergyWAttachment
  71  norm_num
  72
  73/-! ## §2. Likelihood-style statements -/
  74
  75/-- The RS z=0 baseline is within one sigma of the Planck+BAO+SNe constant-w result.
  76The residual equals the quoted sigma, so the statement is non-strict. -/
  77theorem darkEnergyW_residual_le_one_sigma :
  78    darkEnergyWResidual ≤ planckW0Sigma := by
  79  unfold darkEnergyWResidual planckW0Central rsW0Baseline planckW0Sigma
  80  rw [w_RS_linear_at_zero]
  81  norm_num
  82
  83/-- Current `w` precision is not sensitive to the φ⁻⁴⁴ z-scale target. -/
  84theorem darkEnergyW_sigma_gt_rs_z1_target :
  85    rsW1DeviationTarget < planckW0Sigma := by
  86  unfold rsW1DeviationTarget darkEnergyWAttachment planckW0Sigma
  87  norm_num
  88
  89/-- Dark-energy `w(z)` dataset attachment is present, positive, and
  90explicitly marked not currently sensitive. -/
  91theorem darkEnergyW_dataset_attachment_status :
  92    HasPositiveSensitivity darkEnergyWAttachment ∧
  93    HasPositiveTargetScale darkEnergyWAttachment ∧
  94    darkEnergyWAttachment.currentlySensitive = false :=
  95  ⟨darkEnergyW_sensitivity_pos, darkEnergyW_target_pos, rfl⟩
  96
  97/-! ## §3. Master cert -/
  98
  99structure DarkEnergyWPlanckLikelihoodCert where
 100  sigma_pos : 0 < planckW0Sigma
 101  target_pos : 0 < rsW1DeviationTarget
 102  residual_le_one_sigma :
 103    darkEnergyWResidual ≤ planckW0Sigma
 104  not_currently_sensitive :
 105    rsW1DeviationTarget < planckW0Sigma
 106  dataset_status :
 107    HasPositiveSensitivity darkEnergyWAttachment ∧
 108    HasPositiveTargetScale darkEnergyWAttachment ∧
 109    darkEnergyWAttachment.currentlySensitive = false
 110
 111def darkEnergyWPlanckLikelihoodCert : DarkEnergyWPlanckLikelihoodCert where
 112  sigma_pos := planckW0Sigma_pos
 113  target_pos := rsW1DeviationTarget_pos
 114  residual_le_one_sigma := darkEnergyW_residual_le_one_sigma
 115  not_currently_sensitive := darkEnergyW_sigma_gt_rs_z1_target
 116  dataset_status := darkEnergyW_dataset_attachment_status
 117
 118theorem darkEnergyWPlanckLikelihoodCert_inhabited :
 119    Nonempty DarkEnergyWPlanckLikelihoodCert :=
 120  ⟨darkEnergyWPlanckLikelihoodCert⟩
 121
 122/-- One-statement dark-energy w0 likelihood attachment theorem. -/
 123theorem dark_energy_w_planck_likelihood_one_statement :
 124    (darkEnergyWResidual ≤ planckW0Sigma) ∧
 125    (rsW1DeviationTarget < planckW0Sigma) ∧
 126    (darkEnergyWAttachment.currentlySensitive = false) ∧
 127    Nonempty DarkEnergyWPlanckLikelihoodCert :=
 128  ⟨darkEnergyW_residual_le_one_sigma,
 129   darkEnergyW_sigma_gt_rs_z1_target,
 130   rfl,
 131   darkEnergyWPlanckLikelihoodCert_inhabited⟩
 132
 133end
 134
 135end DarkEnergyWPlanckLikelihood
 136end Verification
 137end IndisputableMonolith
 138