xc_closed_shell_zero
plain-language theorem explainer
The theorem shows that the exchange-correlation contribution to the DFT energy vanishes exactly when the spin-density ratio equals one. Quantum chemists deriving functionals from first principles would cite it to fix the zero point of the XC term at the closed-shell reference. The proof is a one-line wrapper that unfolds xcContribution and invokes the unit-zero lemma for the underlying J-cost function.
Claim. Let $x = ρ_α / ρ_β$ be the spin-density ratio. The exchange-correlation contribution satisfies $xc(1) = 0$.
background
The DFTExchangeFromJCost module derives the exchange-correlation functional from the J-cost of Recognition Science. The variable x parametrizes the spin-density ratio of a closed-shell system; the contribution is required to vanish at x=1, to be symmetric under x ↔ 1/x, and to be bounded below. These conditions match the calibrations of the J-cost function J(x) = (x-1)²/(2x). The upstream lemma Jcost_unit0 states that Jcost 1 = 0 by direct simplification of the squared-ratio expression.
proof idea
The proof is a one-line wrapper: it unfolds the definition of xcContribution and applies the lemma Jcost_unit0, which states Jcost 1 = 0.
why it matters
This theorem supplies the closed_shell_zero field of the DFTExchangeCert structure. That structure populates the one-statement theorem dft_exchange_one_statement, which collects the full set of XC properties: zero at closed shell, strict positivity elsewhere, spin-interchange symmetry, and the golden-section band value J(φ) ∈ (0.11, 0.13). It realizes the J-uniqueness step (T5) of the forcing chain inside quantum chemistry, confirming that the Recognition Composition Law forces the XC minimum to the closed-shell point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.