equilibrium_attractive

formal source

 538
 539    The defect sequence {total_defect(traj(t))} is monotone decreasing
 540    and bounded below, hence convergent. -/
 541theorem equilibrium_attractive {N : ℕ}
 542    (traj : Trajectory N)
 543    (h : IsVariationalTrajectory traj) :
 544    (∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t)) ∧
 545    (∀ t, 0 ≤ total_defect (traj t)) :=
 546  ⟨trajectory_defect_monotone traj h, fun t => total_defect_nonneg (traj t)⟩
 547
 548/-! ## The Uniform Minimizer (Explicit Solution) -/
 549
 550/-- The uniform configuration with charge σ: all entries equal exp(σ/N). -/
 551noncomputable def uniform_config {N : ℕ} (hN : 0 < N) (σ : ℝ) : Configuration N :=
 552  { entries := fun _ => Real.exp (σ / N)
 553    entries_pos := fun _ => Real.exp_pos _ }
 554
 555/-- The uniform configuration has the correct log-charge. -/
 556theorem uniform_config_charge {N : ℕ} (hN : 0 < N) (σ : ℝ) :
 557    log_charge (uniform_config hN σ) = σ := by
 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