syncPeriod_3_eq_360

formal source

 116        exact (Nat.ne_of_lt hmul) (heq.symm)
 117
 118/-! A convenience corollary matching the paper's explicit numeric claim `lcm(8,45)=360`. -/
 119theorem syncPeriod_3_eq_360 : syncPeriod 3 = 360 := by
 120  native_decide
 121
 122/-! The paper also packages the minimization in terms of a resource functional
 123\(\mathcal{F}(D,45)=\alpha\,\mathrm{lcm}(2^D,45)+\beta D\) with \(\alpha>0,\beta\ge0\).
 124We record that consequence here. -/
 125
 126/-- If `α>0` and `β≥0`, then the resource functional
 127`F(D)=α * lcm(2^D,45) + β * D` is minimized at `D=3` among `D≥3`. -/
 128theorem sync_resource_functional_minimized (α β : ℝ) (hα : 0 < α) (hβ : 0 ≤ β)
 129    {D : ℕ} (hD : 3 ≤ D) :
 130    α * (syncPeriod 3 : ℝ) + β * (3 : ℝ) ≤ α * (syncPeriod D : ℝ) + β * (D : ℝ) := by
 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). -/
 148noncomputable def apsidalAngle (D : ℕ) : ℝ :=
 149  (2 * Real.pi) / Real.sqrt (4 - (D : ℝ))