electrochemicalProcessCount
plain-language theorem explainer
The theorem states that the Recognition Science model recognizes exactly five electrochemical processes. Modelers of charge-transfer systems in RS units cite this enumeration when building process inventories. The proof is a direct decision on the Fintype cardinality of the inductive type listing oxidation, reduction, electrolysis, galvanic cell, and corrosion.
Claim. $ | {oxidation, reduction, electrolysis, galvanic cell, corrosion} | = 5 $
background
The ElectrochemistryFromRS module defines electrochemical processes via an inductive type with five cases: oxidation, reduction, electrolysis, galvanic cell, and corrosion. This cardinality matches the configuration dimension D = 5 in the RS framework. The module notes that electrochemical equilibrium corresponds to J = 0, the point of zero recognition cost for charge transfer.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance of the inductive type ElectrochemicalProcess.
why it matters
This theorem populates the five_processes field of the ElectrochemistryCert definition. It substantiates the module claim that five processes equal configDim D = 5, consistent with discrete counts arising from the self-similar fixed point in the forcing chain. It precedes the equilibrium certification step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.