unity_is_optimal

formal source

 243
 244/-- **Lemma**: If the current log-charge is zero, unity is feasible
 245    and achieves the global minimum. -/
 246theorem unity_is_optimal {N : ℕ} (hN : 0 < N) (c : Configuration N)
 247    (h_zero_charge : log_charge c = 0) :
 248    IsVariationalSuccessor c (unity_config N hN) := by
 249  constructor
 250  · show log_charge (unity_config N hN) = log_charge c
 251    rw [unity_log_charge_zero hN, h_zero_charge]
 252  · intro c' _
 253    rw [unity_defect_zero hN]
 254    exact total_defect_nonneg c'
 255
 256/-- **Theorem (Variational Step Existence)**:
 257    A total-defect minimizer always exists in the feasible set.
 258
 259    The proof constructs the minimizer explicitly: it is the configuration
 260    where every entry equals exp(log_charge(c) / N), distributing the
 261    conserved charge equally. This is the AM-GM-optimal configuration. -/
 262theorem variational_step_exists {N : ℕ} (hN : 0 < N)
 263    (c : Configuration N) :
 264    ∃ next : Configuration N, IsVariationalSuccessor c next := by
 265  let μ := log_charge c / N
 266  use (constant_config μ : Configuration N)
 267  constructor
 268  · show log_charge (constant_config μ : Configuration N) = log_charge c
 269    rw [constant_config_log_charge]
 270    unfold μ
 271    exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
 272  · intro c' _hc'
 273    rw [constant_config_total_defect]
 274    have hbound := total_defect_lower_bound hN c'
 275    rw [_hc'] at hbound
 276    unfold μ