Thermodynamics Boltzmann Distribution

The Boltzmann distribution

The Boltzmann distribution is a central rule of statistical mechanics. It says that for a system in contact with a heat bath at temperature T, the probability P_i that the system occupies a state with energy E_i is proportional to exp(-E_i / kT), where k is the Boltzmann constant. States with lower energy are more likely, and the exponential penalty for higher energy grows as temperature falls. The normalizing factor Z = Σ_i exp(-E_i / kT), called the partition function, ensures the probabilities sum to one. Ludwig Boltzmann introduced this form in the 1870s while studying gas kinetics; it underlies nearly all of equilibrium thermodynamics.

The distribution has two famous limits. At very high temperatures, all states become nearly equally probable. At low temperatures, the system concentrates in its lowest-energy state. For a two-level system with energy gap ΔE, the ground-state probability is 1 / (1 + exp(-βΔE)), where β = 1/kT. As T → 0, this probability approaches 1; at T → ∞ it approaches 0.5. These limits are proven in the framework's machine-checked library of formal theorems. The distribution also leads to the standard thermodynamic relations: free energy F = -kT ln Z, and entropy S = k(β⟨E⟩ + ln Z), where ⟨E⟩ is average energy.

In Recognition Science, the same distribution emerges from a different starting point. The framework models each possible state of a system as carrying a recognition cost, a number measuring how expensive it is for reality to keep that state in its ledger, a discrete record of events. The central claim is that states with lower cost are more probable, and when many subsystems interact, the cost-optimal allocation of probability takes the Boltzmann form. The framework's library defines a system as a list of energy levels with degeneracies, and defines the probability of each level as its Boltzmann factor divided by the partition function. It proves that these probabilities are nonnegative and sum to one, that the partition function is positive, and that temperature as defined by 1/β is positive.

The framework's derivation follows the same logic as standard statistical mechanics, but with recognition cost as the primitive instead of energy. The total recognition cost is held fixed, the most probable distribution maximizes the number of microstates subject to that constraint, and a Lagrange multiplier β = 1/kT appears. The framework proves the identity F = ⟨E⟩ - TS, connecting its definitions to the classical free energy. It also defines a falsifier structure: a system, a measured probability ratio, and a predicted ratio exp(-βΔE), where a deviation greater than 10 percent would count as a failure of the framework's prediction. This makes the Boltzmann form a testable claim, not merely a definitional choice.

The practical consequence is that Recognition Science does not need to assume the Boltzmann distribution as an axiom. It derives the exponential form from the forced cost function J(x) = (x + 1/x)/2 - 1, which itself follows from five plain conditions on any cost function. The framework's library proves the two-level limits and the free-energy identity as theorems. What remains open is whether the recognition-cost interpretation adds predictive power beyond the standard derivation, and whether the falsifier structure can be instantiated with real experimental data.

/-- **THEOREM**: Probabilities are non-negative. -/
theorem prob_nonneg (sys : System) (beta : ℝ) (hb : beta > 0) (i : Fin sys.levels.length) :
    probability sys beta i ≥ 0 := by
  unfold probability boltzmannFactor
  apply div_nonneg
  · apply mul_nonneg
    · exact Nat.cast_nonneg _
    · exact (exp_pos _).le
  · exact (partition_positive sys beta hb).le

/-- **THEOREM**: Probabilities sum to 1 (normalization). -/
theorem prob_normalized (sys : System) (beta : ℝ) (hb : beta > 0) :
    (Finset.univ.sum fun i => probability sys beta i) = 1 := by
  unfold probability
  simp only [div_eq_mul_inv]
  rw [← Finset.sum_mul]
  have hz : partitionFunction sys beta ≠ 0 := (partition_positive sys beta hb).ne'
  -- Sum of Boltzmann factors = partition function (by definition)
  have hsum : Finset.sum Finset.univ (fun i : Fin sys.levels.length =>
      boltzmannFactor (sys.levels.get i) beta) = partitionFunction sys beta := by
    unfold partitionFunction
    exact finset_sum_eq_list_sum sys (fun l => boltzmannFactor l beta)
  rw [hsum]
  exact mul_inv_cancel₀ hz

/-- **THEOREM**: Free energy identity F = ⟨E⟩ - TS. -/
theorem free_energy_identity (sys : System) (beta : ℝ) (hb : beta > 0) :
    freeEnergy sys beta = averageEnergy sys beta - temperature beta * entropy sys beta := by
  -- F = -T ln Z
  -- S = β⟨E⟩ + ln Z
  -- ⟨E⟩ - T*S = ⟨E⟩ - (1/β)(β⟨E⟩ + ln Z) = ⟨E⟩ - ⟨E⟩ - (1/β) ln Z = -(1/β) ln Z = F
  unfold freeEnergy entropy temperature averageEnergy
  have hb' : beta ≠ 0 := hb.ne'
  field_simp
  ring

