`deflection_double`

proved

show as: view math explainer →

module: IndisputableMonolith.Engineering.AsteroidTrajectoryShaping
domain: Engineering
line: 74 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Engineering.AsteroidTrajectoryShaping on GitHub at line 74.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.