partition_function_positive
plain-language theorem explainer
The theorem shows that the partition function Z for any discrete system remains strictly positive at positive temperature. Modelers deriving thermodynamic potentials from ledger sums would cite it to ensure the logarithm in free energy stays defined. The proof unfolds the sum definition then applies Finset.sum_pos together with termwise positivity from degeneracy and the exponential.
Claim. Let sys be a finite discrete system whose energy levels each carry degeneracy at least 1. For any real temperature T > 0 the partition function satisfies Z(sys, T) > 0, where Z is the sum over levels of degeneracy times exp(-β E) with β = 1/(k_B T).
background
The module derives statistical mechanics from RS ledger structure. DiscreteSystem is the structure with numLevels : ℕ (strictly positive), energy and degeneracy maps on Fin numLevels, plus the axioms that numLevels > 0 and every degeneracy ≥ 1. The partition function is the finite sum Σ g_i exp(-β E_i) that encodes all thermodynamic potentials via the relations given in the module header.
proof idea
Unfold the definition of partitionFunction. Construct a witness that the index Finset is nonempty. Apply the library lemma Finset.sum_pos. For each summand invoke mul_pos on the positive real cast of degeneracy (via Nat.cast_pos and the system's deg_pos) and the library fact exp_pos.
why it matters
Positivity of Z guarantees that ln Z is defined, so the Helmholtz free energy F = -k_B T ln Z and the downstream quantities entropy and heat capacity are well-defined inside the same module. The result therefore closes the basic ledger-to-thermodynamics step described in the module doc-comment without reference to the forcing chain or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.