gibbs_reaction
plain-language theorem explainer
The gibbs_reaction definition encodes the rule that the sign of the Gibbs free energy change decides whether a reaction advances or reverses. Researchers deriving thermodynamic equilibria from J-cost minimization in Recognition Science cite this label when discussing reaction spontaneity. It is implemented as a direct string constant without invoking any lemmas or computations.
Claim. The change in Gibbs free energy for a reaction is given by $ΔG = ∑_i ν_i μ_i - ∑_j ν_j μ_j$, where $μ$ is the chemical potential. The sign of $ΔG$ determines reaction direction: negative for forward progress, positive for the reverse, and zero at equilibrium. In Recognition Science this $ΔG$ equals the net change in J-cost for the stoichiometry.
background
The module THERMO-007 derives chemical potential from J-cost gradients. Chemical potential $μ$ measures the energy cost of adding one particle and equals the partial derivative $(∂F/∂N){T,V}$ or $(∂G/∂N){T,P}$. In Recognition Science this gradient is the marginal J-cost, so particles flow to minimize total J-cost and $μ$ sets ledger occupation states.
proof idea
The declaration is a one-line definition that directly assigns the string 'ΔG determines reaction direction'. No lemmas from the depends_on list are applied; the body serves only as a conceptual label for the sign rule.
why it matters
This definition supplies the reaction-direction rule that links standard thermodynamics to the J-cost framework inside the ChemicalPotential module. It reinforces the emergence of potentials from the Recognition Composition Law and the forcing chain steps T5 (J-uniqueness) and T6 (phi fixed point). It leaves open the explicit derivation of equilibrium constants from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.