ElectrochemicalProcess
plain-language theorem explainer
The inductive definition enumerates the five canonical electrochemical processes in the Recognition Science model. A physicist deriving charge-transfer equilibria or Nernst potentials from the J-functional equation would cite this enumeration to fix configDim D at 5. The definition is a direct inductive type whose Fintype and DecidableEq instances are obtained automatically by derivation.
Claim. Let $P$ be the finite set of electrochemical processes consisting of oxidation, reduction, electrolysis, galvanic cell, and corrosion, equipped with decidable equality.
background
Recognition Science obtains electrochemistry from the J-cost function, where J equals zero at equilibrium (Nernst potential with zero driving force) and J greater than zero measures the recognition cost of a charge-transfer barrier. The module states that five canonical processes realize configDim D equals 5. The J-cost is imported from the Cost module and appears in the downstream ElectrochemistryCert as the equilibrium condition Jcost 1 equals 0.
proof idea
Direct inductive definition of the five constructors with automatic derivation of DecidableEq, Repr, BEq, and Fintype. No tactic steps or lemmas are applied; the instances follow from the inductive structure.
why it matters
The definition supplies the finite set required by electrochemicalProcessCount (which proves cardinality 5) and by the ElectrochemistryCert structure (which pairs the cardinality with the equilibrium condition Jcost 1 equals 0). It fills the A1 Chemistry / E1 Applied slot that maps the five processes onto configDim D equals 5 in the Recognition Science derivation from the J-functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.