entropy
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.