entropy
plain-language theorem explainer
Entropy for a discrete system at positive temperature equals k_B times the sum of the natural log of the partition function and beta times the average energy. Cosmologists and information theorists working in Recognition Science cite this when linking ledger J-costs to the second law or holographic bounds. The definition is a direct algebraic transcription of the standard statistical mechanics formula using the module's partitionFunction and averageEnergy.
Claim. $S = k_B (ln Z + β ⟨E⟩)$ where $Z$ is the partition function of the discrete system at temperature $T > 0$ and ⟨E⟩ is the mean energy.
background
The Thermodynamics.PartitionFunction module derives the partition function Z as a sum over ledger configurations weighted by J-cost, per the module documentation. DiscreteSystem is a structure with numLevels energy levels, an energy map, and a degeneracy map, requiring numLevels > 0 and degeneracy ≥ 1 for each level. Upstream results include the Boltzmann constant k_B from ComputationLimitsStructure (with its Landauer energy theorem) and the entropy definition from Foundation.InitialCondition, which states that entropy of a configuration is proportional to its total defect with zero defect yielding the minimum entropy state.
proof idea
The definition is a one-line wrapper that directly substitutes the module's partitionFunction and averageEnergy into the standard formula S = k_B (ln Z + β ⟨E⟩).
why it matters
This definition supplies the entropy expression used by downstream results including cone_entropy_bound in ConeExport.Theorem (bounding entropy by area over 4 λ_rec²) and initial_state_minimum_entropy in Foundation.InitialCondition. It completes the THERMO-002 target of extracting thermodynamic quantities from RS ledger structure. In the framework it connects J-cost minimization to the arrow of time and holographic bounds without invoking the full forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.