dft_exchange_one_statement
plain-language theorem explainer
The exchange-correlation contribution to DFT energy equals the J-cost function of the spin-density ratio x. It vanishes at the closed-shell point x=1, is strictly positive for other positive x, is invariant under x to 1/x, and evaluates to a value in (0.11,0.13) at the golden ratio. Density-functional theorists seeking a first-principles derivation of the exchange functional would cite this result. The proof assembles four prior J-cost lemmas into a single conjunction.
Claim. Let $f(x)$ denote the exchange-correlation contribution for spin-density ratio $x>0$. Then $f(1)=0$, $f(x)>0$ whenever $x>0$ and $x≠1$, $f(x)=f(x^{-1})$ for all $x>0$, and $0.11<f(φ)<0.13$ where $φ$ is the golden ratio.
background
In this module the exchange-correlation functional of density functional theory is obtained from the Recognition Science J-cost. The spin-density ratio $x=ρ_α/ρ_β$ measures deviation from closed shell; the contribution is defined by $f(x):=J(x)$ where $J$ satisfies the Recognition Composition Law. Upstream results establish that $J$ vanishes at unity (Jcost_unit0), is positive elsewhere (Jcost_pos_of_ne_one), and is symmetric under inversion (Jcost_symm). The golden ratio $φ$ enters as the self-similar fixed point from the forcing chain T5-T6.
proof idea
The proof is a term-mode conjunction that directly packages four sibling results: xc_closed_shell_zero (which applies Jcost_unit0), xc_min_at_closed_shell (which applies Jcost_pos_of_ne_one), xc_spin_interchange (which applies Jcost_symm), and xc_at_phi_band (which unfolds xcContribution to Jcost and invokes the numerical bounds on φ).
why it matters
This theorem consolidates the core properties of the DFT exchange functional forced by J-cost uniqueness. It realizes T5 J-uniqueness in the quantum-chemistry sector and predicts the alpha-band value inside (0.11,0.13). The module doc states that modern functionals sit near the closed-shell minimum at x=1; the result closes derivation track E1 and supplies the falsifier that any XC functional preferring a spin-polarised reference on H₂ would contradict the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.