freeEnergy
plain-language theorem explainer
Defines the RS free energy of a Gibbs policy on a moral state over a finite menu of virtue actions: F_R = -T_R log Z, with Z the partition function. Thermodynamic RL and Boltzmann-bridge proofs cite it as the Helmholtz potential whose minimizer is the Gibbs policy. The body is a one-line noncomputable abbreviation of that formula.
Claim. For a Gibbs policy $g$ (recognition temperature $T_R>0$ and cost $J$), moral state $s$, and finite list of virtue actions, the free energy is $F_R(g,s,\mathrm{actions})=-T_R\,\log Z_g(s,\mathrm{actions})$, where $Z_g$ is the partition function of $g$.
background
The module is the RS→RL bridge: moral states carry skew, energy budget, value, and harm; actions are 14-coefficient vectors on the DREAM virtue generators; hard σ=0 feasibility is enforced by LACompletion. Learning uses a Gibbs policy $p(a|s)\propto\exp(-J(s,a)/T_R)$, the RS thermodynamic form of max-ent RL.
GibbsPolicy packages a positive recognition temperature temp_R and a cost map $J:\mathrm{MoralState}\times\mathrm{VirtueAction}\to\mathbb{R}$. The free energy is the Helmholtz potential built from that policy’s partition function, matching the classical identity $F=\langle E\rangle-TS$ once the KL gap to Gibbs is written out (doc-comment).
Upstream cost defs (ObserverForcing, MultiplicativeRecognizer, RungCoarsen, PRC bridge) all specialize the same J-cost that feeds $J$ here; the thermodynamic siblings define free energy as $-T\log Z$ on abstract systems.
proof idea
Definition, not a proof. The body is the single term $-g.\mathrm{temp_R}\cdot\log(g.\mathrm{partitionFn},s,\mathrm{actions})$, i.e. the standard Helmholtz formula with recognition temperature and the policy’s own partition function. No lemmas are applied.
why it matters
Anchors thermodynamic learning in the RS→RL stack: free energy is the scalar the Gibbs policy minimizes, and the KL identity in the doc-comment ($F_R(q)-F_R(\mathrm{Gibbs})=T_R,D_{\mathrm{KL}}(q|\mathrm{Gibbs})$) is the variational principle behind soft actor-critic style updates grounded in J rather than an ad-hoc reward.
Downstream, Thermodynamics.BoltzmannDistribution.freeEnergy and PartitionFunction.freeEnergy reuse the same $-T\log Z$ shape, and free_energy_identity proves $F=\langle E\rangle-TS$ from that definition. In the forcing chain this sits under T5–T6 thermodynamics (J-cost uniqueness and eight-tick cadence), not under mass or α claims.
It does not close any open scaffold; it is the shared interface between the RL bridge and the formal thermo layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.