free_energy_identity
plain-language theorem explainer
The free energy identity equates the Helmholtz free energy of a discrete energy-level system to its average energy minus temperature times entropy. Thermodynamic derivations within Recognition Science cite it to link J-cost minimization to classical potentials. The proof is a direct term-mode reduction that unfolds the four definitions, clears the nonzero beta hypothesis, and normalizes via field simplification followed by ring arithmetic.
Claim. For a system with energy levels and inverse temperature $beta > 0$, the free energy satisfies $F = averageEnergy - temperature(beta) * entropy$, where temperature is $1/beta$.
background
In the BoltzmannDistribution module a System is a nonempty list of EnergyLevel structures. The J-cost from PhiForcingDerived supplies the primitive recognition cost whose minimization under ledger balance yields the partition function and Boltzmann weights. Entropy is imported from InitialCondition as total defect of a configuration, with zero defect giving the minimum-entropy state. Temperature and averageEnergy are defined locally from beta and the weighted sum over levels.
proof idea
Term-mode proof. Unfold freeEnergy, entropy, temperature and averageEnergy. Introduce the auxiliary fact beta ≠ 0 from the positivity hypothesis. Apply field_simp to clear denominators, then ring to obtain the algebraic identity.
why it matters
Supplies the free_energy_identity used by HelmholtzRealCert to certify discrete Boltzmann entropy and by free_energy_is_natural to show the decomposition F = ⟨J⟩ − T S is the natural quantity from average J-cost plus Shannon entropy. It bridges J-uniqueness (T5) to thermodynamic potentials and supports the forcing chain through the eight-tick octave. It touches the open embedding of continuous spectra into the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.