electrochemicalPotential
plain-language theorem explainer
Electrochemical potential is the sum of chemical potential and the product of charge with electric potential. Battery and electrochemistry modelers cite it to track particle flow driven by total J-cost minimization. The definition is a direct algebraic extension of the J-cost gradient for chemical potential.
Claim. The electrochemical potential is defined by $tilde{mu} = mu + q phi$, where $mu$ is the chemical potential obtained as the J-cost gradient with respect to particle number, $q$ is the charge, and $phi$ is the electric potential.
background
The module THERMO-007 derives chemical potential from J-cost gradients in Recognition Science. Chemical potential measures the energy cost of adding one particle and drives flow from high to low values, appearing in Fermi-Dirac and Bose-Einstein statistics. In the RS setting it equals the partial derivative of free energy or Gibbs free energy with respect to particle number, realized as a J-cost gradient that particles minimize on the recognition ledger.
proof idea
Direct definition that adds the electrostatic term to the base chemical potential, matching the battery voltage relation given in the module comment.
why it matters
This definition extends the J-cost gradient mechanism for chemical potential to include electrostatic contributions, allowing batteries to be treated as J-cost gradient devices. It sits inside the thermodynamics module that connects Recognition Science forcing chains to observable electrochemical behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.