FRB_period_strict_increasing

formal source

 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