reaction_equilibrium
plain-language theorem explainer
Chemical equilibrium for reactions requires the summed chemical potentials of products to equal those of reactants. Researchers deriving thermodynamics from J-cost minimization would cite this as the Recognition Science form of the law of mass action. The proof is a direct term-mode appeal to triviality once the equilibrium condition is identified with vanishing total J-cost gradient.
Claim. For a reaction such as $A + B ⇌ C + D$, equilibrium holds when the chemical potentials satisfy $μ_A + μ_B = μ_C + μ_D$. Recognition Science equates this condition to the vanishing of the total J-cost gradient with respect to particle number.
background
The J-cost function is defined as $J(x) = (x + x^{-1})/2 - 1$, serving as the canonical cost measure in log coordinates. Chemical potential is obtained as the partial derivative of the free energy (or J-cost) with respect to particle number at fixed temperature and volume. The module places this construction in the setting where particle flows minimize total J-cost, with ΔG identified with ΔJ-cost for any reaction.
proof idea
The proof is a term-mode application of the trivial tactic. It directly affirms the equilibrium equality once the J-cost minimization principle is imposed, without further reduction steps or lemma applications.
why it matters
This supplies the equilibrium condition inside the chemical-potential derivation from J-cost gradients. It connects to the broader Recognition framework through the J-uniqueness property and the composition law that governs cost additivity. No downstream theorems are recorded yet, leaving open its use in explicit reaction-rate or kinetics derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.