ElectrochemistryCert
plain-language theorem explainer
ElectrochemistryCert packages the assertion that exactly five electrochemical processes exist and that equilibrium occurs at zero J-cost. Modelers of charge transfer barriers would cite this when connecting recognition cost to Nernst potentials or overpotentials. The structure is realized directly by two fields, one drawn from Fintype cardinality on the process inductive type and one from the upstream equilibrium result.
Claim. A structure certifying that the set of electrochemical processes has cardinality 5 and that the J-cost function satisfies $J(1)=0$.
background
ElectrochemicalProcess is the inductive type with constructors oxidation, reduction, electrolysis, galvanicCell, corrosion. Jcost measures recognition cost of a configuration; the upstream equilibrium theorem states that Jcost 1 equals zero. The module sets the process count equal to configDim D equals 5 and identifies electrochemical equilibrium with vanishing driving force.
proof idea
One-line structure definition whose five_processes field is the Fintype.card of ElectrochemicalProcess and whose equilibrium field is the upstream equilibrium theorem.
why it matters
The certificate fixes the process count at five and equilibrium at J equals zero, supplying the concrete data used by the downstream electrochemistryCert definition. It realizes the module claim that five processes equal configDim D equals 5 and ties the J-cost equilibrium condition to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.