theorem
proved
tactic proof
sync_resource_functional_minimized
show as:
view Lean formalization →
formal statement (Lean)
128theorem sync_resource_functional_minimized (α β : ℝ) (hα : 0 < α) (hβ : 0 ≤ β)
129 {D : ℕ} (hD : 3 ≤ D) :
130 α * (syncPeriod 3 : ℝ) + β * (3 : ℝ) ≤ α * (syncPeriod D : ℝ) + β * (D : ℝ) := by
proof body
Tactic-mode proof.
131 have hsyncNat : syncPeriod 3 ≤ syncPeriod D := (synchronization_selection_principle (D := D) hD).1
132 have hsync : (syncPeriod 3 : ℝ) ≤ (syncPeriod D : ℝ) := by
133 exact_mod_cast hsyncNat
134 have hdim : (3 : ℝ) ≤ (D : ℝ) := by
135 exact_mod_cast hD
136 have h1 : α * (syncPeriod 3 : ℝ) ≤ α * (syncPeriod D : ℝ) :=
137 mul_le_mul_of_nonneg_left hsync (le_of_lt hα)
138 have h2 : β * (3 : ℝ) ≤ β * (D : ℝ) :=
139 mul_le_mul_of_nonneg_left hdim hβ
140 linarith
141
142/-! ## Constraint (K): Kepler non-precession (algebraic core) -/
143
144open Real
145
146/-- The apsidal-angle formula used in `Draft_v1.tex` after substituting the Green-kernel power
147law: `Δθ(D) = 2π / √(4 - D)` (with `D` treated as a real parameter). -/