gibbsPD_p
plain-language theorem explainer
The lemma states that the probability component of the Gibbs probability distribution built from a recognition system and cost function equals the standard Gibbs equilibrium measure. Researchers deriving the second law in Recognition Science cite it when equating free-energy expressions to KL divergences along J-descent trajectories. The proof is a direct reflexivity step from the definition of the Gibbs probability distribution.
Claim. Let $sys$ be a recognition system and $X:Ω→ℝ$ a cost function. The probability field of the Gibbs probability distribution for $sys$ and $X$ equals the Gibbs equilibrium measure $gibbs_measure(sys,X)$.
background
A RecognitionSystem fixes a positive recognition temperature $T_R$. The Gibbs measure is the equilibrium distribution over the finite configuration space $Ω$ that minimizes recognition free energy for a given cost assignment $X$. The Gibbs probability distribution is the structured object whose probability field $p$ stores this equilibrium. The module assembles the second law by showing that any J-descent operator (an abstract model of the recognition operator) produces monotone non-increasing KL divergence and free energy relative to this equilibrium. The data-processing inequality from the free-energy monotone module supplies the canonical witness for the non-expansiveness property.
proof idea
One-line term proof that applies reflexivity to the definition of the Gibbs probability distribution.
why it matters
This identity is invoked inside the KL-free-energy identity lemma and thereby inside the master second-law theorem. It supplies the concrete link between the abstract J-descent operator and the Gibbs equilibrium required by the Recognition Science derivation of the second law, which proceeds with zero new axioms. The result sits inside the chain that yields both the free-energy and entropy forms of the second law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.