IndisputableMonolith.Verification.FalsifierRegisterDatasets

   1import Mathlib
   2
   3/-!
   4# Quantum Gravity Falsifier Register Dataset Attachments
   5
   6## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   7
   8This module attaches concrete named datasets and numerical sensitivity
   9records to every row of the quantum-gravity master plan §7 falsifier
  10register.
  11
  12The records are deliberately conservative. A row is **attached** when it
  13has:
  14
  15* a named observational channel or dataset;
  16* a numerical sensitivity scale;
  17* an RS target scale or band to compare against;
  18* an honest flag saying whether current data are already sensitive to
  19  the RS target.
  20
  21The purpose is falsifiability accounting, not empirical confirmation.
  22The records below do not claim that any dataset has confirmed RS. They
  23only make explicit which experiment tests which prediction, and at what
  24reported precision.
  25
  26Anchor examples:
  27
  28* Planck 2018: `Ω_Λ = 0.6889 ± 0.0056`.
  29* Planck+BAO+SNe: `w₀ = -1.03 ± 0.03` (constant-w extension).
  30* Cassini Shapiro delay: `γ - 1 = (2.1 ± 2.3)×10⁻⁵`.
  31* EHT M87*: ring diameter `42 ± 3 μas`, shadow-size Kerr consistency
  32  at roughly 17%, circularity deviation ≤10%.
  33* GRAVITY S2: Schwarzschild-precession factor `f_SP = 1.10 ± 0.19`.
  34* NANOGrav 15-year: Hellings-Downs correlated stochastic background,
  35  68 pulsars, 15 yr baseline, power-law spectrum compatible with the
  36  SMBHB reference slope `γ = 13/3`.
  37* EPTA DR2: CRS/GWB spectral-index record around `γ ≈ 3.83` and
  38  `log10 A ≈ -14.32` in the relevant analysis.
  39* GWTC-3 tests of GR: no significant deviations from GR, no
  40  post-merger echoes in analyzed events, graviton-mass bound
  41  `m_g ≤ 2.42×10⁻²³ eV/c²`.
  42
  43Zero `sorry`. Zero new RS-specific axioms.
  44-/
  45
  46namespace IndisputableMonolith
  47namespace Verification
  48namespace FalsifierRegisterDatasets
  49
  50noncomputable section
  51
  52/-! ## §1. Dataset attachment record -/
  53
  54/-- Dataset attachment for a falsifier-register row.
  55
  56`sensitivity` and `rsTargetScale` are dimensionless unless the field
  57`units` says otherwise. `currentlySensitive` records whether the named
  58dataset can already reach the RS target scale. For several future rows
  59this is honestly `false`: the dataset is named, but it is not yet
  60sensitive enough to test the φ-suppressed target. -/
  61structure DatasetAttachment where
  62  sector : String
  63  dataset : String
  64  units : String
  65  sensitivity : ℝ
  66  rsTargetScale : ℝ
  67  currentlySensitive : Bool
  68
  69/-- Positive numerical sensitivity requirement. -/
  70def HasPositiveSensitivity (D : DatasetAttachment) : Prop :=
  71  0 < D.sensitivity
  72
  73/-- Positive RS target scale requirement. -/
  74def HasPositiveTargetScale (D : DatasetAttachment) : Prop :=
  75  0 < D.rsTargetScale
  76
  77/-! ## §2. Named dataset records -/
  78
  79/-- BMV tabletop / MAQRO-class phase-rate row.
  80
  81Target band from the master plan and `papers/reproducibility/bmv_phase_rate.py`:
  82`[4.77, 5.04]×10⁻⁷ rad/s`. Current MAQRO-class experiment is a future
  83channel, so the row is attached but not yet currently sensitive. -/
  84def bmvAttachment : DatasetAttachment where
  85  sector := "BMV phase-rate sign and magnitude"
  86  dataset := "MAQRO-class tabletop BMV entanglement-generation experiment"
  87  units := "rad/s"
  88  sensitivity := 5.04e-7 - 4.77e-7
  89  rsTargetScale := (4.77e-7 + 5.04e-7) / 2
  90  currentlySensitive := false
  91
  92/-- Hawking temperature row.
  93
  94The falsifier threshold is 10% on the leading Hawking temperature formula.
  95The row is attached to future analog-gravity / primordial-BH searches. -/
  96def hawkingTemperatureAttachment : DatasetAttachment where
  97  sector := "Hawking temperature"
  98  dataset := "Future analog-gravity or primordial-BH temperature measurement"
  99  units := "fractional T_H"
 100  sensitivity := 0.10
 101  rsTargetScale := 1.0
 102  currentlySensitive := false
 103
 104/-- Leading-log entropy coefficient row.
 105
 106Target coefficient `c_RS = -log φ / 2 ≈ -0.2406`; falsifier sensitivity
 1070.10 safely distinguishes RS from LQG's `-1/2` margin (`>0.25`). -/
 108def leadingLogEntropyAttachment : DatasetAttachment where
 109  sector := "Leading-log entropy coefficient"
 110  dataset := "LIGO/Virgo ringdown and future LISA/Einstein Telescope QNM spectroscopy"
 111  units := "coefficient"
 112  sensitivity := 0.10
 113  rsTargetScale := 0.05
 114  currentlySensitive := false
 115
 116/-- Page curve row.
 117
 118Structural row: future analog-gravity experiment must distinguish the
 119triangular Page curve from monotone Hawking entropy increase. -/
 120def pageCurveAttachment : DatasetAttachment where
 121  sector := "Page curve"
 122  dataset := "Future analog-gravity Page-curve experiment"
 123  units := "shape discriminator"
 124  sensitivity := 1.0
 125  rsTargetScale := 1.0
 126  currentlySensitive := false
 127
 128/-- Echo phenomenology row.
 129
 130GWTC-3 tests of GR report no post-merger echoes in the analyzed events.
 131RS echo damping target is the dimensionless amplitude ratio `1/φ ≈ 0.618`. -/
 132def echoAttachment : DatasetAttachment where
 133  sector := "Black-hole echo phenomenology"
 134  dataset := "LIGO/Virgo/KAGRA GWTC-3 tests of GR ringdown / post-merger echo search"
 135  units := "echo amplitude ratio"
 136  sensitivity := 0.10
 137  rsTargetScale := 0.618
 138  currentlySensitive := false
 139
 140/-- Cosmological constant row.
 141
 142Planck 2018 base-ΛCDM record: `Ω_Λ = 0.6889 ± 0.0056`; RS band
 143`Ω_Λ ∈ (0.683, 0.686)` is close enough for a two-sigma consistency check. -/
 144def omegaLambdaAttachment : DatasetAttachment where
 145  sector := "Cosmological constant ΩΛ"
 146  dataset := "Planck 2018 TT,TE,EE+lowE+lensing"
 147  units := "ΩΛ"
 148  sensitivity := 0.0056
 149  rsTargetScale := 0.686 - 0.683
 150  currentlySensitive := true
 151
 152/-- Dark-energy equation-of-state row.
 153
 154Planck+BAO+SNe gives a constant-w example `w₀ = -1.03 ± 0.03`.
 155DESI DR1/DR2 gives the modern dynamic-w channel. The structural RS target
 156scale `φ⁻⁴⁴ z` is about `6.38×10⁻¹⁰` at z=1, far below current
 157cosmological equation-of-state precision. -/
 158def darkEnergyWAttachment : DatasetAttachment where
 159  sector := "Dark-energy equation of state w(z)"
 160  dataset := "DESI BAO + Planck CMB + supernovae w0-wa analyses"
 161  units := "w"
 162  sensitivity := 0.03
 163  rsTargetScale := 6.376e-10
 164  currentlySensitive := false
 165
 166/-- QNM discriminator row.
 167
 168GWTC-3 tests of GR report remnant consistency and no significant QNM
 169deviation; future LISA/ET supply the high-precision row. The numerical
 170sensitivity here stores the current graviton-mass bound as the concrete
 171GWTC-3 scale reported in the tests-of-GR abstract. -/
 172def qnmAttachment : DatasetAttachment where
 173  sector := "Quasinormal-mode / ringdown discriminator"
 174  dataset := "LIGO/Virgo/KAGRA GWTC-3 tests of GR; future LISA/Einstein Telescope"
 175  units := "eV/c^2 graviton-mass bound"
 176  sensitivity := 2.42e-23
 177  rsTargetScale := 0.2406
 178  currentlySensitive := false
 179
 180/-- PTA stochastic background row.
 181
 182NANOGrav 15-year: 68 pulsars over 15 years, Hellings-Downs correlated
 183background, power-law spectrum compatible with the SMBHB reference slope
 184`γ = 13/3`. The RS structural target uses `log φ ≈ 0.481` as a positive
 185φ-rational signature; this row is attached, but not yet dynamically
 186matched to the full spectrum. -/
 187def ptaAttachment : DatasetAttachment where
 188  sector := "PTA stochastic gravitational-wave background"
 189  dataset := "NANOGrav 15-year + EPTA DR2 nanohertz stochastic background"
 190  units := "spectral-index scale"
 191  sensitivity := 0.80
 192  rsTargetScale := 0.481
 193  currentlySensitive := false
 194
 195/-- Strong-field row: EHT / GRAVITY / Cassini.
 196
 197This row stores Cassini's PPN-γ precision as the most precise current
 198solar-system strong/weak-field number, while the dataset string records
 199the full strong-field channel list. -/
 200def strongFieldAttachment : DatasetAttachment where
 201  sector := "Strong-field / precision-GR tests"
 202  dataset := "Cassini Shapiro delay; GRAVITY S2 precession; EHT M87* shadow"
 203  units := "fractional metric-deviation scale"
 204  sensitivity := 2.3e-5
 205  rsTargetScale := 6.376e-10
 206  currentlySensitive := false
 207
 208/-! ## §3. Positivity lemmas for each record -/
 209
 210theorem bmv_sensitivity_pos : HasPositiveSensitivity bmvAttachment := by
 211  unfold HasPositiveSensitivity bmvAttachment
 212  norm_num
 213
 214theorem hawking_sensitivity_pos :
 215    HasPositiveSensitivity hawkingTemperatureAttachment := by
 216  unfold HasPositiveSensitivity hawkingTemperatureAttachment
 217  norm_num
 218
 219theorem leadingLog_sensitivity_pos :
 220    HasPositiveSensitivity leadingLogEntropyAttachment := by
 221  unfold HasPositiveSensitivity leadingLogEntropyAttachment
 222  norm_num
 223
 224theorem pageCurve_sensitivity_pos :
 225    HasPositiveSensitivity pageCurveAttachment := by
 226  unfold HasPositiveSensitivity pageCurveAttachment
 227  norm_num
 228
 229theorem echo_sensitivity_pos : HasPositiveSensitivity echoAttachment := by
 230  unfold HasPositiveSensitivity echoAttachment
 231  norm_num
 232
 233theorem omegaLambda_sensitivity_pos :
 234    HasPositiveSensitivity omegaLambdaAttachment := by
 235  unfold HasPositiveSensitivity omegaLambdaAttachment
 236  norm_num
 237
 238theorem darkEnergyW_sensitivity_pos :
 239    HasPositiveSensitivity darkEnergyWAttachment := by
 240  unfold HasPositiveSensitivity darkEnergyWAttachment
 241  norm_num
 242
 243theorem qnm_sensitivity_pos : HasPositiveSensitivity qnmAttachment := by
 244  unfold HasPositiveSensitivity qnmAttachment
 245  norm_num
 246
 247theorem pta_sensitivity_pos : HasPositiveSensitivity ptaAttachment := by
 248  unfold HasPositiveSensitivity ptaAttachment
 249  norm_num
 250
 251theorem strongField_sensitivity_pos :
 252    HasPositiveSensitivity strongFieldAttachment := by
 253  unfold HasPositiveSensitivity strongFieldAttachment
 254  norm_num
 255
 256/-! ## §4. Target-scale positivity -/
 257
 258theorem bmv_target_pos : HasPositiveTargetScale bmvAttachment := by
 259  unfold HasPositiveTargetScale bmvAttachment
 260  norm_num
 261
 262theorem hawking_target_pos :
 263    HasPositiveTargetScale hawkingTemperatureAttachment := by
 264  unfold HasPositiveTargetScale hawkingTemperatureAttachment
 265  norm_num
 266
 267theorem leadingLog_target_pos :
 268    HasPositiveTargetScale leadingLogEntropyAttachment := by
 269  unfold HasPositiveTargetScale leadingLogEntropyAttachment
 270  norm_num
 271
 272theorem pageCurve_target_pos :
 273    HasPositiveTargetScale pageCurveAttachment := by
 274  unfold HasPositiveTargetScale pageCurveAttachment
 275  norm_num
 276
 277theorem echo_target_pos : HasPositiveTargetScale echoAttachment := by
 278  unfold HasPositiveTargetScale echoAttachment
 279  norm_num
 280
 281theorem omegaLambda_target_pos :
 282    HasPositiveTargetScale omegaLambdaAttachment := by
 283  unfold HasPositiveTargetScale omegaLambdaAttachment
 284  norm_num
 285
 286theorem darkEnergyW_target_pos :
 287    HasPositiveTargetScale darkEnergyWAttachment := by
 288  unfold HasPositiveTargetScale darkEnergyWAttachment
 289  norm_num
 290
 291theorem qnm_target_pos : HasPositiveTargetScale qnmAttachment := by
 292  unfold HasPositiveTargetScale qnmAttachment
 293  norm_num
 294
 295theorem pta_target_pos : HasPositiveTargetScale ptaAttachment := by
 296  unfold HasPositiveTargetScale ptaAttachment
 297  norm_num
 298
 299theorem strongField_target_pos :
 300    HasPositiveTargetScale strongFieldAttachment := by
 301  unfold HasPositiveTargetScale strongFieldAttachment
 302  norm_num
 303
 304/-! ## §5. Master certificate -/
 305
 306/-- Master certificate: every §7 falsifier-register row has a named
 307dataset, a positive numerical sensitivity scale, and a positive RS target
 308scale. -/
 309structure FalsifierDatasetRegisterCert where
 310  bmv_sensitivity : HasPositiveSensitivity bmvAttachment
 311  bmv_target : HasPositiveTargetScale bmvAttachment
 312  hawking_sensitivity : HasPositiveSensitivity hawkingTemperatureAttachment
 313  hawking_target : HasPositiveTargetScale hawkingTemperatureAttachment
 314  leadingLog_sensitivity : HasPositiveSensitivity leadingLogEntropyAttachment
 315  leadingLog_target : HasPositiveTargetScale leadingLogEntropyAttachment
 316  pageCurve_sensitivity : HasPositiveSensitivity pageCurveAttachment
 317  pageCurve_target : HasPositiveTargetScale pageCurveAttachment
 318  echo_sensitivity : HasPositiveSensitivity echoAttachment
 319  echo_target : HasPositiveTargetScale echoAttachment
 320  omegaLambda_sensitivity : HasPositiveSensitivity omegaLambdaAttachment
 321  omegaLambda_target : HasPositiveTargetScale omegaLambdaAttachment
 322  darkEnergyW_sensitivity : HasPositiveSensitivity darkEnergyWAttachment
 323  darkEnergyW_target : HasPositiveTargetScale darkEnergyWAttachment
 324  qnm_sensitivity : HasPositiveSensitivity qnmAttachment
 325  qnm_target : HasPositiveTargetScale qnmAttachment
 326  pta_sensitivity : HasPositiveSensitivity ptaAttachment
 327  pta_target : HasPositiveTargetScale ptaAttachment
 328  strongField_sensitivity : HasPositiveSensitivity strongFieldAttachment
 329  strongField_target : HasPositiveTargetScale strongFieldAttachment
 330
 331def falsifierDatasetRegisterCert : FalsifierDatasetRegisterCert where
 332  bmv_sensitivity := bmv_sensitivity_pos
 333  bmv_target := bmv_target_pos
 334  hawking_sensitivity := hawking_sensitivity_pos
 335  hawking_target := hawking_target_pos
 336  leadingLog_sensitivity := leadingLog_sensitivity_pos
 337  leadingLog_target := leadingLog_target_pos
 338  pageCurve_sensitivity := pageCurve_sensitivity_pos
 339  pageCurve_target := pageCurve_target_pos
 340  echo_sensitivity := echo_sensitivity_pos
 341  echo_target := echo_target_pos
 342  omegaLambda_sensitivity := omegaLambda_sensitivity_pos
 343  omegaLambda_target := omegaLambda_target_pos
 344  darkEnergyW_sensitivity := darkEnergyW_sensitivity_pos
 345  darkEnergyW_target := darkEnergyW_target_pos
 346  qnm_sensitivity := qnm_sensitivity_pos
 347  qnm_target := qnm_target_pos
 348  pta_sensitivity := pta_sensitivity_pos
 349  pta_target := pta_target_pos
 350  strongField_sensitivity := strongField_sensitivity_pos
 351  strongField_target := strongField_target_pos
 352
 353theorem falsifierDatasetRegisterCert_inhabited :
 354    Nonempty FalsifierDatasetRegisterCert :=
 355  ⟨falsifierDatasetRegisterCert⟩
 356
 357/-- One-statement form: all falsifier-register rows have positive
 358dataset sensitivities and positive RS target scales. -/
 359theorem falsifier_dataset_register_one_statement :
 360    HasPositiveSensitivity bmvAttachment ∧
 361    HasPositiveSensitivity hawkingTemperatureAttachment ∧
 362    HasPositiveSensitivity leadingLogEntropyAttachment ∧
 363    HasPositiveSensitivity pageCurveAttachment ∧
 364    HasPositiveSensitivity echoAttachment ∧
 365    HasPositiveSensitivity omegaLambdaAttachment ∧
 366    HasPositiveSensitivity darkEnergyWAttachment ∧
 367    HasPositiveSensitivity qnmAttachment ∧
 368    HasPositiveSensitivity ptaAttachment ∧
 369    HasPositiveSensitivity strongFieldAttachment ∧
 370    Nonempty FalsifierDatasetRegisterCert :=
 371  ⟨bmv_sensitivity_pos,
 372   hawking_sensitivity_pos,
 373   leadingLog_sensitivity_pos,
 374   pageCurve_sensitivity_pos,
 375   echo_sensitivity_pos,
 376   omegaLambda_sensitivity_pos,
 377   darkEnergyW_sensitivity_pos,
 378   qnm_sensitivity_pos,
 379   pta_sensitivity_pos,
 380   strongField_sensitivity_pos,
 381   falsifierDatasetRegisterCert_inhabited⟩
 382
 383end
 384
 385end FalsifierRegisterDatasets
 386end Verification
 387end IndisputableMonolith
 388