partition_function_positive
Partition function positivity guarantees that the sum over ledger-weighted configurations remains strictly positive for any positive temperature. Researchers deriving thermodynamic potentials from Recognition Science ledger structures would cite this result to ensure logarithms and derivatives are defined. The proof is a direct term-mode application of Finset.sum_pos after unfolding the definition and verifying each summand is positive via degeneracy and exponential positivity.
claimLet $sys$ be a DiscreteSystem (finite collection of energy levels with positive integer degeneracies and at least one level) and let $T > 0$. Then the partition function $Z(sys, T) > 0$.
background
The module THERMO-002 derives the partition function from RS ledger structure, where Z emerges as a sum over ledger configurations weighted by their J-cost. A DiscreteSystem is a structure recording the number of energy levels, their energies, and positive integer degeneracies, with at least one level present. Upstream results include the definition of Boltzmann constant k_B from ComputationLimitsStructure and various anchor and forcing functions from Foundation and Physics modules that feed into energy assignments.
proof idea
Unfold the definition of partitionFunction to expose the Finset sum. Construct a Nonempty witness for the index set Fin sys.numLevels using the nonempty field of sys. Apply Finset.sum_pos, proving each summand positive by multiplying the positive cast of degeneracy (via Nat.cast_pos and deg_pos) with the positive exponential (exp_pos). The nonempty hypothesis ensures the sum is taken over a nonempty set.
why it matters in Recognition Science
This positivity result underpins the definition of the Helmholtz free energy F = -k_B T ln Z and subsequent thermodynamic quantities in the module. It closes a basic well-definedness step in the derivation of thermodynamics from ledger sums in Recognition Science. No direct parent theorems are listed in the used_by graph, but it supports the sibling definitions of freeEnergy, entropy, and heatCapacity. It aligns with the framework's goal of deriving all physics from the functional equation via the forcing chain T0-T8.
scope and limits
- Does not establish positivity when T ≤ 0.
- Does not compute the explicit value of the partition function.
- Does not incorporate the J-cost function directly in the statement.
- Does not address continuous systems or infinite level counts.
formal statement (Lean)
59theorem partition_function_positive (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) :
60 partitionFunction sys T hT > 0 := by
proof body
Term-mode proof.
61 unfold partitionFunction
62 have hne : Nonempty (Fin sys.numLevels) := ⟨⟨0, sys.nonempty⟩⟩
63 apply Finset.sum_pos
64 · intro i _
65 apply mul_pos
66 · -- degeneracy ≥ 1 > 0
67 have h := sys.deg_pos i
68 exact Nat.cast_pos.mpr (Nat.lt_of_lt_of_le Nat.zero_lt_one h)
69 · exact exp_pos _
70 · exact @Finset.univ_nonempty (Fin sys.numLevels) _ hne
71
72/-! ## Thermodynamic Quantities from Z -/
73
74/-- The Helmholtz free energy F = -k_B T ln Z. -/