AcidBaseTheory
The inductive definition enumerates the five canonical acid-base theories that Recognition Science associates with configDim equal to 5. Chemists using the RS model cite this enumeration when certifying that the theory count saturates the five-dimensional configuration space. The definition proceeds by explicit listing of the five constructors followed by automatic derivation of Fintype and related instances.
claimLet $T$ be the finite set of acid-base theories consisting of the Arrhenius theory, the Brønsted-Lowry theory, the Lewis theory, the Usanovich theory, and the Pearson HSAB theory.
background
The module grounds chemistry in the Recognition Science configuration dimension, which is fixed at D = 5. It enumerates the five standard acid-base theories that exhaust this dimension: 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 inductive type supplies the carrier for the subsequent cardinality statement that the number of theories equals 5.
proof idea
The declaration is a direct inductive definition that lists the five constructors explicitly. Derivation of DecidableEq, Repr, BEq, and Fintype is performed automatically by the Lean typeclass mechanism with no manual proof steps required.
why it matters in Recognition Science
This definition supplies the carrier type for AcidBaseTheoriesCert, which asserts Fintype.card AcidBaseTheory = 5, and for the companion theorem acidBaseTheory_count. It implements the module claim that exactly five theories correspond to configDim D = 5 in the RS chemistry foundations. The structure closes the enumeration step before any further certification or counting arguments are applied.
scope and limits
- Does not derive any ordering or hierarchy among the five theories.
- Does not supply a mapping from configDim to the listed theories.
- Does not encode chemical or physical properties of any theory.
- Does not establish equivalences or reductions between the theories.
formal statement (Lean)
17inductive AcidBaseTheory where
18 | arrhenius
19 | bronstedLowry
20 | lewis
21 | usanovich
22 | pearsonHSAB
23 deriving DecidableEq, Repr, BEq, Fintype
24