acidBaseTheory_count
plain-language theorem explainer
The theorem asserts that the finite type of acid-base theories has cardinality exactly five. Chemists or foundational physicists working in the Recognition Science chemistry module would cite it to confirm the enumeration tied to configuration dimension. The proof is a direct decision procedure that exhausts the five constructors of the inductive type.
Claim. The set of acid-base theories has cardinality five: $ |{Arrhenius, Brønsted-Lowry, Lewis, Usanovich, Pearson HSAB}| = 5 $.
background
The module Chemistry.AcidBaseTheoriesFromConfigDim defines acid-base theories via an inductive type whose five constructors are arrhenius, bronstedLowry, lewis, usanovich, and pearsonHSAB; these derive the Fintype instance used for cardinality. The module documentation states that this enumeration equals configDim D = 5 and lists the five canonical theories: Arrhenius (proton donor in water), Brønsted-Lowry (proton donor), Lewis (electron-pair acceptor), Usanovich (electron/cation/anion), and Pearson HSAB (hard/soft acids-bases). The sole upstream result is the inductive definition of AcidBaseTheory itself.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on the inductive type with five constructors.
why it matters
This theorem supplies the five_theories field inside the acidBaseTheoriesCert definition, which certifies the enumeration. It anchors the chemistry foundations depth of the Recognition Science framework by realizing configDim D = 5 as the source of the five canonical acid-base theories. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.