558 unfold log_charge uniform_config 559 simp only [Real.log_exp] 560 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, 561 nsmul_eq_mul, mul_div_cancel₀] 562 exact Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN) 563 564/-- **Theorem (Explicit Solution)**: 565 For any configuration c with log-charge σ, the uniform configuration 566 with charge σ is the variational successor. 567 568 This is the explicit "equation of motion": 569 entries(t+1) = [exp(σ/N), exp(σ/N), ..., exp(σ/N)] 570 where σ = ∑ᵢ log(entries(t)ᵢ). 571 572 The uniform distribution minimizes total J-cost subject to fixed 573 log-sum (by Jensen's inequality on the convex function J). -/
depends on (16)
Lean names referenced from this declaration's body.