cert
plain-language theorem explainer
Packages the four structural facts of the oxidation-state certificate: the canonical d-block count equals 7, is positive, and the J-cost on the measured/expected ratio vanishes on the diagonal and is nonnegative off it. Chemists citing the RS Count-Law prediction for transition-metal oxidation multiplicity use this bundle. It is a pure structure instance wiring four already-proved lemmas.
Claim. There is a certificate asserting: the canonical oxidation-state count equals $7$; that count is strictly positive; for every nonzero real $s$, the oxidation-state cost of the ratio $s/s$ is zero; and for all positive reals $m,e$, the oxidation-state cost of $m/e$ is nonnegative.
background
The module treats transition-metal oxidation multiplicity as a ConfigDim count. Recognition Science predicts the canonical number of common oxidation states for d-block metals is $2^3-1=7$ (Count Law at spatial dimension $D=3$): three binary axes for charge sign, d-electron count relative to half-fill, and ligand-field position. Empirically this matches the IUPAC "golden-7" common states (e.g. Mn common set of size 7).
The cost on an oxidation-state ratio is the standard J-cost $J(x)=(x+x^{-1})/2-1$ evaluated at measured/expected. Upstream, canonicalOxidationStateCount_eq is a one-line unfold-and-norm proof that the count definition equals 7; positivity follows by rewrite. Diagonal vanishing uses $J(1)=0$; nonnegativity is Cost.Jcost_nonneg on a positive ratio (same nonnegativity used for recognition-event costs in ObserverForcing).
proof idea
Definitional structure instance, not a tactic proof. Each field of OxidationStateCert is filled by the corresponding lemma: equality by canonicalOxidationStateCount_eq, positivity by canonicalOxidationStateCount_pos, diagonal zero by oxidationStateCost_at_expected (unfold, div_self, Cost.Jcost_unit0), and nonnegativity by oxidationStateCost_nonneg (unfold, Cost.Jcost_nonneg on div_pos). No extra reasoning.
why it matters
Closes the structural certificate for the chemistry claim that d-block oxidation multiplicity is forced by the eight-tick / $D=3$ Count Law ($2^3-1=7$), tying T7 (eight-tick octave) and T8 ($D=3$) into inorganic chemistry. The cost fields embed the same J-uniqueness (T5) used throughout RS: deviation from the expected oxidation state is a nonnegative J-cost minimized only on the expected ratio. No downstream consumers are wired yet (used_by empty); the sibling inhabitedness fact is the natural next hook. The module falsifier remains empirical: a d-block element whose stable common oxidation-state count lies outside $7\pm 2$ under standard conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.