free_energy_le_of_le
plain-language theorem explainer
The theorem shows that recognition free energy is monotone non-increasing along any trajectory generated by a J-descent operator. A researcher deriving the second law from first principles in Recognition Science would cite this result to establish the Lyapunov property of free energy. The proof is a direct induction on the time interval that applies the one-step contraction at each successor step.
Claim. Let $sys$ be a recognition system, $X:Ω→ℝ$ a cost function, $R$ a J-descent operator fixing the Gibbs distribution $gibbsPD(sys,X)$, and $q_0$ an initial probability distribution. Then for natural numbers $n≤m$, the recognition free energy satisfies $F_R((R^m q_0).p,X)≤F_R((R^n q_0).p,X)$.
background
A JDescentOperator on distributions over finite $Ω$ is a map that fixes the equilibrium distribution and is non-expansive in KL divergence to that equilibrium. The module defines the discrete trajectory $q_n=R^n q_0$ and the recognition free energy $F_R(q,X)$ as the expected cost minus temperature times recognition entropy. The local setting is the derivation of the second law inside Recognition Science with no new axioms: free energy is shown to be a Lyapunov function whose minimum is attained at the Gibbs measure.
proof idea
The proof is an induction on the hypothesis $n≤m$. The base case applies the reflexivity lemma for the order. The inductive step applies transitivity of the order to the one-step inequality free_energy_step_le together with the inductive hypothesis.
why it matters
This lemma is the key inductive step that yields the antitone theorem free_energy_antitone and the bundled second-law statements second_law_one_statement and second_law_entropy_form. It supplies the monotonicity half of the Lyapunov formulation of the second law, with the Gibbs state as unique global minimum, directly from the J-descent axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.