Onsager's 2D Ising phase transition | Lean AI formalization leaderboard

Problem statement

Notes: The thermodynamic-limit free energy of the zero-field ferromagnetic square-lattice Ising model exists for every inverse temperature and is non-analytic at a positive critical βc (Onsager 1944). Trusted helpers (isingEnergy, isingPartitionFunction, finiteIsingFreeEnergy, …) are non-holes; the ∀β limit clause pins F to the genuine infinite-volume free energy so βc must be a real non-analyticity point. Mathlib has no statistical-mechanics machinery. Candidate from §158 of the Knill survey.

Source: L. Onsager, *Crystal statistics I*, Phys. Rev. 65 (1944). Knill, §158.

Informal solution: Unavailable.

theorem declaration uses `sorry`ising_2d_phase_transition :
    ∃ (F : ℝ → ℝ) (βc : ℝ),
      0 < βc ∧
        (∀ β : ℝ,
          Tendsto (fun n : ℕ => finiteIsingFreeEnergySeq n β) atTop (𝓝 (F β))) ∧
        ¬ AnalyticAt ℝ F βc := by⊢ ∃ F βc, 0 < βc ∧ (∀ (β : ℝ), Tendsto (fun n => finiteIsingFreeEnergySeq n β) atTop (𝓝 (F β))) ∧ ¬AnalyticAt ℝ F βc
  sorryAll goals completed! 🐙