BIT_carrier_period_pos

formal source

  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