variational_step_exists

formal source

 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 μ
 277    exact hbound
 278
 279/-! ## Uniqueness of the Variational Step -/
 280
 281/-- **Theorem (Variational Step Uniqueness)**:
 282    If two configurations both minimize total defect over the feasible set,
 283    they are identical.
 284
 285    Proof uses strict convexity of J: if c₁ ≠ c₂ both minimize total J-cost,
 286    their midpoint (adjusted to satisfy the constraint) would have strictly
 287    lower cost, contradicting minimality.
 288
 289    This is the core determinism result: the next state is UNIQUE. -/
 290theorem variational_step_unique {N : ℕ} (hN : 0 < N)
 291    (c : Configuration N)
 292    (next₁ next₂ : Configuration N)