IndisputableMonolith.Gravity.PTAStructural

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cosmology.PhiRungLadder
   4import IndisputableMonolith.Gravity.MasterTheorem
   5
   6/-!
   7# Gravity Track 6.B: PTA Stochastic Background Structural Discriminator
   8
   9This module supplies the theorem-grade algebraic part of the PTA stochastic
  10background discriminator.  The structural RS signature is the same rung-44
  11positive scale `φ^(-44)` used elsewhere in the gravity/cosmology bridge.  A
  12zero inflation-baseline proposition is therefore structurally distinct from
  13the RS signature.
  14
  15This does not attach a PTA dataset or claim current observational separation.
  16Dataset sensitivity and channel-specific spectral fitting remain empirical
  17falsifier work.  The Lean content here is the algebraic, theorem-grade
  18inhabitant for the master theorem input
  19`PTAStochasticGWDistinctFromInflation`.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Gravity
  24namespace PTAStructural
  25
  26open Constants
  27
  28/-- Structural RS PTA stochastic-background signature at the rung-44 scale. -/
  29noncomputable def rs_pta_stochastic_phi_signature : ℝ :=
  30  Constants.phi ^ (-44 : ℤ)
  31
  32/-- Pure inflation zero-baseline proxy for the structural discriminator. -/
  33def inflation_zero_stochastic_baseline : ℝ := 0
  34
  35theorem rs_pta_stochastic_phi_signature_pos :
  36    0 < rs_pta_stochastic_phi_signature := by
  37  unfold rs_pta_stochastic_phi_signature
  38  exact zpow_pos phi_pos _
  39
  40theorem rs_pta_stochastic_phi_signature_ne_inflation_zero :
  41    rs_pta_stochastic_phi_signature ≠ inflation_zero_stochastic_baseline := by
  42  intro h
  43  have hpos := rs_pta_stochastic_phi_signature_pos
  44  unfold inflation_zero_stochastic_baseline at h
  45  rw [h] at hpos
  46  linarith
  47
  48/-- Structural PTA discriminator proposition: RS predicts a positive
  49φ-rung stochastic signature, distinct from the zero inflation-baseline proxy. -/
  50def rs_pta_distinct_inflation_prop : Prop :=
  51  0 < rs_pta_stochastic_phi_signature ∧
  52    rs_pta_stochastic_phi_signature ≠ inflation_zero_stochastic_baseline
  53
  54theorem rs_pta_distinct_inflation_prop_holds :
  55    rs_pta_distinct_inflation_prop :=
  56  ⟨rs_pta_stochastic_phi_signature_pos,
  57   rs_pta_stochastic_phi_signature_ne_inflation_zero⟩
  58
  59/-- Inhabitant for the master theorem PTA hypothesis input. -/
  60def ptaStochasticGWDistinctFromInflationWitness :
  61    MasterTheorem.PTAStochasticGWDistinctFromInflation where
  62  rs_pta_distinct_inflation := rs_pta_distinct_inflation_prop
  63  holds := rs_pta_distinct_inflation_prop_holds
  64
  65/-! ## Observable-band strengthening -/
  66
  67/-- The theorem-facing RS PTA band centered on the rung-44 stochastic signature. -/
  68def rs_pta_observable_band (x : ℝ) : Prop :=
  69  rs_pta_stochastic_phi_signature / 2 < x ∧
  70    x < (3 * rs_pta_stochastic_phi_signature) / 2
  71
  72theorem rs_pta_stochastic_phi_signature_in_observable_band :
  73    rs_pta_observable_band rs_pta_stochastic_phi_signature := by
  74  have hpos := rs_pta_stochastic_phi_signature_pos
  75  unfold rs_pta_observable_band
  76  constructor <;> nlinarith
  77
  78/-- Inflationary PTA baselines in the structural comparison class.  This class
  79is intentionally explicit: the pure inflation baseline is the zero stochastic
  80signature against which the rung-44 RS band is separated. -/
  81def inflationary_pta_family_baseline (x : ℝ) : Prop :=
  82  x = inflation_zero_stochastic_baseline
  83
  84theorem inflationary_pta_family_baseline_not_in_rs_band
  85    (x : ℝ) (hx : inflationary_pta_family_baseline x) :
  86    ¬ rs_pta_observable_band x := by
  87  intro hband
  88  rcases hband with ⟨hlow, _⟩
  89  unfold inflationary_pta_family_baseline inflation_zero_stochastic_baseline at hx
  90  subst x
  91  have hpos := rs_pta_stochastic_phi_signature_pos
  92  nlinarith
  93
  94/-- Observable-band PTA discriminator: the RS rung-44 stochastic signature lies
  95inside a positive band, while every baseline in the explicit inflationary
  96zero-signature class lies outside that band. -/
  97def rs_pta_distinct_inflation_observable_band_prop : Prop :=
  98  rs_pta_observable_band rs_pta_stochastic_phi_signature ∧
  99    ∀ x : ℝ, inflationary_pta_family_baseline x → ¬ rs_pta_observable_band x
 100
 101theorem rs_pta_distinct_inflation_observable_band_prop_holds :
 102    rs_pta_distinct_inflation_observable_band_prop :=
 103  ⟨rs_pta_stochastic_phi_signature_in_observable_band,
 104   inflationary_pta_family_baseline_not_in_rs_band⟩
 105
 106/-- Master-theorem witness strengthened from nonzero structural separation to
 107an explicit positive observable band separated from the inflationary zero
 108baseline class. -/
 109def ptaStochasticGWObservableBandWitness :
 110    MasterTheorem.PTAStochasticGWDistinctFromInflation where
 111  rs_pta_distinct_inflation := rs_pta_distinct_inflation_observable_band_prop
 112  holds := rs_pta_distinct_inflation_observable_band_prop_holds
 113
 114structure PTAStructuralCert where
 115  signature_pos : 0 < rs_pta_stochastic_phi_signature
 116  distinct_from_inflation_zero :
 117    rs_pta_stochastic_phi_signature ≠ inflation_zero_stochastic_baseline
 118  discriminator_holds : rs_pta_distinct_inflation_prop
 119  master_hypothesis_witness :
 120    MasterTheorem.PTAStochasticGWDistinctFromInflation
 121
 122noncomputable def ptaStructuralCert : PTAStructuralCert where
 123  signature_pos := rs_pta_stochastic_phi_signature_pos
 124  distinct_from_inflation_zero :=
 125    rs_pta_stochastic_phi_signature_ne_inflation_zero
 126  discriminator_holds := rs_pta_distinct_inflation_prop_holds
 127  master_hypothesis_witness := ptaStochasticGWDistinctFromInflationWitness
 128
 129theorem ptaStructuralCert_inhabited :
 130    Nonempty PTAStructuralCert :=
 131  ⟨ptaStructuralCert⟩
 132
 133/-- Track 6.B structural one-statement.  The PTA stochastic signature is
 134positive and therefore distinct from the zero inflation-baseline proxy; the
 135master theorem PTA input is inhabited. -/
 136theorem pta_structural_one_statement :
 137    (0 < rs_pta_stochastic_phi_signature) ∧
 138    (rs_pta_stochastic_phi_signature ≠ inflation_zero_stochastic_baseline) ∧
 139    rs_pta_distinct_inflation_prop ∧
 140    Nonempty MasterTheorem.PTAStochasticGWDistinctFromInflation :=
 141  ⟨rs_pta_stochastic_phi_signature_pos,
 142   rs_pta_stochastic_phi_signature_ne_inflation_zero,
 143   rs_pta_distinct_inflation_prop_holds,
 144   ⟨ptaStochasticGWDistinctFromInflationWitness⟩⟩
 145
 146end PTAStructural
 147end Gravity
 148end IndisputableMonolith
 149