coarse_graining_decreases_free_energy
plain-language theorem explainer
Coarse-graining a positive probability distribution over states cannot increase recognition free energy in a recognition system. Information-theoretic physicists would cite it as the Recognition Science version of the second law. The tactic proof packages the pushed-forward distribution, invokes the free-energy KL identity at both resolutions, applies the data-processing inequality to the KL term, and shows the free-energy difference is non-positive using non-negative temperature together with equality of the two Gibbs free energies.
Claim. Let $F_R$ denote recognition free energy. For a recognition system $sys$, observable $X:Ω→ℝ$, positive probability distribution $p$ on $Ω$, and coarse-graining map $φ:Ω→Ω'$, if the Gibbs measure of the effective cost pushes forward correctly under $φ$ and the recognition free energy of each Gibbs measure equals the free energy of its cost function, then $F_R(sys,p',J')≤F_R(sys,p,X)$ where $p'$ is the push-forward of $p$ and $J'$ is the effective cost of $X$ under $φ$.
background
The module proves that recognition free energy is non-increasing under RS dynamics such as coarse-graining. Recognition free energy $F_R(sys,q,Y)$ is the functional minimized by the Gibbs measure for cost function $Y$; it decomposes via the KL identity into expected cost plus temperature times KL divergence. Effective cost is the cost function obtained after applying the coarse-graining map $φ$. Push-forward transports distributions and measures forward under $φ$. The data-processing inequality for KL divergence and the fact that the Gibbs distribution minimizes free energy are the two equivalent characterizations of the monotonicity result.
proof idea
The tactic proof first builds the pushed-forward probability distribution $p'pd$ from the given positivity and sum-one hypotheses. It obtains the free-energy KL identities at both the fine and coarse levels. The data-processing inequality is applied directly to the original distribution and its Gibbs measure to produce a non-increase in KL divergence. A functional-extensionality step equates the pushed-forward Gibbs measure with the Gibbs measure of the effective cost. The free-energy difference is rewritten as temperature times the KL difference plus the difference of the two Gibbs free energies; the latter vanishes by the given alignment hypothesis, temperature is non-negative, and the KL term is non-positive, so linarith closes the inequality.
why it matters
This is the first main result listed in the Free Energy Monotonicity module and supplies the statistical-mechanics form of the second law inside Recognition Science. It directly supports the arrow-of-time definition (direction of time given by $dF_R/dt≤0$) and appears in the module status report. The result realizes the equivalence between free-energy monotonicity, the data-processing inequality, and Gibbs minimization; it closes one piece of the scaffolding for thermodynamic stability in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.