IndisputableMonolith.Verification.CassiniStrongFieldLikelihood

   1import Mathlib
   2import IndisputableMonolith.Gravity.StrongFieldStructural
   3import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   4
   5/-!
   6# Cassini Strong-Field Likelihood Attachment
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   9
  10This module upgrades the §7 strong-field falsifier row from a dataset
  11attachment to a dataset-specific likelihood-style Lean certificate.
  12
  13Dataset:
  14
  15* Bertotti-Iess-Tortora Cassini radio-link Shapiro-delay test:
  16  `γ - 1 = (2.1 ± 2.3) × 10⁻⁵`.
  17
  18RS structural target:
  19
  20* `φ⁻⁴⁴ ≈ 6.376×10⁻¹⁰` as recorded in
  21  `Verification.FalsifierRegisterDatasets.strongFieldAttachment`.
  22
  23The certificate proves two honest facts:
  24
  251. Cassini's central value is statistically compatible with the RS
  26   structural target at 1σ.
  272. Cassini is **not currently sensitive** to the target scale:
  28   `φ⁻⁴⁴` is far below the reported `2.3×10⁻⁵` one-sigma precision.
  29
  30This is a consistency / non-sensitivity test, not empirical confirmation.
  31Zero `sorry`. Zero new RS-specific axioms.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Verification
  36namespace CassiniStrongFieldLikelihood
  37
  38open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  39
  40noncomputable section
  41
  42/-! ## §1. Dataset constants and residual -/
  43
  44/-- Cassini central measurement for the PPN deviation `γ - 1`. -/
  45def cassiniGammaMinusOneCentral : ℝ := 2.1e-5
  46
  47/-- Cassini one-sigma uncertainty for `γ - 1`. -/
  48def cassiniGammaSigma : ℝ := 2.3e-5
  49
  50/-- RS strong-field structural target scale, taken from the §7 dataset attachment. -/
  51def cassiniRSTargetScale : ℝ := strongFieldAttachment.rsTargetScale
  52
  53/-- Residual between Cassini central value and the RS structural target scale. -/
  54def cassiniStrongFieldResidual : ℝ :=
  55  |cassiniGammaMinusOneCentral - cassiniRSTargetScale|
  56
  57theorem cassiniGammaSigma_pos : 0 < cassiniGammaSigma := by
  58  unfold cassiniGammaSigma
  59  norm_num
  60
  61theorem cassiniRSTargetScale_pos : 0 < cassiniRSTargetScale := by
  62  unfold cassiniRSTargetScale strongFieldAttachment
  63  norm_num
  64
  65/-! ## §2. Likelihood-style statements -/
  66
  67/-- Cassini central value is within 1σ of the RS structural target scale. -/
  68theorem cassini_residual_lt_one_sigma :
  69    cassiniStrongFieldResidual < cassiniGammaSigma := by
  70  unfold cassiniStrongFieldResidual cassiniGammaMinusOneCentral
  71    cassiniRSTargetScale cassiniGammaSigma strongFieldAttachment
  72  norm_num
  73
  74/-- Cassini is not currently sensitive to the φ⁻⁴⁴ target:
  75the one-sigma uncertainty is larger than the target scale. -/
  76theorem cassini_sigma_gt_rs_target :
  77    cassiniRSTargetScale < cassiniGammaSigma := by
  78  unfold cassiniRSTargetScale cassiniGammaSigma strongFieldAttachment
  79  norm_num
  80
  81/-- Cassini dataset attachment is present, positive, and explicitly marked
  82not currently sensitive. -/
  83theorem cassini_dataset_attachment_status :
  84    HasPositiveSensitivity strongFieldAttachment ∧
  85    HasPositiveTargetScale strongFieldAttachment ∧
  86    strongFieldAttachment.currentlySensitive = false :=
  87  ⟨strongField_sensitivity_pos, strongField_target_pos, rfl⟩
  88
  89/-! ## §3. Master cert -/
  90
  91structure CassiniStrongFieldLikelihoodCert where
  92  sigma_pos : 0 < cassiniGammaSigma
  93  target_pos : 0 < cassiniRSTargetScale
  94  residual_lt_one_sigma :
  95    cassiniStrongFieldResidual < cassiniGammaSigma
  96  not_currently_sensitive :
  97    cassiniRSTargetScale < cassiniGammaSigma
  98  dataset_status :
  99    HasPositiveSensitivity strongFieldAttachment ∧
 100    HasPositiveTargetScale strongFieldAttachment ∧
 101    strongFieldAttachment.currentlySensitive = false
 102
 103def cassiniStrongFieldLikelihoodCert : CassiniStrongFieldLikelihoodCert where
 104  sigma_pos := cassiniGammaSigma_pos
 105  target_pos := cassiniRSTargetScale_pos
 106  residual_lt_one_sigma := cassini_residual_lt_one_sigma
 107  not_currently_sensitive := cassini_sigma_gt_rs_target
 108  dataset_status := cassini_dataset_attachment_status
 109
 110theorem cassiniStrongFieldLikelihoodCert_inhabited :
 111    Nonempty CassiniStrongFieldLikelihoodCert :=
 112  ⟨cassiniStrongFieldLikelihoodCert⟩
 113
 114/-- One-statement Cassini likelihood attachment theorem. -/
 115theorem cassini_strong_field_likelihood_one_statement :
 116    (cassiniStrongFieldResidual < cassiniGammaSigma) ∧
 117    (cassiniRSTargetScale < cassiniGammaSigma) ∧
 118    (strongFieldAttachment.currentlySensitive = false) ∧
 119    Nonempty CassiniStrongFieldLikelihoodCert :=
 120  ⟨cassini_residual_lt_one_sigma,
 121   cassini_sigma_gt_rs_target,
 122   rfl,
 123   cassiniStrongFieldLikelihoodCert_inhabited⟩
 124
 125end
 126
 127end CassiniStrongFieldLikelihood
 128end Verification
 129end IndisputableMonolith
 130