unity_log_charge_zero

formal source

 235
 236/-- **Lemma**: The unity configuration (all entries = 1) has zero total defect
 237    and zero log-charge. -/
 238theorem unity_log_charge_zero {N : ℕ} (hN : 0 < N) :
 239    log_charge (unity_config N hN) = 0 := by
 240  unfold log_charge unity_config
 241  simp only [Real.log_one]
 242  exact Finset.sum_const_zero
 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