electrochemistryCert
plain-language theorem explainer
The definition assembles a certificate asserting exactly five canonical electrochemical processes together with equilibrium at zero J-cost. An applied chemist modeling charge transfer barriers would cite it to anchor Nernst potentials inside the Recognition Science J-function. The construction is a direct record instantiation that pairs the enumerated process count with the J-equals-zero theorem.
Claim. The electrochemistry certificate asserts that the number of canonical processes equals five and that the recognition cost vanishes at unit scale: $J(1)=0$.
background
In Recognition Science the J-cost function quantifies recognition effort for a process, with the upstream equilibrium result establishing Jcost 1 = 0 by direct reduction to Jcost_unit0. The module enumerates five canonical processes (oxidation, reduction, electrolysis, galvanic cell, corrosion) whose cardinality is fixed by a decide tactic. The local theoretical setting is A1 Chemistry / E1 Applied, where electrochemical equilibrium corresponds to zero driving force and overpotential appears as positive J-cost.
proof idea
The definition is a one-line record constructor that supplies the five-process count from the decide-based theorem and the equilibrium condition from the Jcost_unit0 reduction.
why it matters
This definition completes the certification block for electrochemistry inside the RS physics module, linking the five-process count and J-equals-zero equilibrium to the broader J-uniqueness property. It supplies the concrete instance required by the ElectrochemistryCert structure and sits downstream of the nonlinear-dynamics equilibrium theorem. No downstream uses are recorded, leaving open its later embedding into larger charge-transfer simulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.