spinRatio
plain-language theorem explainer
spinRatio defines the dimensionless spin-density ratio x = ρ_α / ρ_β as the identity map on the reals. DFT modelers deriving exchange-correlation functionals from J-cost uniqueness cite it to parameterize spin polarization in the closed-shell sector. The definition is a direct one-line abbreviation to the identity function.
Claim. Let $x = ρ_α / ρ_β$ denote the dimensionless spin-density ratio. The spin-density ratio map is the identity function $x ↦ x$.
background
The module derives the exchange-correlation functional in density functional theory from the J-cost stationary point of the density-ratio variable. The spin-density ratio x tracks deviation from closed-shell symmetry at x=1, with the exchange energy required to be symmetric under x ↦ x^{-1}, normalized to zero at x=1, and bounded below. These conditions match the calibrations of J-cost. Upstream, CostAlgebra.id supplies the identity automorphism, while PhiForcingDerived.of structures the J-cost and ArithmeticOf.canonical supplies the initial Peano object for the arithmetic setting.
proof idea
The declaration is a one-line definition that equates spinRatio to the identity function on the reals.
why it matters
This definition supplies the input variable for the XC contribution in the DFT exchange derivation from J-cost. It supports the prediction that the minimum occurs at x=1, consistent with T5 J-uniqueness in the forcing chain. Downstream siblings such as xcContribution and dftExchangeCert build directly on this parameterization to recover the quadratic correction near closed shell and the band-gap value at x=φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.