canonicalOxidationStateCount_pos
plain-language theorem explainer
The canonical oxidation-state count for d-block metals is strictly positive. Anyone packaging the ConfigDim Count-Law certificate needs this positivity side-condition. The proof rewrites the count to 7 via the equality lemma and finishes by numeric normalization.
Claim. The canonical oxidation-state count equals $2^3-1$ and satisfies $0 < 2^3-1$ (equivalently $0 < 7$).
background
This module fixes a structural RS prediction for transition-metal chemistry: the canonical number of oxidation states for d-block elements is the Count Law at spatial dimension $D=3$, namely $2^3-1=7$. The three binary axes are charge sign, d-electron count relative to half-fill, and ligand-field placement. That matches the common seven-state ranges (Mn, Cr, Fe) and the IUPAC "golden-7" pattern.
The count itself is the natural-number definition $2^3-1$. A sibling equality theorem reduces it to the concrete numeral 7. Downstream cost lemmas treat deviation of an observed oxidation ratio from the expected state via the usual J-cost, but this declaration only concerns positivity of the count.
The forcing chain already supplies $D=3$ (T8) and the eight-tick octave (T7); here those enter only as the exponent and the Count-Law shape $2^D-1$.
proof idea
One-line tactic proof. Rewrite the goal with the sibling equality canonicalOxidationStateCount = 7, then norm_num discharges $0 < 7$. No chemistry or cost reasoning is used.
why it matters
Feeds the bundled certificate cert : OxidationStateCert, which records count equality, count positivity, vanishing of oxidation-state cost at the expected ratio, and non-negativity of that cost. Without positivity the certificate type would be uninhabited as a well-formed count.
In the framework this is the trivial but required side-condition on the Count Law at $D=3$ (T8), the same $2^3-1$ pattern that appears with the eight-tick octave (T7). It closes no open physics gap by itself; it makes the structural chemistry certificate fully proved (0 sorry, 0 axiom) so downstream consumers can assume a positive canonical multiplicity of seven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.