sync_resource_functional_minimized

formal source

 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 : ℝ))
 150
 151/-- A direct formalization of the paper's last step:
 152`Δθ = 2π` holds iff `D=3` for the substituted closed-form apsidal angle. -/
 153theorem kepler_selection_principle (D : ℕ) :
 154    apsidalAngle D = 2 * Real.pi ↔ D = 3 := by
 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