theorem
proved
tactic proof
kepler_selection_principle
show as:
view Lean formalization →
formal statement (Lean)
153theorem kepler_selection_principle (D : ℕ) :
154 apsidalAngle D = 2 * Real.pi ↔ D = 3 := by
proof body
Tactic-mode proof.
155 constructor
156 · intro h
157 have hpi : (2 * Real.pi) ≠ 0 := by
158 exact mul_ne_zero (by norm_num) Real.pi_ne_zero
159 -- Let x be the denominator √(4 - D).
160 set x : ℝ := Real.sqrt (4 - (D : ℝ))
161 have hx : x ≠ 0 := by
162 intro hx0
163 have : apsidalAngle D = 0 := by
164 simp [apsidalAngle, x, hx0]
165 have h0 : 0 = 2 * Real.pi := by
166 simpa [this] using h
167 exact hpi h0.symm
168 -- Rewrite h as (2π) * x⁻¹ = 2π, then cancel.
169 have h' : (2 * Real.pi) * x⁻¹ = 2 * Real.pi := by
170 simpa [apsidalAngle, x, div_eq_mul_inv] using h
171 have hmul : (2 * Real.pi) * (x⁻¹ * x) = (2 * Real.pi) * x := by
172 -- multiply both sides by x
173 simpa [mul_assoc] using congrArg (fun t => t * x) h'
174 have hmul' : (2 * Real.pi) = (2 * Real.pi) * x := by
175 simpa [mul_assoc, inv_mul_cancel₀ hx, mul_one] using hmul
176 -- cancel 2π to get x = 1
177 have hx1 : x = 1 := by
178 have hcancel : (2 * Real.pi) * x = (2 * Real.pi) * 1 := by
179 calc
180 (2 * Real.pi) * x = (2 * Real.pi) := by simpa [mul_assoc] using hmul'.symm
181 _ = (2 * Real.pi) * 1 := by simp
182 exact mul_left_cancel₀ hpi hcancel
183 -- show 0 ≤ 4 - D so we can square the sqrt
184 have hnonneg : 0 ≤ 4 - (D : ℝ) := by
185 by_contra hneg
186 have hle : 4 - (D : ℝ) ≤ 0 := le_of_not_ge hneg
187 have : Real.sqrt (4 - (D : ℝ)) = 0 := Real.sqrt_eq_zero_of_nonpos hle
188 -- but x = sqrt(...) = 1
189 have : (1 : ℝ) = 0 := by simpa [x, hx1] using this
190 exact one_ne_zero this
191 have hsq : x ^ 2 = 4 - (D : ℝ) := by
192 simpa [x, pow_two] using (Real.sq_sqrt hnonneg)
193 -- x=1 => 4 - D = 1 => D = 3
194 have hreal : (D : ℝ) = 3 := by
195 have : (1 : ℝ) ^ 2 = 4 - (D : ℝ) := by simpa [hx1] using hsq
196 nlinarith
197 -- cast-injectivity to return to ℕ
198 exact (Nat.cast_injective (R := ℝ) (by simpa using hreal))
199 · intro hD
200 subst hD
201 have : (4 - (3 : ℝ)) = (1 : ℝ) := by norm_num
202 simp [apsidalAngle, this]
203
204/-! ## Paper Packaging: Dimensional Rigidity (T/K/S) -/
205
206/-- Paper-style (S) constraint: `D` is admissible (`D ≥ 3`) and is a minimizer of `syncPeriod`. -/