/-- **THEOREM**: At low temperature (large β), ground state dominates.
    Proof: As β → ∞, exp(-β*gap) → 0 (for gap > 0), so prob → 1/(1+0) = 1

    Uses Real.tendsto_exp_neg_atTop_nhds_zero. -/
theorem low_temp_limit (gap : ℝ) (hg : gap > 0) :
    Filter.Tendsto (groundStateProb gap) Filter.atTop (nhds 1) := by
  unfold groundStateProb
  -- Key: exp(-β*gap) = exp(-(β*gap)) → 0 as β → ∞ (since β*gap → ∞)
  have h2 : Filter.Tendsto (fun beta => Real.exp (-beta * gap)) Filter.atTop (nhds 0) := by
    have h1 : Filter.Tendsto (fun beta : ℝ => beta * gap) Filter.atTop Filter.atTop :=
      Filter.Tendsto.atTop_mul_const hg Filter.tendsto_id
    have h1' := Real.tendsto_exp_neg_atTop_nhds_zero.comp h1
    -- Rewrite to match the function form
    convert h1' using 1
    ext beta
    simp only [Function.comp_apply, neg_mul]
  -- 1 + exp(-β*gap) → 1 + 0 = 1
  have h3 : Filter.Tendsto (fun beta => 1 + Real.exp (-beta * gap)) Filter.atTop (nhds 1) := by
    have := h2.const_add 1
    simp only [add_zero] at this
    exact this
  -- 1 / (1 + exp(-β*gap)) → 1/1 = 1
  have h4 : Filter.Tendsto (fun beta => 1 / (1 + Real.exp (-beta * gap))) Filter.atTop (nhds 1) := by
    have hne : ∀ beta : ℝ, 1 + Real.exp (-beta * gap) ≠ 0 :=
      fun _ => (add_pos_of_pos_of_nonneg one_pos (exp_pos _).le).ne'
    have hdiv : Filter.Tendsto (fun beta : ℝ => (1 : ℝ) / (1 + Real.exp (-beta * gap)))
                Filter.atTop (nhds ((1 : ℝ) / 1)) := by
      exact Filter.Tendsto.div (tendsto_const_nhds) h3 one_ne_zero
    simp only [div_one] at hdiv
    exact hdiv
  exact h4

/-- **THEOREM**: At high temperature (small β), states are equally populated.
    Proof: groundStateProb is continuous and groundStateProb(0) = 0.5.

    The rigorous proof uses continuity of the composition of continuous functions. -/
theorem high_temp_limit (gap : ℝ) (_hg : gap > 0) :
    Filter.Tendsto (groundStateProb gap) (nhds 0) (nhds 0.5) := by
  rw [← high_temp_value gap]
  unfold groundStateProb
  -- Use continuity: the function is a composition of continuous functions
  have hcont : Continuous (fun beta : ℝ => 1 / (1 + Real.exp (-beta * gap))) := by
    refine Continuous.div continuous_const ?_ (fun x => ?_)
    · exact continuous_const.add (Real.continuous_exp.comp (continuous_neg.mul continuous_const))
    · have : 1 + Real.exp (-x * gap) > 0 := add_pos_of_pos_of_nonneg one_pos (exp_pos _).le
      exact this.ne'
  exact hcont.continuousAt.tendsto

/-- **THEOREM**: Free energy identity F = ⟨E⟩ - TS. -/
theorem free_energy_identity (sys : System) (beta : ℝ) (hb : beta > 0) :
    freeEnergy sys beta = averageEnergy sys beta - temperature beta * entropy sys beta := by
  -- F = -T ln Z
  -- S = β⟨E⟩ + ln Z
  -- ⟨E⟩ - T*S = ⟨E⟩ - (1/β)(β⟨E⟩ + ln Z) = ⟨E⟩ - ⟨E⟩ - (1/β) ln Z = -(1/β) ln Z = F
  unfold freeEnergy entropy temperature averageEnergy
  have hb' : beta ≠ 0 := hb.ne'
  field_simp
  ring

What this page does not claim

The framework does not prove that the Boltzmann distribution is the only possible distribution for all systems. The framework does not claim that recognition cost is physically observable independently of energy. The framework does not derive the value of the Boltzmann constant k.

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/BoltzmannDistribution.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: