deflection_zero

formal source

  61units): `δ(t) = (impulseCoefficient · t²) / 2`. -/
  62def deflection (t : ℝ) : ℝ := (impulseCoefficient * t^2) / 2
  63
  64theorem deflection_zero : deflection 0 = 0 := by
  65  unfold deflection; simp
  66
  67theorem deflection_nonneg (t : ℝ) : 0 ≤ deflection t := by
  68  unfold deflection
  69  apply div_nonneg
  70  · exact mul_nonneg (le_of_lt impulseCoefficient_pos) (sq_nonneg _)
  71  · norm_num
  72
  73/-- Doubling lead time quadruples deflection. -/
  74theorem deflection_double (t : ℝ) :
  75    deflection (2 * t) = 4 * deflection t := by
  76  unfold deflection
  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