recognition_free_energy
plain-language theorem explainer
Recognition free energy is defined as expected J-cost minus recognition temperature times recognition entropy. Researchers proving monotonicity results and the H-theorem in Recognition Science cite this as the central variational quantity. The definition is a direct algebraic subtraction of the expected_cost and recognition_entropy functions.
Claim. $F_R = E_p[J(X)] - T_R S_R(p)$, where $T_R$ is the recognition temperature of the system, $E_p[J(X)]$ is the expected J-cost under distribution $p$, and $S_R(p)$ is the recognition entropy of $p$.
background
The module defines the statistical mechanics of Recognition Science by extending zero-temperature J-cost minimization to finite recognition temperature TR. RecognitionSystem is the structure holding TR > 0, with beta defined as its inverse. Expected cost is the sum over states of p(ω) times Jcost(X(ω)). Recognition entropy is the negative sum of p(ω) log p(ω), with the convention that 0 log 0 equals 0.
proof idea
One-line definition that subtracts the product of sys.TR and recognition_entropy p from expected_cost p X.
why it matters
This supplies the free energy whose decrease is established in coarse_graining_decreases_free_energy, h_theorem_recognition, and rs_arrow_of_time. It realizes the variational principle at finite TR, connecting J-cost to the Gibbs measure via the entropy-maximizer theorem. The definition closes the bridge from the Recognition Composition Law to thermodynamic identities such as the free-energy gap equaling TR times KL divergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.