Pith. sign in
module module high

IndisputableMonolith.Thermodynamics.PartitionFunction

show as:
view Lean formalization →

This module defines the partition function and derived thermodynamic quantities such as free energy, entropy, and heat capacity for discrete systems using the J-cost from the Cost module. Researchers deriving statistical mechanics results within Recognition Science would reference these definitions. The module consists of definitions and basic properties with no complex proofs.

claim$k_B$ (Boltzmann constant), $\beta$ (inverse temperature), DiscreteSystem (finite collection of states with J-costs), partitionFunction $Z = \sum \exp(-\beta \cdot \text{energyFromJCost}(s))$, freeEnergy $F = -k_B T \ln Z$, averageEnergy, entropy $S$, heatCapacity.

background

The module imports the fundamental RS time quantum $\tau_0 = 1$ tick from Constants and the J-cost function from the Cost module. It introduces DiscreteSystem as a structure for finite sets of states each assigned a J-cost, then defines $k_B$, $\beta$, the partition function as the sum of Boltzmann factors over states, and the standard thermodynamic potentials derived from it. The module doc-comment identifies the Boltzmann constant as a central object.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the thermodynamic definitions that connect the J-cost ledger to ensemble averages and potentials. It supports later derivations of thermodynamic relations that tie into the forcing chain (T5 J-uniqueness through T8 D=3) and Recognition Composition Law. No specific parent theorems are recorded in the used_by edges.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (21)