def
definition
carrier_frequency
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Engineering.AsteroidTrajectoryShaping on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
36/-! ## §1. Carrier and impulse -/
37
38/-- Drive carrier frequency = `5 · φ Hz`. -/
39def carrier_frequency : ℝ := 5 * phi
40
41theorem carrier_frequency_pos : 0 < carrier_frequency := by
42 unfold carrier_frequency; exact mul_pos (by norm_num) phi_pos
43
44theorem carrier_frequency_band :
45 (8.05 : ℝ) < carrier_frequency ∧ carrier_frequency < 8.10 := by
46 unfold carrier_frequency
47 have h1 := phi_gt_onePointSixOne
48 have h2 := phi_lt_onePointSixTwo
49 refine ⟨by linarith, by linarith⟩
50
51/-- Per-cycle impulse coefficient (dimensionless analogue): scales
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