enzymeClass_count
plain-language theorem explainer
The theorem asserts that the finite type of enzyme classes has cardinality five, matching the five canonical EC classes one through five. Researchers constructing catalysis thresholds in the Recognition framework cite this cardinality when building the enzyme catalysis certificate. The proof is a one-line decision procedure that enumerates the five inductive constructors.
Claim. The finite type of enzyme classes has cardinality five: $|$EnzymeClass$| = 5$.
background
The module develops enzyme catalysis thresholds from the J-cost functional in Recognition Science. EnzymeClass is the inductive type whose five constructors are oxidoreductase, transferase, hydrolase, lyase, and isomerase; these derive Fintype, DecidableEq, and related instances. The local setting fixes configDim D = 5 for the chemistry layer, corresponding to EC classes 1-5 with ligases and translocases treated as extensions.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds directly from the Fintype derivation on the inductive type, which computes the cardinality as five without further lemmas.
why it matters
This result supplies the five_classes field to the downstream enzymeCatalysisCert definition, anchoring the B10 industrial chemistry depth. It realizes configDim D = 5 for enzyme mechanisms and sits inside the phi-ladder structure of the Recognition framework. The module reports zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.