fe_kl_id
plain-language theorem explainer
The lemma equates the recognition free energy of an arbitrary distribution q to that of the Gibbs equilibrium plus the recognition temperature times the KL divergence from q to equilibrium. Researchers deriving the second law from J-descent operators would cite this identity to convert information contraction into free-energy descent. The proof is a one-line wrapper that rewrites the Gibbs distribution definition and invokes the general free-energy-KL identity.
Claim. Let $sys$ be a recognition system with positive temperature $T_R$, let $X:Ω→ℝ$ be a cost function, and let $q$ be a probability distribution on the finite set $Ω$. Then $F_R(q)-F_R(π)=T_R⋅D_{KL}(q‖π)$, where $π$ is the Gibbs equilibrium distribution induced by $X$, $F_R$ denotes recognition free energy, and $D_{KL}$ is Kullback-Leibler divergence.
background
A RecognitionSystem consists of a positive real temperature $T_R$ that scales noise in the recognition process. Recognition free energy is defined as expected cost minus $T_R$ times recognition entropy. KL divergence is the sum $∑q_ω log(q_ω/p_ω)$ (zero when $q=p$). The upstream free_energy_kl_identity states: F_R(q)−F_R(Gibbs)=TR⋅D_KL(q‖Gibbs). The module constructs the Gibbs distribution via gibbsPD and uses JDescentOperator structures whose step fixes equilibrium while contracting KL divergence to it.
proof idea
One-line wrapper that rewrites the second free-energy argument via the auxiliary gibbsPD_p lemma and then applies the free_energy_kl_identity theorem directly from the MaxEntFromCost module.
why it matters
This identity is invoked inside the proof of free_energy_step_le to obtain single-step free-energy contraction under any JDescentOperator. Combined with kl_divergence_antitone it yields the full second-law statement that free energy is monotone non-increasing along recognition trajectories, grounding thermodynamic irreversibility in the J-cost and the eight-tick octave structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.