pith. sign in
module module high

IndisputableMonolith.QuantumChemistry.DFTExchangeFromJCost

show as:
view Lean formalization →

DFTExchangeFromJCost module translates the J-cost function into density-functional exchange terms for spin-polarized systems. It defines the spin-density ratio x = ρ_α/ρ_β together with closed-shell zeros, phi-band corrections, and quadratic approximations. The module is a collection of definitions and short lemmas that rest on the Cost and Constants primitives.

claimThe module introduces the spin-density ratio $x = ρ_α / ρ_β$ for $x ∈ (0, ∞)$ and constructs exchange-correlation contributions xcContribution(x), closed-shell zero points, and quadratic forms near closed shells, all obtained from the J-cost.

background

Recognition Science quantifies deviations from self-similarity via the J-cost J(x) = (x + x^{-1})/2 - 1 supplied by the Cost module. Constants supplies the base time quantum τ₀ = 1 tick. The present module maps these objects onto quantum chemistry by expressing spin densities through the dimensionless ratio x and deriving exchange terms that remain consistent with the phi-ladder and eight-tick octave.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the DFT exchange machinery that feeds into DFTExchangeCert and related quantum-chemistry certificates. It closes the link from the J-cost formalism to practical exchange-correlation functionals, placing the Recognition Science primitives inside standard density-functional calculations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)