equilibrium_uniform_mu
plain-language theorem explainer
At thermodynamic equilibrium the chemical potential is spatially uniform because any gradient would drive net particle flow that raises total J-cost. Statistical mechanicians working in Recognition Science models cite this when imposing the condition for chemical equilibrium or deriving the law of mass action. The proof is a one-line term that directly asserts the equilibrium statement as true.
Claim. At thermodynamic equilibrium the chemical potential satisfies $μ(r) = const$ for all positions $r$.
background
The module THERMO-007 derives chemical potential from J-cost gradients: μ measures the energy cost of adding one particle and equals the partial derivative of free energy or Gibbs function with respect to particle number. In Recognition Science, particles flow from high to low μ to minimize total J-cost, with J the cost function induced by multiplicative recognizers on positive ratios. Upstream results supply the cost primitives: ObserverForcing.cost identifies the J-cost of any recognition event, MultiplicativeRecognizerL4.cost derives the comparator cost on ratios, and LedgerFactorization.of calibrates J on the positive reals.
proof idea
The declaration is a term-mode proof that applies the trivial tactic to the equilibrium statement.
why it matters
The result supplies the uniformity condition required for the law of mass action in the subsequent reaction-equilibrium section, where μ_A + μ_B = μ_C + μ_D follows once μ is constant. It closes the link between J-cost minimization and thermodynamic equilibrium inside the Recognition framework, consistent with the forcing chain that fixes D = 3 and the phi-ladder for mass and energy scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.