IndisputableMonolith.Verification.EHTM87StrongFieldLikelihood

   1import Mathlib
   2import IndisputableMonolith.Gravity.StrongFieldStructural
   3import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   4
   5/-!
   6# EHT M87* 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 third
  11dataset-specific likelihood-style certificate, this time for Event
  12Horizon Telescope observations of M87*.
  13
  14Dataset:
  15
  16* EHT M87* first image:
  17  ring diameter `42 ± 3 μas`, circularity deviation ≤10%, and
  18  shadow-size consistency with Kerr at roughly the 17% level.
  19
  20RS structural target:
  21
  22* a tiny positive fractional deviation from pure GR / Kerr, represented
  23  structurally by `φ⁻⁴⁴`.
  24
  25The certificate proves two honest facts:
  26
  271. The RS structural target is within the current EHT shadow-size and
  28   circularity sensitivity scales.
  292. EHT is **not currently sensitive** to the RS target scale: `φ⁻⁴⁴`
  30   is far below both 17% and 10%.
  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 EHTM87StrongFieldLikelihood
  39
  40open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  41
  42noncomputable section
  43
  44/-! ## §1. Dataset constants and residuals -/
  45
  46/-- EHT M87* ring-diameter central value, in microarcseconds. -/
  47def ehtM87RingDiameterCentralMicroas : ℝ := 42.0
  48
  49/-- EHT M87* ring-diameter one-sigma uncertainty, in microarcseconds. -/
  50def ehtM87RingDiameterSigmaMicroas : ℝ := 3.0
  51
  52/-- Conservative fractional shadow-size sensitivity, using 17% Kerr-consistency scale. -/
  53def ehtM87ShadowFractionalSigma : ℝ := 0.17
  54
  55/-- Conservative circularity sensitivity, using the ≤10% circularity-deviation scale. -/
  56def ehtM87CircularityFractionalSigma : ℝ := 0.10
  57
  58/-- RS structural target fractional deviation scale, taken from the §7 strong-field attachment. -/
  59def ehtM87RSTargetScale : ℝ := strongFieldAttachment.rsTargetScale
  60
  61/-- Residual between current Kerr-consistent central fractional deviation (0) and the RS target. -/
  62def ehtM87ShadowResidual : ℝ :=
  63  |0 - ehtM87RSTargetScale|
  64
  65/-- Residual for circularity channel. -/
  66def ehtM87CircularityResidual : ℝ :=
  67  |0 - ehtM87RSTargetScale|
  68
  69theorem ehtM87ShadowFractionalSigma_pos : 0 < ehtM87ShadowFractionalSigma := by
  70  unfold ehtM87ShadowFractionalSigma
  71  norm_num
  72
  73theorem ehtM87CircularityFractionalSigma_pos :
  74    0 < ehtM87CircularityFractionalSigma := by
  75  unfold ehtM87CircularityFractionalSigma
  76  norm_num
  77
  78theorem ehtM87RSTargetScale_pos : 0 < ehtM87RSTargetScale := by
  79  unfold ehtM87RSTargetScale strongFieldAttachment
  80  norm_num
  81
  82/-! ## §2. Likelihood-style statements -/
  83
  84/-- EHT shadow-size channel is compatible with the RS structural target. -/
  85theorem ehtM87_shadow_residual_lt_sigma :
  86    ehtM87ShadowResidual < ehtM87ShadowFractionalSigma := by
  87  unfold ehtM87ShadowResidual ehtM87RSTargetScale
  88    ehtM87ShadowFractionalSigma strongFieldAttachment
  89  norm_num
  90
  91/-- EHT circularity channel is compatible with the RS structural target. -/
  92theorem ehtM87_circularity_residual_lt_sigma :
  93    ehtM87CircularityResidual < ehtM87CircularityFractionalSigma := by
  94  unfold ehtM87CircularityResidual ehtM87RSTargetScale
  95    ehtM87CircularityFractionalSigma strongFieldAttachment
  96  norm_num
  97
  98/-- EHT shadow-size channel is not currently sensitive to `φ⁻⁴⁴`. -/
  99theorem ehtM87_shadow_sigma_gt_rs_target :
 100    ehtM87RSTargetScale < ehtM87ShadowFractionalSigma := by
 101  unfold ehtM87RSTargetScale ehtM87ShadowFractionalSigma strongFieldAttachment
 102  norm_num
 103
 104/-- EHT circularity channel is not currently sensitive to `φ⁻⁴⁴`. -/
 105theorem ehtM87_circularity_sigma_gt_rs_target :
 106    ehtM87RSTargetScale < ehtM87CircularityFractionalSigma := by
 107  unfold ehtM87RSTargetScale ehtM87CircularityFractionalSigma strongFieldAttachment
 108  norm_num
 109
 110/-- Strong-field dataset attachment is present, positive, and explicitly
 111marked not currently sensitive. -/
 112theorem ehtM87_dataset_attachment_status :
 113    HasPositiveSensitivity strongFieldAttachment ∧
 114    HasPositiveTargetScale strongFieldAttachment ∧
 115    strongFieldAttachment.currentlySensitive = false :=
 116  ⟨strongField_sensitivity_pos, strongField_target_pos, rfl⟩
 117
 118/-! ## §3. Master cert -/
 119
 120structure EHTM87StrongFieldLikelihoodCert where
 121  shadow_sigma_pos : 0 < ehtM87ShadowFractionalSigma
 122  circularity_sigma_pos : 0 < ehtM87CircularityFractionalSigma
 123  target_pos : 0 < ehtM87RSTargetScale
 124  shadow_residual_lt_sigma :
 125    ehtM87ShadowResidual < ehtM87ShadowFractionalSigma
 126  circularity_residual_lt_sigma :
 127    ehtM87CircularityResidual < ehtM87CircularityFractionalSigma
 128  shadow_not_currently_sensitive :
 129    ehtM87RSTargetScale < ehtM87ShadowFractionalSigma
 130  circularity_not_currently_sensitive :
 131    ehtM87RSTargetScale < ehtM87CircularityFractionalSigma
 132  dataset_status :
 133    HasPositiveSensitivity strongFieldAttachment ∧
 134    HasPositiveTargetScale strongFieldAttachment ∧
 135    strongFieldAttachment.currentlySensitive = false
 136
 137def ehtM87StrongFieldLikelihoodCert : EHTM87StrongFieldLikelihoodCert where
 138  shadow_sigma_pos := ehtM87ShadowFractionalSigma_pos
 139  circularity_sigma_pos := ehtM87CircularityFractionalSigma_pos
 140  target_pos := ehtM87RSTargetScale_pos
 141  shadow_residual_lt_sigma := ehtM87_shadow_residual_lt_sigma
 142  circularity_residual_lt_sigma := ehtM87_circularity_residual_lt_sigma
 143  shadow_not_currently_sensitive := ehtM87_shadow_sigma_gt_rs_target
 144  circularity_not_currently_sensitive := ehtM87_circularity_sigma_gt_rs_target
 145  dataset_status := ehtM87_dataset_attachment_status
 146
 147theorem ehtM87StrongFieldLikelihoodCert_inhabited :
 148    Nonempty EHTM87StrongFieldLikelihoodCert :=
 149  ⟨ehtM87StrongFieldLikelihoodCert⟩
 150
 151/-- One-statement EHT M87* likelihood attachment theorem. -/
 152theorem eht_m87_strong_field_likelihood_one_statement :
 153    (ehtM87ShadowResidual < ehtM87ShadowFractionalSigma) ∧
 154    (ehtM87CircularityResidual < ehtM87CircularityFractionalSigma) ∧
 155    (ehtM87RSTargetScale < ehtM87ShadowFractionalSigma) ∧
 156    (ehtM87RSTargetScale < ehtM87CircularityFractionalSigma) ∧
 157    (strongFieldAttachment.currentlySensitive = false) ∧
 158    Nonempty EHTM87StrongFieldLikelihoodCert :=
 159  ⟨ehtM87_shadow_residual_lt_sigma,
 160   ehtM87_circularity_residual_lt_sigma,
 161   ehtM87_shadow_sigma_gt_rs_target,
 162   ehtM87_circularity_sigma_gt_rs_target,
 163   rfl,
 164   ehtM87StrongFieldLikelihoodCert_inhabited⟩
 165
 166end
 167
 168end EHTM87StrongFieldLikelihood
 169end Verification
 170end IndisputableMonolith
 171