AcidBaseTheoriesCert
plain-language theorem explainer
The structure certifies that the inductive enumeration of acid-base theories has cardinality five, matching configDim D=5 in the Recognition Science model. Chemists grounding acid-base behavior in the forcing chain would cite this when linking the five canonical theories to the phi-ladder and eight-tick octave. Its definition is a direct packaging of the Fintype.card result from the inductive type.
Claim. Let $T$ be the set of acid-base theories consisting of Arrhenius (proton donor in water), Brønsted-Lowry (proton donor), Lewis (electron-pair acceptor), Usanovich (electron/cation/anion exchange), and Pearson HSAB (hard/soft classification). Then $|T| = 5$.
background
The module derives acid-base theories from configDim D=5 within the Recognition Science framework, where the five theories are Arrhenius, Brønsted-Lowry, Lewis, Usanovich, and Pearson HSAB. The inductive type AcidBaseTheory enumerates these five cases and derives DecidableEq, Repr, BEq, and Fintype instances. The structure AcidBaseTheoriesCert packages the single assertion that the cardinality of this type equals five.
proof idea
This is a structure definition with one field. The field is satisfied by the precomputed Fintype.card value on the inductive type, supplied downstream via the acidBaseTheory_count definition.
why it matters
The definition supplies the certification instance used by acidBaseTheoriesCert, anchoring the five theories to configDim D=5. It sits inside the chemistry foundations that extend the forcing chain (T0-T8) and Recognition Composition Law into molecular behavior, consistent with the eight-tick octave and phi-ladder constants. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.