IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Phantom-Coupled GW Antenna Sensitivity (Track J6 of Plan v5)
   7
   8## Status: THEOREM (engineering derivation)
   9
  10Phantom-cavity-coupled GW antenna (RS_PAT_030) achieves sub-Hz
  11strain sensitivity `h_min(f) = h_0 · (5φ Hz / f)`, where `5φ Hz` is
  12the BIT carrier and `h_0` is the carrier-frequency sensitivity floor.
  13At LISA-band frequencies (`mHz`), sensitivity scales linearly above
  14the BIT carrier and inversely below.
  15
  16## Falsifier
  17
  18Phantom-cavity GW antenna deployed at sub-Hz showing sensitivity
  19ceiling not scaling as `1/f` above noise floor.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Engineering
  24namespace PhantomCoupledGWAntennaSensitivity
  25
  26open Constants
  27
  28noncomputable section
  29
  30/-! ## §1. Carrier and sensitivity floor -/
  31
  32/-- Carrier frequency = 5φ Hz. -/
  33def carrier : ℝ := 5 * phi
  34
  35theorem carrier_pos : 0 < carrier := by
  36  unfold carrier; exact mul_pos (by norm_num) phi_pos
  37
  38theorem carrier_band : (8.05 : ℝ) < carrier ∧ carrier < 8.10 := by
  39  unfold carrier
  40  have h1 := phi_gt_onePointSixOne
  41  have h2 := phi_lt_onePointSixTwo
  42  refine ⟨by linarith, by linarith⟩
  43
  44/-- Sensitivity floor at carrier (dimensionless reference). -/
  45def h_0 : ℝ := 1
  46
  47/-- Sensitivity at frequency `f > 0`: `h_min(f) = h_0 · carrier / f`. -/
  48def sensitivity (f : ℝ) : ℝ :=
  49  if f ≤ 0 then 0 else h_0 * carrier / f
  50
  51theorem sensitivity_at_carrier : sensitivity carrier = h_0 := by
  52  unfold sensitivity h_0
  53  rw [if_neg (not_le.mpr carrier_pos)]
  54  have h_ne : carrier ≠ 0 := ne_of_gt carrier_pos
  55  field_simp
  56
  57theorem sensitivity_pos {f : ℝ} (h : 0 < f) : 0 < sensitivity f := by
  58  unfold sensitivity h_0
  59  rw [if_neg (not_le.mpr h)]
  60  apply div_pos
  61  · simp; exact carrier_pos
  62  · exact h
  63
  64/-- Sensitivity is strictly anti-monotonic in `f` (above carrier:
  65sensitivity decreases; below: increases). -/
  66theorem sensitivity_strict_anti {f₁ f₂ : ℝ} (h₁ : 0 < f₁) (h₂ : f₁ < f₂) :
  67    sensitivity f₂ < sensitivity f₁ := by
  68  unfold sensitivity h_0
  69  have h₂_pos : 0 < f₂ := lt_trans h₁ h₂
  70  rw [if_neg (not_le.mpr h₁), if_neg (not_le.mpr h₂_pos)]
  71  -- 1·carrier/f₂ < 1·carrier/f₁ ↔ carrier/f₂ < carrier/f₁ ↔ f₁ < f₂
  72  simp only [one_mul]
  73  exact div_lt_div_of_pos_left carrier_pos h₁ h₂
  74
  75/-! ## §2. Master certificate -/
  76
  77structure PhantomCoupledGWAntennaSensitivityCert where
  78  carrier_band : (8.05 : ℝ) < carrier ∧ carrier < 8.10
  79  sensitivity_at_carrier : sensitivity carrier = h_0
  80  sensitivity_pos : ∀ {f : ℝ}, 0 < f → 0 < sensitivity f
  81  sensitivity_strict_anti : ∀ {f₁ f₂ : ℝ}, 0 < f₁ → f₁ < f₂ →
  82    sensitivity f₂ < sensitivity f₁
  83
  84def phantomCoupledGWAntennaSensitivityCert :
  85    PhantomCoupledGWAntennaSensitivityCert where
  86  carrier_band := carrier_band
  87  sensitivity_at_carrier := sensitivity_at_carrier
  88  sensitivity_pos := @sensitivity_pos
  89  sensitivity_strict_anti := @sensitivity_strict_anti
  90
  91/-- **GW ANTENNA ONE-STATEMENT.** Carrier `5φ ∈ (8.05, 8.10) Hz`;
  92sensitivity scales as `carrier/f`, strictly anti-monotonic in
  93frequency above and below the carrier. -/
  94theorem gw_antenna_one_statement :
  95    (8.05 : ℝ) < carrier ∧ carrier < 8.10 ∧
  96    sensitivity carrier = h_0 ∧
  97    (∀ {f₁ f₂ : ℝ}, 0 < f₁ → f₁ < f₂ → sensitivity f₂ < sensitivity f₁) :=
  98  ⟨carrier_band.1, carrier_band.2, sensitivity_at_carrier,
  99   @sensitivity_strict_anti⟩
 100
 101end
 102
 103end PhantomCoupledGWAntennaSensitivity
 104end Engineering
 105end IndisputableMonolith
 106