deflection_pos_of_ne_zero

formal source

  77  ring
  78
  79/-- Strict positivity for `t ≠ 0`. -/
  80theorem deflection_pos_of_ne_zero {t : ℝ} (h : t ≠ 0) :
  81    0 < deflection t := by
  82  unfold deflection
  83  apply div_pos
  84  · exact mul_pos impulseCoefficient_pos (by positivity)
  85  · norm_num
  86
  87/-! ## §3. Master certificate -/
  88
  89structure AsteroidTrajectoryShapingCert where
  90  carrier_band : (8.05 : ℝ) < carrier_frequency ∧ carrier_frequency < 8.10
  91  impulse_pos : 0 < impulseCoefficient
  92  deflection_zero : deflection 0 = 0
  93  deflection_nonneg : ∀ t, 0 ≤ deflection t
  94  deflection_double : ∀ t, deflection (2 * t) = 4 * deflection t
  95  deflection_pos : ∀ {t : ℝ}, t ≠ 0 → 0 < deflection t
  96
  97def asteroidTrajectoryShapingCert : AsteroidTrajectoryShapingCert where
  98  carrier_band := carrier_frequency_band
  99  impulse_pos := impulseCoefficient_pos
 100  deflection_zero := deflection_zero
 101  deflection_nonneg := deflection_nonneg
 102  deflection_double := deflection_double
 103  deflection_pos := @deflection_pos_of_ne_zero
 104
 105/-- **ASTEROID TRAJECTORY ONE-STATEMENT.** Carrier frequency
 106`5φ ∈ (8.05, 8.10) Hz`; cumulative deflection scales as `t²` with
 107lead time; doubling lead time quadruples deflection. -/
 108theorem asteroid_one_statement :
 109    (8.05 : ℝ) < carrier_frequency ∧ carrier_frequency < 8.10 ∧
 110    (∀ t, deflection (2 * t) = 4 * deflection t) ∧