`impulseCoefficient_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.AsteroidTrajectoryShaping on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  52with carrier frequency. -/
  53def impulseCoefficient : ℝ := carrier_frequency
  54
  55theorem impulseCoefficient_pos : 0 < impulseCoefficient :=
  56  carrier_frequency_pos
  57
  58/-! ## §2. Cumulative deflection -/
  59
  60/-- Cumulative deflection at lead time `t` (in seconds, dimensionless
  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

papers checked against this theorem

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