xcContribution
plain-language theorem explainer
The definition of the exchange-correlation contribution sets it equal to the J-cost evaluated at the spin-density ratio. A researcher deriving first-principles DFT functionals would cite this to ground the XC term in the Recognition Science cost function on the canonical sector. It is realized as a direct alias to the J-cost function, which carries the uniqueness properties established in the Cost module.
Claim. Let $x = ρ_α / ρ_β$ be the spin-density ratio. The exchange-correlation contribution is defined by $E_{xc}(x) = J(x)$, where $J$ is the J-cost function calibrated to vanish at the closed-shell reference $x = 1$.
background
In the DFT Exchange Functional module the spin-density ratio $x = ρ_α / ρ_β$ parametrizes deviations from closed-shell systems. The model requires the exchange-correlation contribution to be symmetric under spin interchange $x ↦ x^{-1}$, to normalize to zero at $x = 1$, and to remain positive elsewhere. These three conditions coincide exactly with the calibrations of the J-cost function from the Cost module, so uniqueness on the positive reals fixes the functional form up to scaling.
proof idea
The declaration is a one-line definition that equates the exchange-correlation contribution directly to the J-cost function. It imports Jcost from the Cost module and inherits its algebraic properties (vanishing at unity, positivity off unity, and quadratic leading term) without further reduction steps.
why it matters
This definition supplies the core term for the DFTExchangeCert structure and the master one-statement theorem that certifies zero at closed-shell, strict positivity elsewhere, spin symmetry, and the value at the golden-section ratio lying in (0.11, 0.13). It realizes the module claim that Recognition Science forces the XC minimum at the closed-shell point via J-uniqueness and connects to the forcing-chain landmarks T5 and the phi-ladder predictions for the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.