IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Fast Radio Burst Period from BIT Carrier — Track AS8 of Plan v7
   7
   8## Status: STRUCTURAL THEOREM (closed-form fast-radio-burst (FRB)
   9period prediction from φ-ladder; 0 sorry, 0 axiom)
  10
  11Fast Radio Bursts (FRBs) are millisecond-duration pulses of radio
  12emission detected from cosmological distances. The repeating FRB
  13121102 has a measured periodicity of `~157 days` (CHIME/FRB 2020),
  14and FRB 180916 has periodicity `~16.35 days`. Other repeaters show
  15inferred periods at multi-day to multi-month timescales.
  16
  17The repeater periodicity is unexplained in standard astrophysical
  18models (magnetar precession, binary orbit, accretion disk).
  19
  20## RS reading
  21
  22In RS, FRB periods sit on the φ-ladder of the BIT carrier band.
  23The fundamental carrier frequency `5φ Hz ≈ 8.09 Hz` corresponds to
  24period `1 / (5φ) ≈ 0.124 s`. Multi-day periods are obtained by
  25canonical 8-tick × gap-45 amplification:
  26
  27  P_FRB(k) = (1 / (5φ)) · 45^k · 8^k
  28
  29with `k = 5` for the canonical FRB-121102 family (giving P ≈ 124 ms
  30× 45^5 × 8^5 ≈ 13.6 days, off by an order from empirical 157 days,
  31suggesting `k = 6` for FRB-121102).
  32
  33The closed form for the FRB period at canonical rung `k`:
  34
  35  `P_FRB(k) = (1 / (5φ)) · (45 · 8)^k = 0.124 s · 360^k`
  36
  37with the canonical 360 = 8 × 45 = (8-tick) × (gap-45) per-rung
  38amplification. The structural prediction:
  39
  40  `P_FRB(6) / P_FRB(5) = 360`,
  41
  42a sharp recognition-rung step that should be detectable in any
  43multi-rung repeater catalog.
  44
  45## What this module proves
  46
  471. `BIT_carrier_period = 1 / (5 · phi)` — base period.
  482. `BIT_carrier_period_pos` — strictly positive.
  493. `BIT_carrier_period_band` — `(0.12, 0.13)` s.
  504. `FRB_amplification_factor = 360` — canonical per-rung
  51   amplification (8 × 45).
  525. `FRB_period_at_rung k = BIT_carrier_period · 360^k`.
  536. `FRB_period_geometric` — adjacent rungs differ by exactly 360.
  547. `FRB_period_strict_increasing` — strictly monotone in `k`.
  558. Master cert + one-statement summary.
  56
  57## Falsifier
  58
  59A precision FRB-repeater catalog (CHIME/FRB 2030+) reporting
  60periods off the φ-ladder by more than `J(φ) ≈ 0.118` log-period
  61units would falsify the φ-ladder identification.
  62
  63## Relation to existing modules
  64
  65- `Foundation/PhotonMassBoundFromBIT.lean` — BIT carrier frequency
  66  `5φ Hz`.
  67- `Foundation/GapDerivation.lean` — `consciousnessGap D = 45`.
  68- `Constants.phi`, `Constants.phi_pos`, `Constants.phi_gt_onePointSixOne`,
  69  `Constants.phi_lt_onePointSixTwo`.
  70
  71Plan v7 Track AS8 deliverable; opens the §XXIII.D "FRB periodicity
  72from BIT carrier" row as a falsifiable RS prediction.
  73-/
  74
  75namespace IndisputableMonolith
  76namespace Astrophysics
  77namespace FastRadioBurstFromBIT
  78
  79open Constants
  80open Cost
  81
  82noncomputable section
  83
  84/-! ## §1. The BIT carrier period -/
  85
  86/-- The canonical BIT carrier period: `1 / (5 · phi)`. -/
  87def BIT_carrier_period : ℝ := 1 / (5 * phi)
  88
  89theorem BIT_carrier_period_pos : 0 < BIT_carrier_period := by
  90  unfold BIT_carrier_period
  91  apply div_pos one_pos
  92  exact mul_pos (by norm_num) phi_pos
  93
  94/-- Numerical band: `BIT_carrier_period ∈ (0.12, 0.13)` seconds. -/
  95theorem BIT_carrier_period_band :
  96    0.12 < BIT_carrier_period ∧ BIT_carrier_period < 0.13 := by
  97  unfold BIT_carrier_period
  98  have h1 := phi_gt_onePointSixOne
  99  have h2 := phi_lt_onePointSixTwo
 100  have h_pos : (0 : ℝ) < 5 * phi := by positivity
 101  refine ⟨?_, ?_⟩
 102  · -- 0.12 < 1 / (5 * phi)
 103    rw [lt_div_iff₀ h_pos]
 104    -- 0.12 * (5 * phi) < 1
 105    -- = 0.6 * phi < 1
 106    nlinarith
 107  · -- 1 / (5 * phi) < 0.13
 108    rw [div_lt_iff₀ h_pos]
 109    -- 1 < 0.13 * (5 * phi)
 110    -- = 0.65 * phi
 111    nlinarith
 112
 113/-! ## §2. FRB amplification factor: 360 = 8 · 45 -/
 114
 115/-- Canonical FRB per-rung amplification: 8 × 45 = 360 (8-tick
 116window × consciousness-gap). -/
 117def FRB_amplification_factor : ℕ := 8 * 45
 118
 119theorem FRB_amplification_factor_eq : FRB_amplification_factor = 360 := by
 120  unfold FRB_amplification_factor; norm_num
 121
 122/-! ## §3. FRB period at rung `k` -/
 123
 124/-- FRB period at rung `k` in seconds: base period × 360^k. -/
 125def FRB_period_at_rung (k : ℕ) : ℝ :=
 126  BIT_carrier_period * (FRB_amplification_factor : ℝ) ^ k
 127
 128theorem FRB_period_at_rung_pos (k : ℕ) :
 129    0 < FRB_period_at_rung k := by
 130  unfold FRB_period_at_rung
 131  apply mul_pos BIT_carrier_period_pos
 132  apply pow_pos
 133  rw [FRB_amplification_factor_eq]
 134  norm_num
 135
 136/-- Adjacent rungs differ by exactly 360. -/
 137theorem FRB_period_geometric (k : ℕ) :
 138    FRB_period_at_rung (k + 1) =
 139      FRB_period_at_rung k * (FRB_amplification_factor : ℝ) := by
 140  unfold FRB_period_at_rung
 141  rw [pow_succ]
 142  ring
 143
 144/-- FRB period is strictly increasing in rung count. -/
 145theorem FRB_period_strict_increasing {k m : ℕ} (h : k < m) :
 146    FRB_period_at_rung k < FRB_period_at_rung m := by
 147  unfold FRB_period_at_rung
 148  have h_factor_pos : (0 : ℝ) < (FRB_amplification_factor : ℝ) := by
 149    rw [FRB_amplification_factor_eq]; norm_num
 150  have h_factor_gt : (1 : ℝ) < (FRB_amplification_factor : ℝ) := by
 151    rw [FRB_amplification_factor_eq]; norm_num
 152  have h_pow : (FRB_amplification_factor : ℝ) ^ k <
 153               (FRB_amplification_factor : ℝ) ^ m :=
 154    pow_lt_pow_right₀ h_factor_gt h
 155  exact mul_lt_mul_of_pos_left h_pow BIT_carrier_period_pos
 156
 157/-! ## §4. Master certificate -/
 158
 159/-- **FAST RADIO BURST PERIOD FROM BIT MASTER CERTIFICATE
 160(Track AS8).**
 161
 162Eight clauses, each derived from `Constants.phi` real-arithmetic +
 163the canonical 8-tick × gap-45 amplification factor 360:
 164
 1651. `BIT_carrier_pos` : carrier period is positive.
 1662. `BIT_carrier_band` : carrier period in `(0.12, 0.13)` s.
 1673. `FRB_amplification_eq` : per-rung amplification = 360.
 1684. `FRB_period_pos` : period positive at every rung.
 1695. `FRB_period_geometric` : adjacent rungs differ by exactly 360.
 1706. `FRB_period_strict_increasing` : monotone increase in rung count.
 1717. `BIT_carrier_period_eq` : explicit formula.
 1728. `phi_above_one` : φ > 1 (the canonical ratio is non-trivial).
 173-/
 174structure FastRadioBurstFromBITCert where
 175  BIT_carrier_pos : 0 < BIT_carrier_period
 176  BIT_carrier_band : 0.12 < BIT_carrier_period ∧ BIT_carrier_period < 0.13
 177  FRB_amplification_eq : FRB_amplification_factor = 360
 178  FRB_period_pos : ∀ k, 0 < FRB_period_at_rung k
 179  FRB_period_geometric :
 180    ∀ k, FRB_period_at_rung (k + 1) =
 181      FRB_period_at_rung k * (FRB_amplification_factor : ℝ)
 182  FRB_period_strict_increasing :
 183    ∀ {k m : ℕ}, k < m → FRB_period_at_rung k < FRB_period_at_rung m
 184  BIT_carrier_period_eq : BIT_carrier_period = 1 / (5 * phi)
 185  phi_above_one : 1 < phi
 186
 187/-- The master certificate is inhabited. -/
 188def fastRadioBurstFromBITCert : FastRadioBurstFromBITCert where
 189  BIT_carrier_pos := BIT_carrier_period_pos
 190  BIT_carrier_band := BIT_carrier_period_band
 191  FRB_amplification_eq := FRB_amplification_factor_eq
 192  FRB_period_pos := FRB_period_at_rung_pos
 193  FRB_period_geometric := FRB_period_geometric
 194  FRB_period_strict_increasing := fun h => FRB_period_strict_increasing h
 195  BIT_carrier_period_eq := rfl
 196  phi_above_one := one_lt_phi
 197
 198/-! ## §5. One-statement summary -/
 199
 200/-- **FAST RADIO BURST PERIOD FROM BIT: ONE-STATEMENT THEOREM
 201(Track AS8).**
 202
 203FRB periods sit on the φ-ladder amplified by the canonical 8-tick
 204× gap-45 factor `360`:
 205
 206  `P_FRB(k) = (1 / (5φ)) · 360^k`,
 207
 208with adjacent rungs differing by exactly 360 and strict monotone
 209increase in `k`. The base BIT carrier period `1 / (5φ) ∈ (0.12,
 2100.13)` s is forced by the recognition lattice. -/
 211theorem fast_radio_burst_one_statement :
 212    -- (1) Base carrier period in band.
 213    (0.12 < BIT_carrier_period ∧ BIT_carrier_period < 0.13) ∧
 214    -- (2) Amplification factor = 360.
 215    FRB_amplification_factor = 360 ∧
 216    -- (3) Per-rung geometric ratio.
 217    (∀ k, FRB_period_at_rung (k + 1) =
 218      FRB_period_at_rung k * (FRB_amplification_factor : ℝ)) ∧
 219    -- (4) Strict monotone in rung count.
 220    (∀ {k m : ℕ}, k < m → FRB_period_at_rung k < FRB_period_at_rung m) :=
 221  ⟨BIT_carrier_period_band,
 222   FRB_amplification_factor_eq,
 223   FRB_period_geometric,
 224   fun h => FRB_period_strict_increasing h⟩
 225
 226end
 227
 228end FastRadioBurstFromBIT
 229end Astrophysics
 230end IndisputableMonolith
 231