pith. machine review for the scientific record. sign in
def definition def or abbrev high

entropy

show as:
view Lean formalization →

Defines entropy of a system as beta times average energy plus the log of the partition function. Workers deriving holographic bounds or the arrow of time from J-cost would cite this expression when moving from microscopic recognition cost to thermodynamic entropy. The definition is a direct one-line transcription of the standard relation S = β⟨E⟩ + ln Z in units with k_B = 1.

claimFor a system consisting of a nonempty list of energy levels, the entropy at inverse temperature β is S = β ⟨E⟩ + ln Z, where ⟨E⟩ is the expectation value of energy under the Boltzmann weights and Z is the sum of those weights.

background

The module derives the Boltzmann distribution from the J-cost functional of Recognition Science. A System is a structure holding a nonempty list of EnergyLevel records; each level carries an energy value used to build the partition function Z = Σ exp(-β E_i) and the average energy ⟨E⟩ = Σ E_i exp(-β E_i) / Z. The supplied entropy definition sits downstream of the defect-based entropy in InitialCondition, where entropy equals total_defect of a configuration, and of the anchor maps Z and F that assign integer charges to particle species.

proof idea

The definition is a one-line algebraic expression that directly implements the thermodynamic identity S = β⟨E⟩ + ln Z. It composes the already-defined averageEnergy and partitionFunction on the System structure; no tactics or lemmas are invoked beyond the Real.log and multiplication primitives.

why it matters in Recognition Science

This definition supplies the entropy functional referenced by cone_entropy_bound (which asserts entropy ≤ area / (4 λ_rec²)) and by initial_state_minimum_entropy (which shows the ground state has minimal entropy). It completes the THERMO-001 derivation of Boltzmann statistics from J-cost minimization and feeds the ArrowOfTime result that entropy increase is asymmetric. The placement links the eight-tick octave and phi-ladder mass formula to thermodynamic selection in cosmology.

scope and limits

formal statement (Lean)

 203noncomputable def entropy (sys : System) (beta : ℝ) : ℝ :=

proof body

Definition body.

 204  beta * averageEnergy sys beta + Real.log (partitionFunction sys beta)
 205
 206/-- Free energy F = -kT ln Z = ⟨E⟩ - TS. -/

used by (40)

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

… and 10 more

depends on (17)

Lean names referenced from this declaration's body.