pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Thermodynamics.HelmholtzReal

show as:
view Lean formalization →

This module defines the partition function over discrete energy levels together with Boltzmann probabilities and the real Helmholtz free energy in the Recognition Science setting. Researchers constructing variational free energy from the recognition composition law cite these objects to ground thermodynamic quantities. The module supplies a set of definitions and elementary positivity and normalization lemmas.

claimFor a discrete set of energies $E_i$, the partition function is $Z = sum_i exp(-beta E_i)$. Boltzmann probabilities are $p_i = exp(-beta E_i)/Z$, and the Helmholtz free energy is $F = -kT log Z$ satisfying $F = E - TS$.

background

The module imports the RS time quantum tau_0 = 1 tick from Constants and the cost structure from Cost, together with FreeEnergy primitives. It introduces the partition function for discrete energy level sets, Boltzmann probabilities, expected energy, Boltzmann entropy, and the Helmholtz free energy with the relation F = E - TS. These objects operate in RS-native units where c = 1 and the phi-ladder supplies the mass and energy scales.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the thermodynamic primitives that feed into VariationalFreeEnergyFromRCL. There the Friston VFE is realized as E_q[E] + KL[q || p_prior] with monotone descent under ledger updates. It therefore connects the RS cost structure to the statistical mechanics needed for variational inference on finite recognition partitions.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (12)