HalfCellCategory
plain-language theorem explainer
The declaration enumerates five half-cell categories for the electrochemical series derived from the phi-ladder. Chemists mapping standard reduction potentials across five orders of magnitude cite this enumeration to fix configDim D = 5. It is introduced directly as an inductive type with five named constructors and derives the standard decidability and finiteness instances.
Claim. The half-cell categories are the finite inductive set with five elements: strong oxidizing, weak oxidizing, SHE reference, weak reducing, and strong reducing.
background
The module derives the electrochemical series from the phi-ladder in Recognition Science. Half-cell categories are partitioned into five canonical types that match configDim D = 5: strong oxidizing, weak oxidizing, neutral SHE reference, weak reducing, and strong reducing. Standard reduction potentials are required to span five orders of magnitude under canonical RS rescaling by phi.
proof idea
The declaration is an inductive definition that introduces exactly five constructors and automatically derives DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This supplies the five categories required by the downstream ElectrochemicalSeriesCert structure, which asserts Fintype.card = 5, consecutive reduction potentials in exact phi ratio, and strictly positive potentials. It anchors the chemistry depth of the Recognition Science framework by discretizing the phi-ladder for electrochemistry, consistent with the five-order span under RS rescaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.