acidBaseTheoriesCert
plain-language theorem explainer
acidBaseTheoriesCert constructs a certificate asserting exactly five acid-base theories in the Recognition Science model, matching the five-dimensional configuration space. Chemists or framework users cite it to confirm the enumeration of Arrhenius, Brønsted-Lowry, Lewis, Usanovich, and Pearson HSAB theories. The definition is a one-line wrapper that directly assigns the result of the upstream cardinality theorem.
Claim. The certificate is the structure asserting that the finite set of acid-base theories has cardinality five, i.e., the number of such theories equals 5.
background
The module treats chemistry foundations by setting the configuration dimension to five, which directly accommodates the five canonical acid-base 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 referenced structure requires that the cardinality of the type of acid-base theories equals five. This rests on the upstream theorem that computes the cardinality by exhaustive enumeration and decides it outright.
proof idea
The definition is a one-line wrapper that populates the cardinality field of the certificate structure with the result of the upstream enumeration theorem.
why it matters
This definition completes the certification step in the chemistry module, aligning the five theories with the framework's configDim parameter and the overall forcing chain that derives physical structures from a single functional equation. It supplies the foundational count for any subsequent chemistry derivations, though the module lists no immediate dependents. The module documentation states zero sorry or axiom, confirming the enumeration is fully decided within the Recognition Science setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.