IndisputableMonolith.Verification.GravityS2StrongFieldLikelihood

   1import Mathlib
   2import IndisputableMonolith.Gravity.StrongFieldStructural
   3import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   4
   5/-!
   6# GRAVITY S2 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 with a second
  11dataset-specific likelihood-style certificate, this time for the GRAVITY
  12Collaboration's S2 Schwarzschild-precession measurement.
  13
  14Dataset:
  15
  16* GRAVITY Collaboration (2020) S2 precession:
  17  `f_SP = 1.10 ± 0.19`, where `f_SP = 0` is Newtonian and `f_SP = 1`
  18  is GR.
  19
  20RS structural target:
  21
  22* a tiny positive deviation from GR, represented structurally as
  23  `f_SP = 1 + φ⁻⁴⁴`.
  24
  25The certificate proves two honest facts:
  26
  271. GRAVITY's central value is statistically compatible with the RS
  28   structural target at 1σ.
  292. GRAVITY is **not currently sensitive** to the RS target scale:
  30   `φ⁻⁴⁴` is far below the reported `0.19` one-sigma precision.
  31
  32This is a consistency / non-sensitivity test, not empirical confirmation.
  33Zero `sorry`. Zero new RS-specific axioms.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Verification
  38namespace GravityS2StrongFieldLikelihood
  39
  40open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  41
  42noncomputable section
  43
  44/-! ## §1. Dataset constants and residual -/
  45
  46/-- GRAVITY S2 central measurement for the Schwarzschild-precession factor. -/
  47def gravityS2FSPCentral : ℝ := 1.10
  48
  49/-- GRAVITY S2 one-sigma uncertainty for `f_SP`. -/
  50def gravityS2FSPSigma : ℝ := 0.19
  51
  52/-- RS structural target deviation scale, taken from the §7 strong-field attachment. -/
  53def gravityS2RSTargetScale : ℝ := strongFieldAttachment.rsTargetScale
  54
  55/-- RS structural target for the S2 precession factor: GR value plus φ⁻⁴⁴. -/
  56def gravityS2RSPredictedFSP : ℝ := 1 + gravityS2RSTargetScale
  57
  58/-- Residual between GRAVITY S2 central value and the RS structural target. -/
  59def gravityS2Residual : ℝ :=
  60  |gravityS2FSPCentral - gravityS2RSPredictedFSP|
  61
  62theorem gravityS2FSPSigma_pos : 0 < gravityS2FSPSigma := by
  63  unfold gravityS2FSPSigma
  64  norm_num
  65
  66theorem gravityS2RSTargetScale_pos : 0 < gravityS2RSTargetScale := by
  67  unfold gravityS2RSTargetScale strongFieldAttachment
  68  norm_num
  69
  70/-! ## §2. Likelihood-style statements -/
  71
  72/-- GRAVITY S2 central value is within 1σ of the RS structural target. -/
  73theorem gravityS2_residual_lt_one_sigma :
  74    gravityS2Residual < gravityS2FSPSigma := by
  75  unfold gravityS2Residual gravityS2FSPCentral gravityS2RSPredictedFSP
  76    gravityS2RSTargetScale gravityS2FSPSigma strongFieldAttachment
  77  norm_num
  78
  79/-- GRAVITY S2 is not currently sensitive to the φ⁻⁴⁴ target:
  80the one-sigma uncertainty is larger than the target scale. -/
  81theorem gravityS2_sigma_gt_rs_target :
  82    gravityS2RSTargetScale < gravityS2FSPSigma := by
  83  unfold gravityS2RSTargetScale gravityS2FSPSigma strongFieldAttachment
  84  norm_num
  85
  86/-- Strong-field dataset attachment is present, positive, and explicitly
  87marked not currently sensitive. -/
  88theorem gravityS2_dataset_attachment_status :
  89    HasPositiveSensitivity strongFieldAttachment ∧
  90    HasPositiveTargetScale strongFieldAttachment ∧
  91    strongFieldAttachment.currentlySensitive = false :=
  92  ⟨strongField_sensitivity_pos, strongField_target_pos, rfl⟩
  93
  94/-! ## §3. Master cert -/
  95
  96structure GravityS2StrongFieldLikelihoodCert where
  97  sigma_pos : 0 < gravityS2FSPSigma
  98  target_pos : 0 < gravityS2RSTargetScale
  99  residual_lt_one_sigma :
 100    gravityS2Residual < gravityS2FSPSigma
 101  not_currently_sensitive :
 102    gravityS2RSTargetScale < gravityS2FSPSigma
 103  dataset_status :
 104    HasPositiveSensitivity strongFieldAttachment ∧
 105    HasPositiveTargetScale strongFieldAttachment ∧
 106    strongFieldAttachment.currentlySensitive = false
 107
 108def gravityS2StrongFieldLikelihoodCert : GravityS2StrongFieldLikelihoodCert where
 109  sigma_pos := gravityS2FSPSigma_pos
 110  target_pos := gravityS2RSTargetScale_pos
 111  residual_lt_one_sigma := gravityS2_residual_lt_one_sigma
 112  not_currently_sensitive := gravityS2_sigma_gt_rs_target
 113  dataset_status := gravityS2_dataset_attachment_status
 114
 115theorem gravityS2StrongFieldLikelihoodCert_inhabited :
 116    Nonempty GravityS2StrongFieldLikelihoodCert :=
 117  ⟨gravityS2StrongFieldLikelihoodCert⟩
 118
 119/-- One-statement GRAVITY S2 likelihood attachment theorem. -/
 120theorem gravity_s2_strong_field_likelihood_one_statement :
 121    (gravityS2Residual < gravityS2FSPSigma) ∧
 122    (gravityS2RSTargetScale < gravityS2FSPSigma) ∧
 123    (strongFieldAttachment.currentlySensitive = false) ∧
 124    Nonempty GravityS2StrongFieldLikelihoodCert :=
 125  ⟨gravityS2_residual_lt_one_sigma,
 126   gravityS2_sigma_gt_rs_target,
 127   rfl,
 128   gravityS2StrongFieldLikelihoodCert_inhabited⟩
 129
 130end
 131
 132end GravityS2StrongFieldLikelihood
 133end Verification
 134end IndisputableMonolith
 135