OxidationStateCert
plain-language theorem explainer
Certificate packing the Count Law claim that d-block metals have seven canonical oxidation states ($2^3-1$ at $D=3$), together with zero-at-match and nonnegativity of the J-cost on oxidation ratios. Inorganic chemists and RS auditors cite it when installing oxidation multiplicity into Phase 8B. It is a pure Prop-bundle structure; inhabited downstream by the sibling certificate constructor.
Claim. A certificate consisting of four claims: the canonical oxidation-state count equals $7$; that count is strictly positive; for every nonzero real $s$, the oxidation-state cost of measuring $s$ against expected $s$ is zero; and for all positive reals $m,e$, the oxidation-state cost of $m$ against $e$ is nonnegative.
background
The module treats oxidation-state multiplicity of d-block metals as a ConfigDim count. Recognition Science forces $D=3$ spatial dimensions (forcing chain T8) and an eight-tick octave of period $2^3$ (T7). The Count Law at $D=3$ therefore predicts $2^3-1=7$ canonical oxidation states, read as three binary axes: charge sign, d-electron count relative to half-fill, and ligand-field side.
The canonical count is the bare natural $2^3-1$. The oxidation-state cost is the standard J-cost $J(m/e)$ on the ratio of measured to expected state; $J$ is the unique nonnegative cost fixed by the Recognition Composition Law, minimized at ratio $1$. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-nonnegativity.
The local setting is a structural theorem module (zero sorry, zero axiom) whose falsifier is any d-block element whose confirmed stable oxidation-state count under standard inorganic conditions lies outside $7\pm 2$.
proof idea
No proof body: this is a structure declaration whose four fields are pure propositions. Field one asserts equality of the canonical count to $7$. Field two asserts positivity of that count. Field three is the diagonal vanishing law for the oxidation-state cost. Field four is nonnegativity of the cost on the positive quadrant. Inhabitation is deferred to the sibling constructor that fills each field from the corresponding lemma (canonicalOxidationStateCount_eq, _pos, oxidationStateCost_at_expected, _nonneg).
why it matters
This structure is the typed interface for the oxidation Count Law. Downstream, the concrete certificate and its Nonempty theorem inhabit it; OxidationStatesDerived re-exports availability and builds the Phase 8B certificate that pins iron's accessible states to $[0,2,3,6]$, manganese reaching $+7$, and manganese's accessible list having length exactly $7$.
Framework landmarks: T7 (eight-tick / $2^3$) and T8 ($D=3$) jointly force the $2^3-1=7$ count; the cost fields reuse the unique J-cost from T5 / RCL. The module doc ties the prediction to the IUPAC "golden-7" common transition-metal oxidation states and to manganese's common set of seven. Open empirical edge: the $\pm 2$ tolerance in the falsifier leaves room for rare high states (e.g. Fe(VIII)) without breaking the certificate interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.