electrochemical_equilibrium
plain-language theorem explainer
The theorem establishes that the recognition cost vanishes at unit scale, which encodes electrochemical equilibrium at zero driving force in the RS model. Physicists modeling charge-transfer barriers or Nernst potentials in RS-native units would cite this as the equilibrium baseline. The proof reduces immediately to the unit lemma for the J-cost function via simplification.
Claim. The recognition cost satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$.
background
In the ElectrochemistryFromRS module, five canonical processes (oxidation, reduction, electrolysis, galvanic cell, corrosion) are identified with configDim D = 5. Electrochemical equilibrium corresponds to vanishing recognition cost J = 0, while overpotential arises when J > 0. The J-cost is defined in the Cost module as J(x) = (x-1)^2 / (2x), which measures the recognition cost of a scale factor x. This theorem relies on the upstream lemma Jcost_unit0, which states Jcost 1 = 0 by direct simplification.
proof idea
The proof is a one-line wrapper that invokes the lemma Jcost_unit0 from the Cost module. That lemma itself proceeds by simp [Jcost] on the definition J(x) = (x-1)^2/(2x).
why it matters
This result supplies the equilibrium condition for the ElectrochemistryCert structure, which bundles the five processes and the equilibrium theorem. It anchors the RS treatment of electrochemistry at the point where driving force vanishes, consistent with the J-uniqueness and recognition composition law in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.