cert
plain-language theorem explainer
Bundles three structural facts about the ligand-field domain cost into one certificate: diagonal vanishing, non-negativity for positive metal/ligand parameters, and a strictly positive canonical threshold. Cited by anyone auditing the RS claim that octahedral 10Dq/B sits near φ^5. Proof is a structure instance wiring three already-proved sibling lemmas.
Claim. There exists a ligand-field certificate asserting: (i) the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module treats crystal-field (ligand-field) splitting of $d$-orbitals in octahedral complexes as a recognition-cost problem on the $\varphi$-ladder. Empirically, weak-field $O_h$ complexes have $10Dq/B\approx 20$–$30$; RS predicts the mid-range value $10Dq/B=\varphi^5\approx 11.09$, so with $B\approx 800,\mathrm{cm}^{-1}$ one gets $10Dq\approx 8800,\mathrm{cm}^{-1}$.
The domain cost $C(m,e)$ is the local J-cost comparison between a metal parameter $m$ and a ligand (or field) parameter $e$. Sibling lemmas already show $C(r,r)=0$ off zero, $C\ge 0$ on the positive quadrant, and that the canonical threshold (the scale at which splitting is declared resolved) is positive. The upstream fact cost_nonneg from ObserverForcing states that every recognition event has non-negative J-cost, which underwrites the domain-cost non-negativity lemma used here.
proof idea
One-line structure instance. The three fields of LigandFieldCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra is performed at this site.
why it matters
Gives a single named inhabitant of the ligand-field certificate so downstream chemistry results can assume the three structural axioms without re-proving them. Anchors the module's claim that octahedral $10Dq/B$ is forced near $\varphi^5$ (the same $\varphi^5$ that appears as $Z_{\mathrm{cf}}$ and in the RS-native $G=\varphi^5/\pi$). No downstream consumers are wired yet (used_by is empty); the certificate is the closed structural theorem advertised in the module header (0 sorry, 0 axiom). It does not itself derive the spectroscopic band, only the cost-theoretic scaffolding on which that comparison sits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.