Thermodynamics Phase Transitions

Phase transitions as cost bifurcations

A phase transition is a dramatic change in the physical properties of a material. Melting ice, boiling water, and the sudden appearance of magnetization in iron are everyday examples. These transitions are classified by how the properties change. A first-order transition, like melting, is discontinuous: the density, entropy, and other properties jump abruptly. A second-order transition, like the onset of superconductivity, is continuous but singular: the properties change smoothly, yet quantities like the specific heat diverge at the transition temperature. A critical point marks the end of a first-order transition line, where the distinction between phases vanishes.

In the standard Landau theory of phase transitions, the state of a system is described by an order parameter, a quantity that is zero in one phase and nonzero in another. For a ferromagnet, the order parameter is magnetization; for a liquid-gas system, it is the density difference. The equilibrium state is found by minimizing a free energy function of this order parameter. The shape of this function changes with temperature, and when its minimum shifts from zero to a nonzero value, a transition occurs.

In Recognition Science, the framework models phase transitions as bifurcations in a cost function. The central object is the cost, a measure of the price of recognition, and its behavior is defined by the function jcostLandscape(m, T) = (T - 1) * m^2 + m^4 / 4, where m is an order parameter and T is a control parameter like temperature. This is a Landau-like form, and the framework's library of machine-checked formal theorems proves that for T > 1, the function has a unique minimum at m = 0. For T < 1, the function has two symmetric minima at nonzero values of m, a result that requires calculus and is stated as a target. The framework therefore defines phases as minima of the cost function, a first-order transition as a jump between minima, and a second-order transition as the merging of minima.

The framework also provides structures to describe the phenomena that accompany these transitions. A first-order transition is characterized by latent heat, a volume change, and hysteresis, which allows for supercooling and superheating. A metastable state is a local minimum of the cost function that is not the global minimum, and its lifetime is set by a nucleation rate. The framework defines a nucleation rate as exp(-barrier / (kB_SI * T)), which is the Arrhenius form, where the barrier is the height of the cost barrier between minima. A quantum phase transition is a transition driven by a control parameter other than temperature, such as pressure or magnetic field, at zero temperature, with examples including the Mott insulator-metal transition and superconductor-insulator transitions.

The framework's library proves that the cost function is zero at m = 0 and positive for T > 1 when m is nonzero. It also states, as targets, theorems for the mechanisms of first-order and second-order transitions, and for spontaneous symmetry breaking, where a symmetric cost function leads to an asymmetric ground state. The framework includes a falsifier structure, which states that the model is falsified if there is no cost interpretation for a phase transition or if a critical point contradicts the framework's predictions. The framework's summary is that phases are cost minima, first-order transitions are jumps between minima, second-order transitions are merging minima, and nucleation is barrier crossing.

/-- For T > 1 and m ≠ 0, the J-cost is positive.
    This means m = 0 is the unique minimum (disordered phase). -/
theorem jcost_positive_for_T_gt_1 (m T : ℝ) (hT : T > 1) (hm : m ≠ 0) :
    jcostLandscape m T > 0 := by
  unfold jcostLandscape
  have hm_sq_pos : m^2 > 0 := sq_pos_of_ne_zero hm
  have hcoef_pos : T - 1 > 0 := by linarith
  have h1 : (T - 1) * m^2 > 0 := mul_pos hcoef_pos hm_sq_pos
  have h2 : m^4 / 4 ≥ 0 := by positivity
  linarith

/-- Nucleation: Crossing the J-cost barrier.

    Thermal fluctuations can push system over barrier.
    Rate ~ exp(-ΔJ/kT) where ΔJ = barrier height. -/
noncomputable def nucleationRate (barrier : ℝ) (T : ℝ) (hT : T > 0) : ℝ :=
  exp (-barrier / (kB_SI * T))

What this page does not claim

The framework does not prove that the cost function has two nonzero minima for T < 1. The framework does not derive the values of critical exponents or universality classes. The framework does not provide a physical derivation of the cost function from a microscopic Hamiltonian.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Thermodynamics/PhaseTransitions.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: