Formal reconstruction · Exact density variation, the local uniform-gas approximation, self-consistent orbitals, declared validity regimes and failures, a nonlocal exchange alternative, thermal and spin extensions, rapid-oscillation corrections, and a formally exact note-added-in-proof formulation
Self-Consistent Equations Including Exchange and Correlation Effects
From a constrained density minimum to actual complex orbitals and energy accounting, with approximation, representability, and self-consistency kept distinct
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureThe shared semantic boundary for the repeated variational route. Ground-state determination is intentionally absent: Hohenberg-Kohn proves it only in a paper-local nondegenerate scope, while Kohn-Sham reuses the variational input without independently realizing that determination argument.
- structure
- structureThe exact fixed-particle-number energy-minimum phenomenon explained by the ground-density variational route.
- structurePaper-local theory and world meanings for the exact shared model.
- structureProof-free data and proposition families selected by one exact ground-density variational route. No field supplies a proof of setup, variational calculation, attainment, minimization, applicability, or interpretation.
- structureA paper-local theory object paired with the selected exact model.
- inductiveExactly the claims retained by the shared variational route.
- structureThe selected state, external potential, density, and particle-number sector constrained by one complete ground-density variational route. Satisfaction additionally requires the exact selected setup and variational calculation.
- structureProof-free source constraint for one paper-local ground-density variational route. The typed token and its paper-local interpretation are retained without storing either a proof that the source route obtains or a variational output. This distinguishes an original derivation from a later paper's imported use of the same exact minimum.
- structureA represented physical system paired with the selected exact model.
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- structure
- structure
- structure
- structurePaper-local ground-state data with actual three-dimensional complex spin orbitals. Exact and approximate functionals have separate definitions, and all Coulomb and density readouts are computed from the selected functions.
- inductiveTyped token for Kohn and Sham's imported exact density-minimum input.
- structureThe physical ground-state system represented by one exact-density model.
- structure
- structure
- structure
- structureAppendix-II correction for short-wavelength density oscillations.
- structurePaper-local spin-paramagnetic extension from section IV.
- structureSection III keeps the exact Mermin density distinct from the selected local approximation.
- structureA fixed-volume temperature path. Number conservation is a separate condition.
- structure
- structureDensity variations at fixed T and chemical potential may change the mean number.
- structure
- structureA density of states is a derivative of a normalized energy-counting measure. Its smooth bulk or resolved-level interpretation remains an analytic input.
- structureThe state index is a spectral index, not the mean electron number.
- structure
- structure
- structure
- structure
Definitions and domain choices
- definition
- definition
- definitionThe complete selected route structurally explains why the exact ground density attains the physical energy and minimizes the functional on the declared fixed-particle-number domain.
- definition
- definition
- definition
- definitionA global paper-local helper from which selected calculations may be instantiated. It is not itself part of route applicability: the selected model consumes only the implication at its own state, potential, density, and particle number.
- definition
- definition
- definitionThe selected model is exactly the context-owned model. This equality retains all seven route-used maps, predicates, and energy functions in addition to the selected state, potential, derived density, and particle number.
- definitionThe exact pre-output setup used for theory/model/world grounding. It fixes the context-selected model together with its physical ground state, derived density, fixed particle-number sector, and selected-density admissibility. It assumes neither energy attainment nor minimization.
- definitionSource-sensitive explanation by one typed paper-local route.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe exact proof-free model induced by this context at selected indices.
- definition
- definition
- definitionThe unique proof-free model fixed by the context's selected ground state, external potential, and particle-number sector.
- definition
- definition
- definition
- definition
- definition
- definitionTheory use and physical representation require the selected exact model and its inhabited ground-density setup. They do not presuppose energy attainment, minimization, or any particular calculation route.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe finite canonical weights define a genuine probability mass function, not an independent law supplied by a physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected density is an admissible representative of a physical ground state.
- definition
- definition
- definitionThe complete inhabited ground-density route at one selected model. The proposition keeps the physical ground-state selection, density and particle-number consistency, membership of the selected density in the declared admissible domain, exact energy attainment, and minimization together. It cannot be satisfied merely because the implication-valued variational calculation has a false setup or an empty admissible domain.
- definitionThe selected state, density, and particle-number sector are mutually consistent under the exact maps stored in the model.
- definition
- definition
- definitionThe paper-local exact calculation, stated as an implication so that its premise and output remain visible. Applicability separately requires the selected setup and therefore cannot be obtained vacuously.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe typed energy-minimum phenomenon selected by this exact model.
- definitionThe typed variational constraint selected by this exact model.
- definitionExact proof-free source constraint selected by a model and source token.
- definition
- definitionCompare a candidate's energy functional with the selected reference model on the reference's declared density domain. This interpretation of completeness requires the same potential and number sector, candidate coverage of that domain, and pointwise equality of total energies. It does not itself certify either functional against the Hamiltonian or nature, constrain extra candidate densities, or extend the reference domain to arbitrary normalized densities.
- definitionThe density is a mathematical representative of a physical ground state at a fixed external potential and particle number. Admissibility, representation, and physical possibility remain separate relations.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
- definition
- definition
- definition
- definition
- definition
- definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
- definition
- definition
- definition
- definition
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA normalized continuum density and stable quadratic internal free energies test the printed signs. This is a thermodynamic diagnostic, not a microscopic material model.
- definition
- definition
- definition
- definitionPositive thermodynamic functions can have a small entropy remainder with a non-small derivative. This is not a proposed microscopic metal spectrum.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSelected representatives of equation (2.9); the spin sum is explicit.
- definitionThe vocabulary must represent the actual density variations to which the imported Hohenberg-Kohn minimum is applied.
- definition
- definitionThe note's formal potential is a derivative of the same exact functional, on the admitted fixed-number density variations. No evaluation algorithm is asserted.
- definition
- definition
- definitionNoninteracting representability and analytic/domain bridges remain explicit. Formal existence does not require an explicitly usable exchange-correlation formula.
- definition
- definition
- definition
- definition
- definition
- definitionEquation (2.2), before the local approximation is made.
- definition
- definition
- definitionThe exact Hohenberg-Kohn input quoted at equation (2.1): the correct density attains the physical ground energy and minimizes the exact functional over the paper's declared representable fixed-particle-number domain.
- definitionRaw source premises interpreting Kohn and Sham's exact density-minimum token. Equation (2.1) is retained explicitly as an imported Hohenberg-Kohn foundation together with the selected ground-state setup; no independent Kohn-Sham derivation or established shared endpoint is inserted.
- definition
- definition
- definitionEquations (2.6)-(2.7), with the same density and the actual density derivative.
- definition
- definitionEquation (2.3), as the selected local approximation formula.
- definition
- definition
- definition
- definition
- definition
- definitionCalculus and a noninteracting density realization are lower inputs. No self-consistent orbital equation or total-energy conclusion is stored here.
- definition
- definitionEquation (2.21) defines an alternative approximate functional, not the exact universal functional. Exact Fock exchange does not make local correlation exact.
- definitionThese are selected-reference identifications. Equality of densities alone does not identify the kinetic energy of arbitrary Slater determinants.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe nonlocal variational calculation includes its density-to-orbital identification; it is not inferred merely from density reconstruction.
- definition
- definition
- definition
- definition
- definition
- definitionThe paper-local premises needed to ground the exact Hohenberg-Kohn input before using energy attainment, minimization, or the later Kohn-Sham orbital route.
- definitionPaper-local realization of every shared exact variational claim.
- definitionThe uniform-gas exchange derivative is a source calculation, not the final ratio.
- definitionEquations (2.18)-(2.19); the Fermi momentum is computed from the density.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe exact interacting ground-density model selected at equation (2.1).
- definition
- definition
- definition
- definitionThe Kohn-Sham ground-state framework is the theory object. The represented world records the interacting ground state, external potential, and fixed particle-number sector to which the exact variational input applies.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEnergy integrals exist along admitted paths near zero; the scalar potential is a genuine derivative at the selected density.
- definitionThese physical energy integrals must exist, not merely have totalized values.
- definition
- definition
- definitionGround occupation is a variational condition on actual fermionic orbital families; solving eigenvalue equations and counting orbitals is insufficient.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe constrained fundamental lemma is an explicit mathematical input. It concerns the actual admitted density variations, not a named conclusion.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA domain condition, not merely the totalized value of a second derivative.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (A2.2), the partially summed exchange-correlation correction.
- definitionEquation (A2.3), the additional nonlocal effective-potential term.
- definitionThe equation-(A2.2) kernel term, retaining the factor one-half and the corrected squared density difference. Kohn and Sham explicitly note that the corresponding second term in Hohenberg-Kohn equation (83) was in error.
- definition
- definitionThe stationary-property argument after equation (A2.3): when the density change is small, evaluate the energy correction on the unmodified density.
- definition
- definitionThe squared two-point density difference displayed in equation (A2.2).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (4.4), the linearized magnetic Euler equation.
- definitionEquations (4.8)-(4.9), the local uniform-gas spin-kernel approximation.
- definition
- definitionEquations (4.5)-(4.6), susceptibility from the inverse response kernel.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (3.2) decomposes internal free energy, not the entire grand potential.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAnalytic inputs below concern functional derivatives and the reference system, not the target equations.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (3.6) contracted with the actual temperature derivative of the density.
- definition
- definitionLiteral plus sign in printed (3.13), kept distinct from the derived thermodynamic identity.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionUnlike the fixed-number fundamental lemma, unrestricted variations detect constants.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionLiteral leading plus sign from (3.15), not a hypothesis of the thermodynamic route.
- definitionControlled Sommerfeld inputs, not an assertion that every finite box has a bulk T-linear heat law.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe plus here subtracts the thermodynamic leading value, which is negative.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionCompleteness is a substantive Hilbert-space input, not a finite occupied list.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSubstantive descriptive completeness: the selected regime contains at least one physically admissible element, and the description represents every such element. The coverage law alone may hold vacuously on an empty domain.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definition
- definition
- definition
- definition
- definition
- definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
- definition
- definition
- definition
- definition
- definition
- definition
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- structure
- definition
- instance
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- checked statementRaw paper inputs construct a certificate for every Kohn-Sham route.
- definition
- checked statement
- definition
- definition
- definition
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (2.10)'s Hartree double-counting subtraction uses one density. For a frozen input and a different output the missing term is explicit here.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe selected interaction is positive definite on every real charge variation. This finite identity is not a claim about arbitrary XC functionals.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEqual successive energy values are not a convergence certificate. All updates below are genuine normalized ground states of their frozen operator.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe two exact limiting cases are alternatives in the paper, not a single joint hypothesis that must hold before either accuracy branch is available.
- checked statement
- checked statement
- checked statementA nonzero kernel and density contrast do not supply equation (A2.2).
- checked statementThis is an information boundary for one actual energy readout, not a claim that a specified full differentiable functional has no derivative.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementPhysical Review A1133, equation (2.1): the exact Hohenberg-Kohn input used by Kohn-Sham keeps the correct density inside its selected admissible domain, attaining and minimizing the exact functional before orbital approximations.
- checked statementPhysical Review A1133, equation (2.1): the exact Hohenberg-Kohn input used by Kohn-Sham directly realizes the structural explanation of ground-density energy attainment and fixed-particle-number minimization. The later local exchange-correlation approximation and auxiliary orbital equations are not part of this shared explanation.
- checked statement
- checked statement
- checked statementThe exact imported Hohenberg-Kohn functional covers its declared representable-density domain before Kohn and Sham introduce orbital or local-density approximations. This is not completeness on arbitrary positive normalized densities.
- checked statement
- checked statementThe complete Kohn-Sham exact variational route transfers every shared claim to the 1965 theory and represented interacting ground system.
- checked statementThe selected exact ground density is a physically sound representation.
- checked statement
- checked statement
- checked statement
- checked statementPhysical Review A1135: the high-density branch has its own relative-error and reliability conclusion. It does not require slow spatial variation.
- checked statementKohn-Sham imports the Hohenberg-Kohn result and instantiates it only at the selected exact interacting model.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe Kohn-Sham adapter retains the exact Hohenberg-Kohn semantics before any orbital construction or local exchange-correlation approximation is added.
- checked statementPhysical Review A1134 and Appendix I: the slowly varying branch has its own controlled density-accuracy conclusion. It does not require the separate high-density premise from A1135.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (A2.2) exposes its corrected squared-difference kernel term.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
The argument is reconstructed from the Lean main file, source map, coverage proof, and independent fidelity ledger, grounded in the archived original six-page APS article. The finite diagnostics and independent consumer are new tests of inference, not claims attributed to Kohn and Sham. Integrability, weak kinetic-domain membership, noninteracting representability, reference Euler equations, constrained-variation separation, and component functional derivatives remain explicit mathematical inputs. The local and exact orbital equations and energy rearrangements are deductions from those inputs, not cached conclusions. The nonlocal orbital correspondence, uniform-gas and asymptotic calculations, and thermal/spin/rapid extensions retain their separately declared deferred inputs. No local approximation is relabeled exact, and no finite diagnostic is presented as a continuum Coulomb solution.
Exact foundation, practical approximation, and independent extensions must not be collapsed
The ground-state branch starts from an exact imported variational principle and the exact universal decomposition. The local self-consistent equations branch from that exact input and feed the validity assessment. The nonlocal approximation and formal exact reformulation also branch from the exact input directly rather than inheriting the completed local approximation. Finite temperature, spin response, and rapid oscillations begin independently with distinct semantic frameworks.
| Transition | Status | Retained boundary |
|---|---|---|
| Ground state to exact density minimum | imported Hohenberg–Kohn result | Nondegeneracy, particle number, and representable-density domain are explicit. |
| Exact decomposition to local equations | local approximation + analytic inputs | The exact and local exchange-correlation functionals remain distinct. |
| Local solution to accuracy regimes | controlled asymptotic calculations | Slow variation and high density do not imply global accuracy. |
| Surface and large-gap regimes to failure | author assessments | The failure claims retain their qualitative epistemic status. |
| Exact exchange to nonlocal surface behavior | controlled ansatz + author assessment | Exchange improves; local correlation remains inadequate. |
| Thermal and spin foundations to extensions | imported/controlled setups + deferred calculations | Thermal locality, low temperature, weak field, and small magnetization are explicit. |
| Rapid oscillations to correction formulas | deferred calculation + unresolved kernel | The energy correction also needs a small density modification. |
| Exact functional to exact one-particle form | exact derivative + representation inputs | The main conclusion is exact but not an explicit calculational prescription. |
The starting point is an exact interacting density minimum
Select a nondegenerate interacting ground state in an external potential and fix its particle number. The exact total-energy functional contains external-potential energy, Hartree energy, and a universal internal functional. The imported Hohenberg–Kohn input says that the state's density attains the physical ground energy and minimizes this exact functional over densities representable at the same particle number.
Eexact[v,n0] = Eground[v],
Eexact[v,n0] ≤ Eexact[v,n] for every declared representable density n with the same particle number. nondegenerate selected ground state; Physical Review p. A1133, equation (2.1) (1)
The universal functional is then decomposed exactly—not approximately—into a noninteracting kinetic functional and the exact exchange-correlation functional.
The paper-local adapter exposes energy attainment and minimization on the fixed-particle-number density domain without adding orbitals or a local approximation. Equation (2.1) realizes the ordinary explanation and a distinct source-sensitive explanation whose token explicitly retains the imported Hohenberg-Kohn foundation rather than presenting it as a Kohn-Sham derivation.
exact_ground_density_inputs_realize_structural_ground_density_variational_explanation · kohn_sham_imported_foundation_realizes_source_structural_ground_density_variational_explanation · exact_ground_density_realizes_shared_variational_principle · Physical Review p. A1133The local equations use actual spin orbitals and constrained density variations
The ground-state realization uses complex spin orbitals on three-dimensional space, in atomic units. Each occupied slot is normalized; distinct slots are orthogonal. The selected noninteracting reference solves its own orbital equations, realizes the density and T_s, and minimizes the reference energy over admissible families with the same positive count. These are representation and ground-selection inputs, not consequences of a density label.
n(r)=sum_(i,sigma) |psi_i(sigma,r)|^2.
integral sum_sigma conjugate(psi_i)*psi_j dr=delta_ij; integral n dr=N.
K psi=-(1/2) Delta psi; each spin component and its kinetic action are square-integrable.
The weak kinetic identity against every smooth compactly supported test function is required.
The norm-square and spin sum matter: literal complex squares are not densities. Density normalization is derived by integrating the occupied norm-squares. The differential action is a real second derivative on R^3, with a weak-domain condition preventing an undefined totalized derivative from masquerading as a kinetic operator.
E_H[n]=(1/2)*integral n(r)*V_H[n](r) dr.
E_xc_local[n]=integral n(r)*epsilon_xc(n(r)) dr.
mu_xc(n)=d[n*epsilon_xc(n)]/dn.
E_local[v,n]=V_v[n]+E_H[n]+T_s[n]+E_xc_local[n].
The exact exchange-correlation functional remains G[n]-T_s[n]. Its replacement by the local uniform-gas integral is the approximation, not an identity asserted about the exact functional. The chemical potential differentiates density times energy per particle, not energy per particle alone.
The Coulomb integrand defining V_H[n](r) is integrable for almost every r.
d[z*epsilon_xc(z)]/dz at z=n(r) exists and equals mu_xc(n(r)), almost everywhere.
For every admitted delta_n, some eta>0 makes these energy integrals finite at n+t*delta_n for every |t|<eta.
These are explicit domain inputs; a totalized integral or derivative alone is not enough.
The local solution retains this functional domain together with its orbital reference. This prevents a divergent energy integral, or a default derivative at a nondifferentiable scalar function, from being treated as a physically defined local functional. Finite energy along each admitted path is separate from the supplied calculation of its derivative.
For |t|<eta with eta>0, n_t is nonnegative almost everywhere, integrable, normalized to N, and representable.
dE_local[n_t]/dt at t=0=integral delta_n*(v+V_H+q_s+mu_xc) dr.
dT_s[n_t]/dt at t=0=integral delta_n*q_s dr.
Reference Euler input: integral delta_n*(q_s+u_ref) dr=0.
Local stationarity therefore gives integral delta_n*(v+V_H+mu_xc-u_ref) dr=0.
The derivative of each component, reference Euler equation, and required integrals are supplied separately. The variation-separation hypothesis says that a locally integrable function annihilating every admitted fixed-number variation is constant almost everywhere. It is a substantive condition on the admitted directions; it is not automatic for an arbitrary representability domain.
c=(1/N)*integral (v_eff-u_ref)*n dr; epsilon_i=epsilon_i_ref+c.
[-(1/2) Delta+v_eff] psi_i=epsilon_i*psi_i almost everywhere.
n=sum_(i,sigma) |psi_i|^2; integral n dr=N>0.
The selected orthonormal lowest-occupied reference and its kinetic-energy identification are retained.
Comparison of the two Euler integrals derives the potential relation up to an additive constant. Transferring the reference orbital equations then derives the self-consistent equations with shifted eigenvalues. Fixing particle number does not fix an absolute potential, and neither the existence of a solution nor a numerical iteration's convergence has been asserted.
E_local=sum_i epsilon_i-E_H+E_xc_local-integral n*mu_xc dr.
The same normalized self-consistent orbitals and explicit energy integrability are required.
The double-counting formula is derived by integrating the actual orbital equations. It is not an independent equality stored in an energy-calculation premise.
mu_x_KS=-k_F/pi=(2/3)*v_x_Slater.
The uniform-gas exchange derivative is an explicit calculation input.
The local theorem derives the potential gauge, orbital equations, and density representation. A separate theorem derives positive electron number and the integral normalization; another integrates the equations to obtain the total energy. The exchange-only ratio consumes its own uniform-gas calculation, not the local solution as an unnecessary premise.
local_density_stationarity_yields_self_consistent_equations · the_selected_orbital_representation_has_actual_positive_electron_number · local_self_consistent_route_yields_energy_formula · exchange_only_local_potential_is_two_thirds_of_slater · original equations (2.3)-(2.10), (2.18)-(2.19)Two controlled success regimes coexist with two declared failures
For a local self-consistent solution with slowly varying density, the supplied gradient analysis gives density correctness through second gradient order. In the high-density regime, the exchange-correlation error is negligible relative to kinetic energy and the local approximation is reliable.
local solution + high density → exchange-correlation error negligible relative to kinetic energy + local approximation reliable. controlled regimes and deferred asymptotic calculations; pp. A1134–A1135 and Appendix I (6)
The paper also supplies qualitative limitation assessments. In a finite electronic system with rapid density variation and a surface or overlap region, the local approximation is not reliable. It is likewise not reliable in the selected large-gap-insulator regime. The source map classifies both assessments and their conclusions as author expectations.
large-gap insulator → local approximation not reliable. author-qualified limitation assessments; Physical Review p. A1135 (7)
The slowly-varying branch and high-density branch are established by separate theorems; neither requires the other regime. A separate theorem retains the surface and large-gap failures without turning their author-assessment status into a universal mathematical result.
slowly_varying_local_scheme_retains_second_gradient_accuracy · high_density_local_scheme_retains_reliability · local_density_approximation_retains_surface_and_large_gap_limitsThe nonlocal alternative uses a density matrix, not an exchange label
The alternative keeps Fock exchange nonlocal and correlation local. A separate occupied family and density are selected: the local and nonlocal solutions are not forced to coincide. The exchange operator, density matrix, and exchange energy are computed from those complex spin orbitals.
conjugate(gamma(sigma,r;tau,r'))=gamma(tau,r';sigma,r).
(X psi)(sigma,r)=-integral sum_tau gamma(sigma,r;tau,r')*psi(tau,r')/|r-r'| dr'.
E_x=-(1/2)*integral integral sum_(sigma,tau) |gamma(sigma,r;tau,r')|^2/|r-r'| dr' dr.
For every occupied orbital and spin, the action integrand is integrable in r' for almost every r.
The inner and outer exchange-energy integrals are integrable.
mu_c(n)=d[n*epsilon_c(n)]/dn.
[-(1/2) Delta+X+v+V_H+mu_c] psi_i=epsilon_i*psi_i.
n=sum_(i,sigma) |psi_i|^2; the occupied family is orthonormal and in the weak kinetic domain.
This is an alternative approximate functional, not an identity for exact G.
The nonlocal variational correspondence is still an explicit mathematical input. So are the identifications of the selected family's kinetic and Fock energies with the density functionals used here. Equality of densities alone would not establish either identification for arbitrary determinants. The nonlocal solution retains its actual Fock integral domain and the same local-functional domain conditions for correlation alone, with epsilon_c in place of epsilon_xc. The additional Fock contraction is separately exposed; the total-energy rearrangement is then derived.
sum_i epsilon_i=T_s+2*E_x+V_v+2*E_H+integral n*mu_c dr.
E_nonlocal=sum_i epsilon_i-E_H-E_x+E_c_local-integral n*mu_c dr.
The contraction, selected-orbital identifications, and integrability are explicit inputs.
The surface assessment remains asymmetric and author-qualified: nonlocal exchange is expected to improve surface behavior, while local correlation near a surface remains inadequate. Exact Fock exchange does not make the correlation approximation exact.
The route returns the nonlocal solution and surface caveats. Its additional energy theorem derives the two exchange and Hartree subtractions from the actual Hamiltonian expectation.
exact_exchange_route_yields_hartree_fock_like_system_with_caveat · nonlocal_self_consistency_retains_the_exchange_contraction_in_its_energy · original equations (2.21)-(2.25)The finite-temperature extension has its own variational foundation
The thermal route is independent of the completed ground-state route. The imported Mermin minimum concerns the exact grand potential at fixed temperature and chemical potential. Its exact density is distinct from the selected approximate stationary density. Equation (3.2) decomposes the internal free-energy functional, not the entire grand potential.
G_s(T,n)=T_s(T,n)-T*S_s(T,n); F_xc_exact(T,n)=G(T,n)-G_s(T,n).
f_xc(T,n)=f_uniform(T,n)-f_uniform_0(T,n).
F_xc_local(T,n)=integral n(r)*f_xc(T,n(r)) dr.
Omega_local(T,n)=V_v[n]+E_H[n]+G_s(T,n)+F_xc_local(T,n)-mu*integral n dr.
The exact Mermin minimum and the approximate stationary density are separate.
The occupation is computed from the public canonical-weight API on the two allowed occupation states of one fermionic mode. The full noninteracting occupation law is their product measure; the coordinate occupations are independent and have the computed binary Gibbs marginals.
Z_i=1+exp(-beta*(epsilon_i-mu)); p_i(n_i)=exp(-beta*(epsilon_i-mu)*n_i)/Z_i.
f_i=p_i(1)=1/(exp(beta*(epsilon_i-mu))+1); 0<f_i<1.
mean(n_i)=f_i; Var(n_i)=f_i*(1-f_i)>0.
S_i=-k_B*(f_i*log(f_i)+(1-f_i)*log(1-f_i)).
Omega_i=-k_B*T*log(Z_i)=mean(E_i)-T*S_i-mu*mean(n_i).
n(r)=sum_i f_i*sum_sigma |psi_i(sigma,r)|^2; integral n dr=sum_i f_i=N_mean.
T_s=sum_i f_i*kineticEnergy(psi_i); S_s=sum_i S_i.
Normalization, orthogonality, completeness, weak kinetic domains, and actual summability are required.
The chemical potential calibrates N_mean=N>0.
For a finite nonempty set of M available modes at positive temperature, sum_i f_i<M.
The scan prints an upper summation limit N in (3.9). A finite list of exactly N normalized modes, each with occupation strictly below one, cannot also integrate to N particles. The formal realization therefore distinguishes the available spectrum from the mean particle number, and records this literal-notation issue rather than silently identifying the two.
delta Omega_local=integral delta_n*(q_s+v_eff-mu) dr; q_s=delta G_s/delta n.
Grand-canonical density variations may change integral n dr.
Admitted density paths remain nonnegative, integrable, representable, and in the actual local functional domain.
Reference Euler input: integral delta_n*(q_s+u_ref-mu_ref) dr=0.
Stationarity and unrestricted variation separation give v_eff-u_ref=mu-mu_ref almost everywhere.
epsilon_i=epsilon_i_ref+(mu-mu_ref); shifting energy and chemical potential together preserves every f_i and n.
[-(1/2) Delta+v_eff] psi_i=epsilon_i*psi_i almost everywhere.
Functional differentiation, the reference Euler relation, and the separation lemma are explicit analytic inputs. The desired self-consistent system is not a field of the calculation data. The independent exact minimum is retained as source context; it is not used to claim that the local approximation has the same minimizing density.
N(T)=integral n(T,r) dr; Omega(T)=F(T)-mu(T)*N(T).
S(T)=-partial_T[G_s(T,n)+F_xc_local(T,n)] at fixed n=n(T).
Along a stationary density path, -F'(T)=S(T)-mu(T)*N'(T).
Fixed mean particle number near T gives N'(T)=0 and -F'(T)=S(T).
D_xc(T)=integral n(T,r)*partial_T f_xc(T,n(T,r)) dr; S(T)=S_s(T)-D_xc(T).
The calculus inputs include actual derivatives of the temperature-dependent density and free energy, differentiation under the exchange-correlation integral, and the noninteracting entropy identity. Stationarity alone does not remove chemical work when the mean particle number varies.
These two entropy equations agree only when D_xc=0.
Printed (3.15): partial_T f_xc=+A*T*(g_h-g_0).
From f_xc=f-f_0 and s=-partial_T f: partial_T f_xc=-(s_h-s_0).
With s_h-s_0=A*T*(g_h-g_0), the thermodynamic sign is negative.
The two printed sign changes cancel in the displayed leading coefficient; no author-approved correction is asserted.
The literal printed equations are Lean propositions distinct from the thermodynamic deductions. They are not assumed simultaneously with incompatible nonzero corrections. The controlled reconstruction below reaches the displayed final coefficient with the thermodynamically consistent signs.
A supplied energy-counting measure defines C(E)=measure((E_floor,E])/normalization; g=C'(mu_0).
Finite band masses, positive normalization, and the actual nonnegative count derivative are required.
The effective-state count is normalized by N; its g_s is distinct from the homogeneous interacting g_h and noninteracting g_0.
D=integral n_0(r)*(g_h(n_0(r))-g_0(n_0(r))) dr.
gamma=A*(N*g_s+D).
S(T)=gamma*T+r_s(T)-r_xc(T).
C_V(T)=T*S'(T); C_V(T)/T=gamma+r_s'(T)-r_xc'(T).
The remainders are defined from the actual component functions, not supplied heat-capacity values.
|r_s(T)|<=d_s(T)*T; |r_xc(T)|<=d_xc(T)*T.
|r_s'(T)|<=d_s(T); |r_xc'(T)|<=d_xc(T), with actual differentiability.
|S(T)/T-gamma|<=d_s(T)+d_xc(T); |C_V(T)/T-gamma|<=d_s(T)+d_xc(T).
If the valid regime persists as T tends to 0 from above and both error budgets vanish, C_V(T)/T tends to gamma.
An entropy asymptotic alone does not supply the required derivative limit.
Remaining analytic scope. A complete, summable spectral reference, representability, functional and temperature calculus, and the density-of-states estimates remain explicit inputs. A finite discrete spectrum is not automatically a bulk Sommerfeld limit. The exact-exchange thermal alternative mentioned but not developed by the authors is not supplied here. Spin, gradient-accuracy, and rapid-oscillation routes still retain their separate deferred calculations.
The thermal solution contains complex spectral orbitals, computed occupations, calibrated mean number, and the noninteracting free-energy identification. The caloric theorem contains the actual free-energy slope, entropy derivative, and controlled entropy and heat estimates, together with a physical reference density.
finite_temperature_variational_route_yields_thermal_equations · low_temperature_route_yields_specific_heat_formula · ThermalPhysics · original section III, A1136-A1137A weak field produces a linearized spin-response problem
The spin route selects a zero-field density in a paramagnetic reference state, a weak magnetic field, and a small magnetization. A supplied quadratic expansion and kernel inversion give three linked outputs.
susceptibility = integral of the inverse spin kernel,
local spin-kernel value = inverse interacting uniform susceptibility − inverse noninteracting uniform susceptibility. weak-field and small-magnetization expansion; equations (4.2)–(4.9) (10)
The theorem returns the linearized Euler equation, inverse-kernel susceptibility, and local uniform-gas spin-kernel approximation together.
weak_field_expansion_yields_spin_response_and_local_kernel · Physical Review p. A1137Short-wavelength density oscillations admit a formal correction with an unresolved kernel
For an infinite electronic system with rapid quantum density oscillations, a supplied partial summation corrects both the exchange-correlation energy and the effective potential. If the induced density modification is small, stationarity permits a first-order energy correction evaluated on the unmodified density.
Exccorrected = Exclocal − kernel correction,
veffcorrected = veffbase + rapid-oscillation correction potential,
small density modification → Ecorrected = Ebase + first-order correction. Appendix-II calculation; equations (A2.1)–(A2.3), including the stated correction to Hohenberg–Kohn equation (83) (11)
The route simultaneously retains that a reliable beyond-RPA kernel is unavailable. The correction is therefore a formal structural result with an explicit open input, not a numerically closed prescription.
The theorem returns both corrected equations, the conditional first-order energy relation, and the kernel nonavailability statement. The corrected exchange-correlation equation separately exposes the one-half-weighted squared-density-difference kernel term.
corrected_exchange_correlation_equation_retains_a2_two_kernel_formula · rapid_oscillation_route_yields_formal_correction_with_kernel_caveat · Physical Review p. A1138Formal exactness needs a derivative and a representation, not a known explicit formula
The note added in proof returns directly to the exact foundation. The ground-state minimum is imported on the actual fixed-N representable domain. A domain-representation bridge makes that minimum apply to the admitted density variations. Differentiability then gives stationarity, rather than treating stationarity as a new unexplained exact-ground-state axiom.
dE_xc_exact[n+t*delta_n]/dt at t=0=integral delta_n*v_xc_exact dr.
The derivative concerns this same exact functional on admitted fixed-N variations.
A known explicit formula is not a premise of the exact orbital theorem.
Noninteracting representability, the lowest-occupied reference, kinetic and Coulomb derivatives, the reference Euler equation, variation separation, local and energy integrability, and the density-domain bridge remain explicit. Those inputs are stronger than merely giving a name to the exact exchange-correlation functional.
epsilon_i_exact=epsilon_i_ref+c_exact.
[-(1/2) Delta+v_eff_exact] psi_i=epsilon_i_exact*psi_i almost everywhere.
n_0=sum_(i,sigma) |psi_i|^2; integral n_0 dr=N>0.
E_exact[v,n_0]=E_ground[v].
This identity uses the same exact functional and normalized selected orbitals, without the local approximation.
The exact route derives these equations and the energy identity without inheriting the local exchange-correlation formula. It is conditional formal exactness, not a construction of all analytic inputs or a numerical method for the unknown many-body functional.
Separately supplied author-status premise: no explicit exact potential formula is known.
The paired result retains both; it does not prove nonavailability from the functional's existence.
The exact theorem derives stationarity from the imported minimum and follows the same actual orbital and energy reasoning. The availability statement is a separate author-status input. The finite diagnostic below tests the substantive weaker inference from one energy readout to a derivative, not an invented theorem that a specified differentiable functional has no formula.
exact_functional_yields_exact_one_particle_formulation · formal_exact_formulation_retains_explicit_potential_obligation · exact_formulation_does_not_inherit_local_density_approximation · note added in proof, A1138Physical countermodels expose missing hypotheses
The following finite diagnostics compute densities, overlaps, Hamiltonians, derivatives, and energies from actual complex wavefunctions. They test logical shortcuts; they are not continuum realizations of the original Coulomb problem.
Two occupied copies of psi each have norm 1 and total density mass 2, but their overlap is 1, not 0.
K=[[1,-1],[-1,1]]; psi_plus=(1,1)/sqrt(2); psi_minus=(1,-1)/sqrt(2).
Both densities are (1/2,1/2), but their kinetic energies are 0 and 2.
H=diag(0,1): (0,1) is stationary for the Rayleigh quotient in every complex direction, but is not a minimum.
H_approx=diag(1,0) has a ground state that is not a ground state of H.
A ground-state iteration can cycle despite an available self-consistent minimum
A two-site repulsive Hartree model retains a positive kinetic quadratic form and a genuine quadratic density interaction. The Hartree potential is proved to be the derivative of that interaction energy. All selected ground-state bounds hold against every normalized complex state, not just two candidate labels.
rho_j=|psi_j|^2; V_H=C*rho; E_H=(1/2)*rho dot C*rho.
H[rho]=K+diag(V_H); E[psi]=psi_dagger*K*psi+E_H[rho].
dE_H[rho+t*delta_rho]/dt at t=0=delta_rho dot V_H.
psi_A=(3,1)/sqrt(10); psi_B=(1,3)/sqrt(10); psi_star=(1,1)/sqrt(2).
rho_A=(9/10,1/10); rho_B=(1/10,9/10); rho_star=(1/2,1/2).
H[rho_B]=[[3,-3/2],[-3/2,7]] has ground state psi_A with eigenvalue 5/2.
H[rho_star]=[[5,-3/2],[-3/2,5]] has ground state psi_star with eigenvalue 7/2.
For every normalized complex psi: E[psi]-7/4=(3/2)*|psi_0-psi_1|^2+(5/4)*(rho_0-rho_1)^2.
Thus psi_star is a self-consistent global minimum, while exact ground updates alternate A,B,A,B,...
Every update solves its actual ground eigenproblem; the density has no limit.
This disproves an unconditional inference from correct ground-state diagonalization to convergence of the undamped self-consistency iteration. It does not rule out a separately justified damping or convergence method.
The nonselfconsistent substitution 5/2-E_H[rho_A]=-1/20 is not E[psi_B]=63/20.
At the fixed point, E[psi_star]=7/4=7/2-E_H[rho_star], with E_H[rho_star]=7/4.
Even the self-consistent eigenvalue 7/2 is not the total energy 7/4.
F(rho)=rho_1 and G(rho)=rho_0 agree at rho=(1/2,1/2).
Along rho(t)=(1/2+t,1/2-t), their actual derivatives are -1 and 1.
A constant potential shift 2 pairs to zero with every fixed-number variation.
The same normalized state has energy 0 under diag(0,1) and energy 2 under diag(2,3).
These checks separate energy per particle from its local potential, a single functional value from a functional derivative, and a fixed-number variational equation from a choice of absolute potential. They do not claim that an entire specified differentiable functional fails to determine its derivative.
OrbitalDiagnostics · the_exact_ground_update_cycle_has_no_density_limit · the_nonselfconsistent_eigenvalue_cannot_be_used_in_the_total_energy_formula · one_energy_readout_does_not_supply_a_functional_derivative
Thermal inference boundaries
Eight additional boundaries use actual fermionic Gibbs ensembles, a normalized continuum density with quadratic internal free energies, and a differentiable thermodynamic path. They test implications rather than claim to solve a microscopic material.
Their mean particle number is 1, their number variance is 1/2, and each mode has occupation 1/2.
The fixed-one-particle sector has two configurations of probability 1/2 and number variance 0.
Both site occupation densities are (1/2,1/2), but the entropies at k_B=1 are 2*log(2) and log(2).
Two available modes are not two mean particles; mean-number calibration is not a sharp-number constraint.
At T=1, the actual grand free energy is stationary with respect to occupation.
N'(1)=exp(-1)/(1+exp(-1))^2>0.
The actual Gibbs means give F'(1)=-S(1)+mu*N'(1), so -F'(1) is not S(1).
As T tends to 0 from above, f(T) tends to 0.
Direct substitution T=0 in the totalized reciprocal formula gives 1/2.
The formula is not continuous at that substituted endpoint; substitution is not a physical zero-temperature limit.
f_uniform(T)=-2*T^2; f_uniform_0(T)=-T^2; f_xc(T)=-T^2.
The actual entropy and heat capacity are S(T)=4*T and C_V(T)=4*T; S_s(T)=2*T.
D_xc(T)=-2*T; the printed entropy sum S_s+D_xc is 0, not 4*T.
The uniform entropy difference is 2*T, while partial_T f_xc=-2*T.
Both entropy and heat are positive for T>0; this is a thermodynamic sign diagnostic, not a microscopic material model.
S(T)/T tends to 3 as T tends to 0 from above.
C(T)=T*S'(T); S'(T)=3+2*T*sin(1/T)-cos(1/T) for T!=0.
Both S(T) and C(T) are positive for 0<T<1/4.
Along T_j=1/(2*pi*(j+1)), C(T_j)/T_j=2, so C(T)/T does not tend to 3.
Small entropy remainders do not ensure small derivative remainders.
ThermalDiagnostics · actual_grand_canonical_stationarity_does_not_identify_entropy_with_the_helmholtz_path_slope · the_entropy_asymptotic_does_not_supply_the_same_specific_heat_asymptotic
Independent quantum models exercise the public library
The independent condensed-matter consumer imports the public density-functional framework, not paper modules or their countermodels. It proves a three-site constrained-search minimum from actual wavefunctions and then applies four shared API conclusions.
E[psi]=3*sum_j |psi_j|^2-|sum_j psi_j|^2=sum_(j<k) |psi_j-psi_k|^2.
Admissible rho: rho_j>=0 and sum_j rho_j=1.
T_s[rho]=3-(sum_j sqrt(rho_j))^2; psi_j=sqrt(rho_j) realizes its minimum.
Every normalized complex wave with density rho has energy at least T_s[rho].
rho_star=(1/3,1/3,1/3) attains T_s=0.
Changing the middle sign preserves rho_star but gives energy 8/3.
rho_bad=(4,0,0) has totalized T_s=-1 but lies outside the fixed-number domain.
The shared route is established from the physical setup and the independently proved variational calculation. It yields route applicability, the established variational principle, a nonvacuous selected minimum, and a bound for every admissible density. The negative out-of-domain value demonstrates why the admissibility predicate cannot be discarded. This is independent reuse of exact finite density logic, not a proof of continuum Kohn-Sham representability.
Independent three-site density-variational consumer · Public-API proof-use auditAn independent three-mode thermal consumer
A second construction uses the public canonical normalization, probability, mean, and log-weight APIs. It has three nonzero-energy modes and eight grand-canonical configurations, distinct from the production two-mode controls. It imports neither paper modules nor production witnesses.
Each mode has occupation 1/3; the grand mean number is 1 and its variance is 2/3.
The three fixed-one-particle configurations each have probability 1/3 and number variance 0.
Both site occupation densities are (1/3,1/3,1/3).
S_grand=3*log(3)-2*log(2); S_fixed=log(3); these entropies differ.
P_grand(N=1)=4/9; conditioning on that sector gives probability 1/3 for each one-particle configuration.
The probabilities, densities, fluctuations, and entropies are computed from the actual energy functions.
Concept guide
Exact ground-density minimum
The exact density attains the physical ground energy and minimizes the exact functional over representable densities with the same particle number.
HohenbergKohnVariationalFoundationExact universal decomposition
The identity separating the universal functional into noninteracting kinetic energy and the exact exchange-correlation functional.
ExactUniversalDecompositionLocal exchange-correlation approximation
The replacement of exact exchange-correlation energy by the selected uniform-gas integral evaluated on the local density.
LocalExchangeCorrelationFormulaLocal self-consistent solution
The local effective potential, complex occupied-orbital equations, norm-square density reconstruction, positive particle count, selected orthonormal lowest reference, actual local-functional domain, and a.e. potential gauge relation. Integral normalization is derived.
LocalSelfConsistentSolutionOrbital-energy formula
The local total-energy expression formed from occupied orbital energies with Hartree and exchange-correlation double-counting subtractions.
LocalTotalEnergyFormulaSlater exchange comparison
The exchange-only statement that the local Kohn–Sham exchange potential equals two-thirds of Slater's potential.
SlaterExchangeComparisonControlled accuracy regimes
Independent limiting branches: second-gradient density accuracy for slow variation, and reliable high-density behavior with negligible relative exchange-correlation error.
slowly_varying_local_scheme_retains_second_gradient_accuracy · high_density_local_scheme_retains_reliabilitySurface and large-gap limits
Author-qualified failures of local reliability in rapid surface/overlap regions and large-gap insulators.
local_density_approximation_retains_surface_and_large_gap_limitsExact-exchange/local-correlation alternative
A Hartree–Fock-like nonlocal exchange system retaining a local correlation term and its surface caveat.
NonlocalExchangeDecompositionThermal self-consistent solution
A complete complex spectral reference with actual Gibbs occupations, normalized mean particle number, weak kinetic domains, the derived effective potential, and the same noninteracting free energy. Mean-number calibration does not make the particle number sharp.
ThermalSelfConsistentSolutionWeak-field spin response
The linearized magnetic Euler equation, inverse-kernel susceptibility, and local uniform-gas kernel correction.
SpinResponseCalculationRapid-oscillation correction
The formal exchange-correlation and effective-potential corrections for short-wavelength density oscillations.
RapidOscillationCorrectionCalculationBeyond-RPA kernel obligation
The explicit statement that a reliable response kernel beyond the selected approximation is unavailable.
reliableBeyondRPAKernelAvailableExact one-particle formulation
The exact potential, orbital equations, normalized density, and energy derived from the exact functional derivative, imported minimum, and explicit analytic and representation premises.
ExactOneParticleFormulationExplicit-potential obligation
A separately supplied author-status statement about an unavailable explicit exact potential formula, not a mathematical nonexistence theorem.
ExplicitExactExchangeCorrelationPotentialKnownShared ground-density variational model
The reusable exact interacting density minimum grounded in a selected state, external potential, and fixed-particle-number world.
sharedGroundDensityModelComplete route inventory, non-implications, and provenance
The source map declares eight routes, sixty-nine claims, and sixty-nine sourced steps. Coverage interprets every atom through the ground-state, thermal, spin, or rapid-oscillation semantics and certifies every route from checked premise maps. Its exhaustive theorem constructs all eight certificates from raw paper-local inputs. The exact one-particle formulation is the main conclusion; the explicit-potential obligation is a separate output of the same route.
| Route | Direct dependencies | Declared outputs | Profile |
|---|---|---|---|
| Exact variational foundation | — | Selected exact setup, imported foundation, exact decomposition, shared variational result | imported exact principle |
| Local self-consistent equations | Exact foundation | Local solution, positive density normalization, energy formula, Slater comparison | local approximation + calculations |
| Accuracy and scope | Local equations | Two controlled successes; surface and large-gap failures | controlled + author-qualified |
| Nonlocal exchange alternative | Exact foundation | Nonlocal solution and energy, improved exchange surface behavior, correlation caveat | controlled ansatz + assessment |
| Finite-temperature extension | — | Thermal self-consistent solution and low-temperature specific heat | imported + controlled |
| Spin-response extension | — | Linear response, susceptibility, local spin kernel | weak-field expansion |
| Rapid-oscillation correction | — | Corrected functional, potential, first-order energy, unavailable kernel | formal correction + open input |
| Exact one-particle formulation | Exact foundation | Exact formulation and orbital energy, separate explicit-potential obligation | formally exact, not explicit |
Exact variational foundation · exact_variational_foundation_route_is_semantically_realized
Local self-consistent equations · local_self_consistent_equations_route_is_semantically_realized
Accuracy and scope · accuracy_and_scope_route_is_semantically_realized
Nonlocal exchange alternative · nonlocal_exchange_alternative_route_is_semantically_realized
Finite temperature · finite_temperature_extension_route_is_semantically_realized
Spin response · spin_response_extension_route_is_semantically_realized
Rapid oscillations · rapid_oscillation_correction_route_is_semantically_realized
Exact one-particle formulation · exact_one_particle_formulation_route_is_semantically_realized
Twenty-seven formally checked limits of inference
| Available fact | Conclusion not supplied | Actual witness or retained scope |
|---|---|---|
| Approximate ground state | Exact ground state | Opposite diagonal two-site Hamiltonians |
| Slowly varying density | High density | Separate gradient and density scales |
| High density | Slowly varying density | The converse scale separation |
| Accuracy in two limits | Global accuracy | Independent surface error |
| Normalized reconstructed density | Orbital eigenvalue equation | Site state under graph kinetic operator |
| One energy readout | A specified functional derivative | Equal diagonal expectations, opposite derivatives |
| A named rapid kernel correction | The actual (A2.2) formula | Nonzero kernel and density contrast |
| An available formal kernel correction | Small induced density change | A selected large modification |
| A formal kernel correction with a large density change | Reliable first-order corrected energy | A failed energy relation |
| Complex orbital density | Literal complex square | Actual global phase change |
| Normalized occupied slots | Orthogonality | Repeated normalized state |
| Equal density | Equal kinetic energy for arbitrary states | Plus and minus graph eigenstates |
| Full Rayleigh stationarity | Ground minimum | Normalized excited eigenstate |
| A genuine ground-state update | Self-consistency | Repulsive Hartree update A to B |
| Repeated exact ground-state updates | Density convergence | Actual alternating cycle with no limit |
| Nonselfconsistent eigenvalue and old density | Correct total energy formula | -1/20 versus 63/20 |
| Self-consistent eigenvalue | Total energy | 7/2 versus 7/4 |
| Energy per particle | Its density-functional potential | 4 versus 12 |
| Fixed-number variation equation | Absolute potential | Constant shift changes energy by particle number times shift |
| Two available thermal modes | Two mean particles | Actual mean one with both occupations one half |
| Calibrated mean particle number | Sharp particle-number sector | Nonzero grand-canonical number variance |
| Equal site density and mean number | Equal ensemble entropy | Two-mode grand and fixed-number Gibbs ensembles |
| Positive-temperature Gibbs occupations | Continuous zero-temperature substitution | Actual limit zero versus totalized value one half |
| Actual grand-canonical stationarity | Entropy equals negative Helmholtz path slope | Nonzero chemical work at fixed chemical potential |
| Normalized density and positive entropy and heat | Printed entropy plus sign | Quadratic free-energy derivatives give four, not zero |
| Actual uniform entropy difference | The same-sign free-energy derivative | Two versus minus two |
| Leading entropy coefficient and positive heat | The same leading heat coefficient | Oscillatory derivative remainder |
Scope of the countermodels
Thirteen ground-state orbital or functional cases use actual complex waves, Hermitian matrices, normalization, integrals or finite sums, and derivatives. Six retained reduced controls concern gradient/density accuracy and rapid-oscillation formulas. Eight thermal boundaries use computed Gibbs ensembles, a normalized continuum density, and actual free-energy and entropy derivatives. These are inference tests, not microscopic material models. None proves empirical accuracy, an arbitrary continuum solution, or mathematical nonavailability of an exact potential formula. The rapid-kernel semantics also preserve the distinction from the half-displacement product printed in Hohenberg-Kohn equation (83).
Machine-checked audit boundary
argument_wellFormed, argument_auditable, routes_wellFormed, and routes_have_exact_predecessor_graph certify graph structure. local_result_steps_apply_selected_inputs_and_contracts, accuracy_and_nonlocal_steps_apply_selected_inputs_and_contracts, independent_extension_steps_apply_selected_inputs_and_contracts, and formal_exact_steps_apply_selected_inputs_and_contracts lock the checked premise lists. every_source_claim_has_semantics covers all sixty-nine claims, and route_semantic_realization_is_exhaustive constructs all eight routes from raw inputs. limiting_accuracy_branches_do_not_inherit_each_other checks both positive limiting-branch dependencies and both non-inheritances. local_self_consistent_solution_retains_imported_foundation_and_approximation, rapid_correction_retains_unresolved_kernel_obligation, exact_formulation_does_not_inherit_local_density_approximation, explicit_potential_obligation_depends_on_exact_formulation_and_missing_formula, and alternative_and_formal_exact_routes_do_not_absorb_local_approximation preserve the decisive exact/approximate/open boundaries.
Lean-encoded bibliographic record
W. Kohn and L. J. Sham, Self-Consistent Equations Including Exchange and Correlation Effects, Physical Review (1965), A1133–A1138.
TraceComplete Lean semantic identifier ledger
Checked paper-local theorems: density_is_nonnegative, normalization_gives_the_actual_electron_count, a_constant_potential_shift_preserves_the_orbitals, the_orbital_equation_has_an_actual_density_weighted_identity, a_normalized_orbital_energy_is_its_hamiltonian_expectation, the_eigenvalue_sum_counts_the_full_effective_potential, the_actual_density_matrix_is_hermitian, a_general_normalized_orbital_energy_is_its_actual_hamiltonian_expectation, the_total_energy_removes_hartree_and_correction_double_counting, local_chemical_potential_is_not_just_the_energy_per_particle, the_hartree_mean_is_twice_the_hartree_energy, a_potential_gauge_shift_changes_energy_by_charge, Reference.a_realized_density_has_the_normalized_particle_number, separate_functional_derivatives_give_the_actual_total_energy_variation, an_actual_constrained_minimum_gives_stationarity_only_with_differentiability, the_actual_stationary_derivative_gives_the_local_euler_integral, comparing_the_two_euler_integrals_retains_fixed_number_variations, fixed_number_stationarity_determines_a_potential_only_up_to_a_constant, the_potential_gauge_constant_is_fixed_by_the_density_mean, the_normalized_stationary_density_identifies_the_selected_gauge_shift, the_noninteracting_reference_transfers_to_the_self_consistent_local_equations, shared_ground_density_model_retains_exact_semantics, paper_setup_realizes_shared_selected_ground_density_setup, hohenberg_kohn_foundation_realizes_shared_variational_bridge, hohenberg_kohn_foundation_realizes_selected_variational_calculation, exact_ground_density_makes_shared_variational_route_applicable, exact_ground_density_inputs_realize_structural_ground_density_variational_explanation, kohn_sham_imported_foundation_realizes_source_structural_ground_density_variational_explanation, exact_ground_density_establishes_shared_variational_result, exact_ground_density_exhibits_nonvacuous_shared_variational_principle, exact_ground_density_setup_realizes_physically_sound_shared_representation, exact_ground_density_realizes_scoped_descriptive_completeness, exact_ground_density_model_inputs_establish_theory_model_grounding, exact_ground_density_establishes_theory_model_grounded_variational_result, exact_ground_density_route_transfers_every_shared_claim, exact_ground_density_realizes_shared_variational_principle, local_density_stationarity_yields_self_consistent_equations, the_selected_orbital_representation_has_actual_positive_electron_number, selected_orbital_energy_accounting_uses_the_actual_correction_mean, local_self_consistent_route_yields_energy_formula, exchange_only_local_potential_is_two_thirds_of_slater, slowly_varying_local_scheme_retains_second_gradient_accuracy, high_density_local_scheme_retains_reliability, local_density_approximation_retains_surface_and_large_gap_limits, exact_exchange_route_yields_hartree_fock_like_system_with_caveat, nonlocal_self_consistency_retains_the_exchange_contraction_in_its_energy, the_exact_variation_energy_is_the_same_exact_density_functional, the_imported_exact_minimum_controls_the_actual_admitted_density_variations, exact_functional_yields_exact_one_particle_formulation, formal_exact_formulation_retains_explicit_potential_obligation, finite_temperature_variational_route_yields_thermal_equations, low_temperature_route_yields_specific_heat_formula, weak_field_expansion_yields_spin_response_and_local_kernel, corrected_exchange_correlation_equation_retains_a2_two_kernel_formula, rapid_oscillation_route_yields_formal_correction_with_kernel_caveat, the_real_wave_has_its_actual_density, the_real_wave_has_its_actual_norm, both_site_states_are_normalized, the_two_test_hamiltonians_are_hermitian, diagonal_energies_are_computed_from_the_wave, an_approximate_ground_state_need_not_be_an_exact_ground_state, a_global_complex_phase_preserves_density_but_not_the_literal_square, two_normalized_occupied_slots_do_not_supply_orthogonality, a_normalized_reconstructed_density_does_not_supply_an_eigenvector, the_graph_kinetic_energy_is_a_positive_square, both_phases_have_the_same_normalized_density, the_same_density_does_not_fix_the_kinetic_energy_of_arbitrary_states, a_stationary_normalized_state_need_not_minimize_the_energy, the_finite_hartree_potential_is_the_actual_energy_derivative, the_repulsive_hartree_kinetic_energy_is_nonnegative, the_hartree_hamiltonian_is_hermitian, the_trial_charge_profiles_are_computed, both_trial_waves_are_normalized, the_selected_hartree_hamiltonians_are_computed, the_two_updates_and_the_fixed_point_solve_the_actual_eigenproblems, the_three_hamiltonian_lower_bounds_are_actual_squares, a_normalized_eigenvector_has_its_actual_eigenvalue_energy, each_update_really_selects_a_ground_state, a_ground_eigenproblem_update_need_not_be_self_consistent, the_total_hartree_energy_has_its_actual_minimum_identity, the_trial_total_energies_and_hartree_means_are_computed, the_balanced_fixed_point_minimizes_the_actual_total_energy, every_step_of_the_cycle_solves_the_actual_ground_eigenproblem, the_iterated_density_stays_a_fixed_distance_from_the_fixed_point, correct_ground_state_updates_do_not_establish_self_consistent_convergence, the_exact_ground_update_cycle_has_no_density_limit, the_nonselfconsistent_eigenvalue_cannot_be_used_in_the_total_energy_formula, the_selfconsistent_total_energy_removes_the_actual_hartree_double_count, the_local_energy_per_particle_does_not_equal_its_potential, the_diagonal_density_functionals_are_actual_state_energies, the_two_fixed_number_functional_derivatives_are_computed, one_energy_value_does_not_identify_a_functional_derivative, a_constant_potential_shift_has_its_actual_charge_weight, fixed_number_variations_do_not_fix_the_absolute_potential, local_functional_minimizer_need_not_minimize_exact_functional, limiting_accuracy_regimes_are_not_joint_requirements, accuracy_in_two_limits_does_not_imply_global_accuracy, density_reconstruction_does_not_supply_orbital_equation, one_energy_readout_does_not_supply_a_functional_derivative, named_rapid_kernel_correction_does_not_supply_equation_a2_two, formal_kernel_correction_without_small_density_change_does_not_fix_energy.
Checked route-realization theorems: every_source_claim_has_semantics, exact_variational_foundation_route_is_semantically_realized, local_self_consistent_equations_route_is_semantically_realized, accuracy_and_scope_route_is_semantically_realized, nonlocal_exchange_alternative_route_is_semantically_realized, finite_temperature_extension_route_is_semantically_realized, spin_response_extension_route_is_semantically_realized, rapid_oscillation_correction_route_is_semantically_realized, exact_one_particle_formulation_route_is_semantically_realized, route_semantic_realization_is_exhaustive.
Checked source-map theorems: alternative_and_formal_exact_routes_do_not_absorb_local_approximation, argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, local_result_steps_apply_selected_inputs_and_contracts, accuracy_and_nonlocal_steps_apply_selected_inputs_and_contracts, independent_extension_steps_apply_selected_inputs_and_contracts, formal_exact_steps_apply_selected_inputs_and_contracts, local_self_consistent_solution_retains_imported_foundation_and_approximation, limiting_accuracy_branches_do_not_inherit_each_other, rapid_correction_retains_unresolved_kernel_obligation, exact_formulation_does_not_inherit_local_density_approximation, explicit_potential_obligation_depends_on_exact_formulation_and_missing_formula.
Semantic atoms: exactGroundStateSetup, hohenbergKohnVariationalFoundation, sharedGroundDensityVariationalPrinciple, exactUniversalDecomposition, localExchangeCorrelationFormula, localStationarity, occupiedCount, localStationarityCalculation, localEffectivePotentialEquation, localOneElectronEquations, densityFromOccupiedOrbitals, selectedLocalOrbitalAdmissibility, localReferenceGauge, localSelfConsistentSolution, localElectronNormalization, localEnergyCalculation, localTotalEnergyFormula, slaterExchangeCalculation, slaterExchangeComparison, slowlyVaryingDensity, highDensity, slowVariationAccuracyCalculation, highDensityAccuracyCalculation, densityCorrectThroughSecondGradientOrder, highDensityApproximationReliable, finiteRapidSurfaceSetup, surfaceLimitationAssessment, surfaceApproximationFailure, largeGapSetup, largeGapLimitationAssessment, largeGapApproximationFailure, nonlocalExchangeDecomposition, nonlocalOccupiedCount, nonlocalStationarity, nonlocalStationarityCalculation, nonlocalSelfConsistentSolution, nonlocalEnergyCalculation, nonlocalTotalEnergyFormula, nonlocalSurfaceAssessment, nonlocalExchangeSurfaceImproved, localCorrelationSurfaceCaveat, finiteTemperatureFoundation, exactThermalDecomposition, localThermalExchangeCorrelationFormula, thermalStationarity, thermalStationarityCalculation, thermalSelfConsistentSolution, lowTemperatureRegime, lowTemperatureSpecificHeatCalculation, lowTemperatureSpecificHeatFormula, weakFieldSpinSetup, spinResponseCalculation, linearizedSpinResponseEquation, susceptibilityFromInverseKernel, localSpinKernelApproximation, infiniteRapidOscillationSetup, smallDensityModification, beyondRPAKernelUnavailable, rapidOscillationCorrectionCalculation, firstOrderEnergyCorrectionCalculation, correctedExchangeCorrelationEquation, correctedPotentialEquation, firstOrderEnergyCorrectionEquation, exactExchangeCorrelationFunctionalDerivative, exactOneParticleCalculation, exactOneParticleFormulation, exactTotalEnergyFormula, explicitExactPotentialNotKnown, exactFormulationRetainsExplicitPotentialObligation.
Source claims: exactSetup, hkFoundation, sharedVariational, universalDecomposition, localXCFormula, localStationary, occupiedCount, localCalculation, localEffectivePotential, localOrbitalEquations, localDensityReconstruction, localOrbitalAdmissibility, localGauge, localSolution, localNormalization, localEnergyCalculation, localEnergyFormula, slaterCalculation, slaterComparison, slowlyVarying, highDensity, slowAccuracyCalculation, highAccuracyCalculation, secondGradientAccuracy, highDensityReliability, surfaceSetup, surfaceAssessment, surfaceFailure, largeGap, largeGapAssessment, largeGapFailure, nonlocalDecomposition, nonlocalOccupiedCount, nonlocalStationary, nonlocalCalculation, nonlocalSolution, nonlocalEnergyCalculation, nonlocalEnergyFormula, nonlocalAssessment, nonlocalSurfaceImproved, correlationSurfaceCaveat, thermalFoundation, thermalDecomposition, thermalLocalFormula, thermalStationary, thermalCalculation, thermalSolution, lowTemperature, specificHeatCalculation, specificHeatFormula, spinSetup, spinCalculation, spinResponseEquation, susceptibility, localSpinKernel, rapidSetup, smallModification, kernelUnavailable, rapidCalculation, correctionEnergyCalculation, correctedXC, correctedPotential, firstOrderEnergy, exactFunctional, exactCalculation, exactFormulation, exactEnergyFormula, explicitPotentialUnknown, explicitPotentialObligation.
Source-ordered inference steps: stateExactSetup, stateHkFoundation, realizeSharedVariational, stateUniversalDecomposition, stateLocalXCFormula, stateLocalStationary, stateOccupiedCount, stateLocalCalculation, deriveLocalEffectivePotential, deriveLocalOrbitalEquations, deriveLocalDensityReconstruction, deriveLocalOrbitalAdmissibility, deriveLocalGauge, deriveLocalSolution, deriveLocalNormalization, stateLocalEnergyCalculation, deriveLocalEnergyFormula, stateSlaterCalculation, deriveSlaterComparison, stateSlowlyVarying, stateHighDensity, stateSlowAccuracyCalculation, stateHighAccuracyCalculation, deriveSecondGradientAccuracy, deriveHighDensityReliability, stateSurfaceSetup, stateSurfaceAssessment, deriveSurfaceFailure, stateLargeGap, stateLargeGapAssessment, deriveLargeGapFailure, stateNonlocalDecomposition, stateNonlocalOccupiedCount, stateNonlocalStationary, stateNonlocalCalculation, deriveNonlocalSolution, stateNonlocalEnergyCalculation, deriveNonlocalEnergyFormula, stateNonlocalAssessment, deriveNonlocalSurfaceImproved, deriveCorrelationSurfaceCaveat, stateThermalFoundation, stateThermalDecomposition, stateThermalLocalFormula, stateThermalStationary, stateThermalCalculation, deriveThermalSolution, stateLowTemperature, stateSpecificHeatCalculation, deriveSpecificHeatFormula, stateSpinSetup, stateSpinCalculation, deriveSpinResponseEquation, deriveSusceptibility, deriveLocalSpinKernel, stateRapidSetup, stateSmallModification, stateKernelUnavailable, stateRapidCalculation, stateCorrectionEnergyCalculation, deriveCorrectedXC, deriveCorrectedPotential, deriveFirstOrderEnergy, stateExactFunctional, stateExactCalculation, deriveExactFormulation, deriveExactEnergyFormula, stateExplicitPotentialUnknown, deriveExplicitPotentialObligation.
Independent argument routes: exactVariationalFoundation, localSelfConsistentEquations, accuracyAndScope, nonlocalExchangeAlternative, finiteTemperatureExtension, spinResponseExtension, rapidOscillationCorrection, exactOneParticleFormulation.
Argument-route classifications: importedDensityVariationalFoundation, localDensityApproximation, controlledLimitsAndFailures, exactExchangeLocalCorrelation, thermalDensityFunctional, weakFieldSpinResponse, shortWavelengthCorrection, formalExactReformulation.
Current checked semantic identifiers
These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.
Primary semantic theorems (212)
density_is_nonnegative, normalization_gives_the_actual_electron_count, a_constant_potential_shift_preserves_the_orbitals, the_orbital_equation_has_an_actual_density_weighted_identity, a_normalized_orbital_energy_is_its_hamiltonian_expectation, the_eigenvalue_sum_counts_the_full_effective_potential, the_actual_density_matrix_is_hermitian, a_general_normalized_orbital_energy_is_its_actual_hamiltonian_expectation, the_total_energy_removes_hartree_and_correction_double_counting, local_chemical_potential_is_not_just_the_energy_per_particle, the_hartree_mean_is_twice_the_hartree_energy, a_potential_gauge_shift_changes_energy_by_charge, Reference.a_realized_density_has_the_normalized_particle_number, separate_functional_derivatives_give_the_actual_total_energy_variation, an_actual_constrained_minimum_gives_stationarity_only_with_differentiability, the_actual_stationary_derivative_gives_the_local_euler_integral, comparing_the_two_euler_integrals_retains_fixed_number_variations, fixed_number_stationarity_determines_a_potential_only_up_to_a_constant, the_potential_gauge_constant_is_fixed_by_the_density_mean, the_normalized_stationary_density_identifies_the_selected_gauge_shift, the_noninteracting_reference_transfers_to_the_self_consistent_local_equations, shared_ground_density_model_retains_exact_semantics, paper_setup_realizes_shared_selected_ground_density_setup, hohenberg_kohn_foundation_realizes_shared_variational_bridge, hohenberg_kohn_foundation_realizes_selected_variational_calculation, exact_ground_density_makes_shared_variational_route_applicable, exact_ground_density_inputs_realize_structural_ground_density_variational_explanation, kohn_sham_imported_foundation_realizes_source_structural_ground_density_variational_explanation, exact_ground_density_establishes_shared_variational_result, exact_ground_density_exhibits_nonvacuous_shared_variational_principle, exact_ground_density_setup_realizes_physically_sound_shared_representation, exact_ground_density_realizes_scoped_descriptive_completeness, exact_ground_density_model_inputs_establish_theory_model_grounding, exact_ground_density_establishes_theory_model_grounded_variational_result, exact_ground_density_route_transfers_every_shared_claim, exact_ground_density_realizes_shared_variational_principle, local_density_stationarity_yields_self_consistent_equations, local_self_consistency_retains_the_actual_functional_domain, the_selected_orbital_representation_has_actual_positive_electron_number, selected_orbital_energy_accounting_uses_the_actual_correction_mean, local_self_consistent_route_yields_energy_formula, exchange_only_local_potential_is_two_thirds_of_slater, slowly_varying_local_scheme_retains_second_gradient_accuracy, high_density_local_scheme_retains_reliability, local_density_approximation_retains_surface_and_large_gap_limits, nonlocal_self_consistency_retains_the_actual_correlation_domain, nonlocal_self_consistency_retains_the_actual_fock_domain, exact_exchange_route_yields_hartree_fock_like_system_with_caveat, nonlocal_self_consistency_retains_the_exchange_contraction_in_its_energy, the_exact_variation_energy_is_the_same_exact_density_functional, the_imported_exact_minimum_controls_the_actual_admitted_density_variations, exact_functional_yields_exact_one_particle_formulation, formal_exact_formulation_retains_explicit_potential_obligation, the_public_canonical_api_normalizes_the_two_occupation_states, the_partition_is_computed_from_zero_or_one_fermion, empty_and_occupied_probabilities_sum_to_one, the_computed_occupation_is_the_fermi_dirac_law, both_occupation_probabilities_are_strictly_between_zero_and_one, the_mean_number_and_energy_are_actual_gibbs_averages, the_number_variance_is_the_actual_bernoulli_variance, a_thermal_fermion_mode_has_nonzero_number_fluctuations, the_entropy_is_the_fermionic_occupation_entropy, the_entropy_retains_energy_and_partition, the_gibbs_averages_give_the_actual_grand_free_energy, the_occupation_free_energy_has_the_same_gibbs_value, a_common_energy_and_chemical_potential_shift_preserves_occupation, a_common_grand_energy_shift_preserves_the_actual_mode_entropy, zero_grand_energy_has_half_occupation, totalized_zero_temperature_substitution_gives_half_occupation, the_actual_occupation_log_odds_are_the_grand_energy, the_fermionic_free_energy_has_the_actual_occupation_derivative, the_computed_fermi_occupation_is_a_stationary_grand_free_energy, an_above_chemical_potential_mode_empties_in_the_actual_zero_temperature_limit, direct_zero_temperature_substitution_disagrees_with_the_physical_limit, a_positive_temperature_fermion_realizes_the_thermal_gibbs_logic, the_noninteracting_mode_law_is_the_actual_product_of_gibbs_distributions, each_mode_marginal_is_its_actual_binary_gibbs_law, the_joint_law_has_the_computed_fermi_occupation_probability, each_spectral_mode_has_the_computed_fermi_dirac_occupation, the_weighted_orbital_density_is_nonnegative, integrating_each_normalized_weighted_orbital_gives_its_mean_occupation, spectral_summability_controls_the_actual_weighted_density_integrals, the_integrated_thermal_density_is_the_mean_number_not_a_state_count, a_finite_available_spectrum_cannot_have_every_mode_filled, finite_mode_count_calibration_requires_more_modes_than_mean_particles, the_thermal_potential_gauge_shifts_the_energy_and_chemical_potential_together, the_actual_schrodinger_equations_survive_a_common_thermal_gauge_shift, the_common_thermal_gauge_shift_preserves_kinetic_energy_and_entropy, a_common_thermal_gauge_shift_preserves_the_complete_reference_domain, a_thermal_reference_realizes_a_positive_normalized_mean_particle_number, the_grand_potential_variation_retains_the_chemical_number_term, a_grand_canonical_minimum_requires_its_actual_differentiable_domain, grand_stationarity_compares_the_potentials_relative_to_their_chemical_potentials, unrestricted_thermal_variations_fix_the_gauge_shift_to_the_chemical_potential_difference, a_fixed_mean_number_makes_the_actual_number_derivative_zero, the_density_path_term_is_chemical_work_until_number_conservation_is_used, differentiating_the_actual_free_energy_retains_the_chemical_work_correction, the_fixed_density_partial_derivative_defines_the_actual_thermal_entropy, fixed_number_thermodynamics_identifies_entropy_with_the_total_free_energy_slope, the_printed_entropy_plus_sign_agrees_with_free_energy_thermodynamics_only_when_its_correction_vanishes, differentiating_the_uniform_free_energy_difference_fixes_its_temperature_sign, the_actual_helmholtz_energy_is_grand_potential_plus_chemical_mean_number, a_regular_density_of_states_is_the_actual_local_state_count_derivative, the_displayed_gamma_is_the_sum_of_two_distinct_spectral_contributions, the_entropy_identity_retains_both_actual_component_remainders, differentiating_the_caloric_argument_requires_the_actual_remainder_derivatives, the_actual_specific_heat_retains_the_slope_corrections, the_low_temperature_caloric_route_produces_an_actual_controlled_heat_formula, vanishing_component_error_budgets_give_the_leading_heat_coefficient, the_uniform_gas_entropy_input_gives_the_opposite_sign_to_printed_equation_fifteen, the_two_printed_sign_changes_cancel_in_the_displayed_leading_coefficient, the_exact_thermal_decomposition_retains_the_internal_free_energy_functional, the_local_thermal_functional_is_the_actual_uniform_gas_free_energy_integral, the_thermal_reference_shift_is_fixed_by_actual_grand_potential_variations, the_selected_thermal_equations_have_actual_complex_orbitals, the_selected_density_has_actual_fermi_occupations_and_the_calibrated_mean_number, finite_temperature_variational_route_yields_thermal_equations, stationarity_and_admissible_temperature_variations_supply_the_actual_caloric_euler_contraction, the_temperature_path_inputs_supply_the_differentiable_caloric_argument, low_temperature_route_yields_specific_heat_formula, weak_field_expansion_yields_spin_response_and_local_kernel, corrected_exchange_correlation_equation_retains_a2_two_kernel_formula, rapid_oscillation_route_yields_formal_correction_with_kernel_caveat, the_real_wave_has_its_actual_density, the_real_wave_has_its_actual_norm, both_site_states_are_normalized, the_two_test_hamiltonians_are_hermitian, diagonal_energies_are_computed_from_the_wave, an_approximate_ground_state_need_not_be_an_exact_ground_state, a_global_complex_phase_preserves_density_but_not_the_literal_square, two_normalized_occupied_slots_do_not_supply_orthogonality, a_normalized_reconstructed_density_does_not_supply_an_eigenvector, the_graph_kinetic_energy_is_a_positive_square, both_phases_have_the_same_normalized_density, the_same_density_does_not_fix_the_kinetic_energy_of_arbitrary_states, a_stationary_normalized_state_need_not_minimize_the_energy, the_finite_hartree_potential_is_the_actual_energy_derivative, the_repulsive_hartree_kinetic_energy_is_nonnegative, the_hartree_hamiltonian_is_hermitian, the_trial_charge_profiles_are_computed, both_trial_waves_are_normalized, the_selected_hartree_hamiltonians_are_computed, the_two_updates_and_the_fixed_point_solve_the_actual_eigenproblems, the_three_hamiltonian_lower_bounds_are_actual_squares, a_normalized_eigenvector_has_its_actual_eigenvalue_energy, each_update_really_selects_a_ground_state, a_ground_eigenproblem_update_need_not_be_self_consistent, the_total_hartree_energy_has_its_actual_minimum_identity, the_trial_total_energies_and_hartree_means_are_computed, the_balanced_fixed_point_minimizes_the_actual_total_energy, every_step_of_the_cycle_solves_the_actual_ground_eigenproblem, the_iterated_density_stays_a_fixed_distance_from_the_fixed_point, correct_ground_state_updates_do_not_establish_self_consistent_convergence, the_exact_ground_update_cycle_has_no_density_limit, the_nonselfconsistent_eigenvalue_cannot_be_used_in_the_total_energy_formula, the_selfconsistent_total_energy_removes_the_actual_hartree_double_count, the_hartree_quadratic_form_separates_number_and_imbalance, a_frozen_density_eigenpair_has_an_exact_total_energy_defect, the_hartree_energy_correction_is_exact_iff_the_input_density_is_reproduced, fixed_number_energy_defect_is_five_times_the_site_density_residual_squared, a_density_residual_bound_controls_the_total_energy_defect, zero_energy_changes_do_not_certify_self_consistency, the_local_energy_per_particle_does_not_equal_its_potential, the_diagonal_density_functionals_are_actual_state_energies, the_two_fixed_number_functional_derivatives_are_computed, one_energy_value_does_not_identify_a_functional_derivative, a_constant_potential_shift_has_its_actual_charge_weight, fixed_number_variations_do_not_fix_the_absolute_potential, local_functional_minimizer_need_not_minimize_exact_functional, limiting_accuracy_regimes_are_not_joint_requirements, accuracy_in_two_limits_does_not_imply_global_accuracy, density_reconstruction_does_not_supply_orbital_equation, one_energy_readout_does_not_supply_a_functional_derivative, named_rapid_kernel_correction_does_not_supply_equation_a2_two, formal_kernel_correction_without_small_density_change_does_not_fix_energy, both_occupation_ensembles_have_computed_normalized_gibbs_weights, the_two_grand_canonical_modes_are_actual_half_occupied_fermions, every_grand_configuration_has_probability_one_quarter, every_fixed_one_particle_configuration_has_probability_one_half, the_grand_number_is_a_mean_one_with_nonzero_actual_variance, the_canonical_number_is_sharply_one_with_zero_actual_variance, the_two_different_ensembles_have_the_same_actual_one_particle_density, the_actual_ensemble_entropies_are_different, equal_density_and_mean_number_do_not_identify_canonical_and_grand_canonical_entropy, calibrating_one_mean_particle_does_not_remove_particle_number_fluctuations, two_available_fermionic_modes_do_not_supply_two_thermal_particles, an_actual_thermal_mode_separates_zero_substitution_from_the_one_sided_limit, the_fixed_chemical_potential_occupation_is_computed_from_the_binary_partition, the_fixed_chemical_potential_grand_potential_is_the_actual_log_partition, the_growing_mean_occupation_has_a_strictly_positive_temperature_derivative, the_grand_potential_derivative_is_minus_the_actual_gibbs_entropy, the_actual_helmholtz_slope_retains_chemical_work_for_a_changing_mean_number, actual_grand_canonical_stationarity_does_not_identify_entropy_with_the_helmholtz_path_slope, the_control_density_is_an_actual_normalized_positive_continuum_density, the_uniform_exchange_correlation_free_energy_is_the_actual_difference, the_quadratic_exchange_correlation_temperature_derivative_is_negative, the_quadratic_local_internal_free_energy_is_computed_from_the_density_integral, the_quadratic_entropy_is_the_actual_partial_free_energy_derivative, the_actual_quadratic_entropy_correction_is_minus_two_temperature, the_quadratic_heat_capacity_is_positive_and_linear, positive_entropy_and_heat_do_not_validate_the_printed_entropy_plus_sign, the_actual_uniform_entropy_difference_has_the_opposite_free_energy_derivative_sign, the_entropy_remainder_ratio_has_a_genuine_zero_limit, the_oscillating_thermodynamic_entropy_is_continuous, the_oscillating_entropy_is_an_actual_free_energy_derivative, the_actual_oscillating_entropy_derivative_keeps_the_cosine_term, the_oscillating_entropy_and_heat_are_positive_in_a_nonempty_low_temperature_interval, the_actual_entropy_has_leading_coefficient_three, the_resolving_temperature_sequence_is_strictly_positive, the_resolving_temperature_sequence_approaches_zero_from_above, the_actual_heat_coefficient_is_two_along_the_resolving_sequence, the_entropy_asymptotic_does_not_supply_the_same_specific_heat_asymptotic
Coverage theorems (10)
every_source_claim_has_semantics, exact_variational_foundation_route_is_semantically_realized, local_self_consistent_equations_route_is_semantically_realized, accuracy_and_scope_route_is_semantically_realized, nonlocal_exchange_alternative_route_is_semantically_realized, finite_temperature_extension_route_is_semantically_realized, spin_response_extension_route_is_semantically_realized, rapid_oscillation_correction_route_is_semantically_realized, exact_one_particle_formulation_route_is_semantically_realized, route_semantic_realization_is_exhaustive
Source-map audit theorems (14)
alternative_and_formal_exact_routes_do_not_absorb_local_approximation, argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, local_result_steps_apply_selected_inputs_and_contracts, accuracy_and_nonlocal_steps_apply_selected_inputs_and_contracts, independent_extension_steps_apply_selected_inputs_and_contracts, formal_exact_steps_apply_selected_inputs_and_contracts, local_self_consistent_solution_retains_imported_foundation_and_approximation, limiting_accuracy_branches_do_not_inherit_each_other, rapid_correction_retains_unresolved_kernel_obligation, exact_formulation_does_not_inherit_local_density_approximation, explicit_potential_obligation_depends_on_exact_formulation_and_missing_formula
Semantic atoms (69)
exactGroundStateSetup, hohenbergKohnVariationalFoundation, sharedGroundDensityVariationalPrinciple, exactUniversalDecomposition, localExchangeCorrelationFormula, localStationarity, occupiedCount, localStationarityCalculation, localEffectivePotentialEquation, localOneElectronEquations, densityFromOccupiedOrbitals, selectedLocalOrbitalAdmissibility, localReferenceGauge, localSelfConsistentSolution, localElectronNormalization, localEnergyCalculation, localTotalEnergyFormula, slaterExchangeCalculation, slaterExchangeComparison, slowlyVaryingDensity, highDensity, slowVariationAccuracyCalculation, highDensityAccuracyCalculation, densityCorrectThroughSecondGradientOrder, highDensityApproximationReliable, finiteRapidSurfaceSetup, surfaceLimitationAssessment, surfaceApproximationFailure, largeGapSetup, largeGapLimitationAssessment, largeGapApproximationFailure, nonlocalExchangeDecomposition, nonlocalOccupiedCount, nonlocalStationarity, nonlocalStationarityCalculation, nonlocalSelfConsistentSolution, nonlocalEnergyCalculation, nonlocalTotalEnergyFormula, nonlocalSurfaceAssessment, nonlocalExchangeSurfaceImproved, localCorrelationSurfaceCaveat, finiteTemperatureFoundation, exactThermalDecomposition, localThermalExchangeCorrelationFormula, thermalStationarity, thermalStationarityCalculation, thermalSelfConsistentSolution, lowTemperatureRegime, lowTemperatureSpecificHeatCalculation, lowTemperatureSpecificHeatFormula, weakFieldSpinSetup, spinResponseCalculation, linearizedSpinResponseEquation, susceptibilityFromInverseKernel, localSpinKernelApproximation, infiniteRapidOscillationSetup, smallDensityModification, beyondRPAKernelUnavailable, rapidOscillationCorrectionCalculation, firstOrderEnergyCorrectionCalculation, correctedExchangeCorrelationEquation, correctedPotentialEquation, firstOrderEnergyCorrectionEquation, exactExchangeCorrelationFunctionalDerivative, exactOneParticleCalculation, exactOneParticleFormulation, exactTotalEnergyFormula, explicitExactPotentialNotKnown, exactFormulationRetainsExplicitPotentialObligation
Claim identifiers (69)
exactSetup, hkFoundation, sharedVariational, universalDecomposition, localXCFormula, localStationary, occupiedCount, localCalculation, localEffectivePotential, localOrbitalEquations, localDensityReconstruction, localOrbitalAdmissibility, localGauge, localSolution, localNormalization, localEnergyCalculation, localEnergyFormula, slaterCalculation, slaterComparison, slowlyVarying, highDensity, slowAccuracyCalculation, highAccuracyCalculation, secondGradientAccuracy, highDensityReliability, surfaceSetup, surfaceAssessment, surfaceFailure, largeGap, largeGapAssessment, largeGapFailure, nonlocalDecomposition, nonlocalOccupiedCount, nonlocalStationary, nonlocalCalculation, nonlocalSolution, nonlocalEnergyCalculation, nonlocalEnergyFormula, nonlocalAssessment, nonlocalSurfaceImproved, correlationSurfaceCaveat, thermalFoundation, thermalDecomposition, thermalLocalFormula, thermalStationary, thermalCalculation, thermalSolution, lowTemperature, specificHeatCalculation, specificHeatFormula, spinSetup, spinCalculation, spinResponseEquation, susceptibility, localSpinKernel, rapidSetup, smallModification, kernelUnavailable, rapidCalculation, correctionEnergyCalculation, correctedXC, correctedPotential, firstOrderEnergy, exactFunctional, exactCalculation, exactFormulation, exactEnergyFormula, explicitPotentialUnknown, explicitPotentialObligation
Step identifiers (69)
stateExactSetup, stateHkFoundation, realizeSharedVariational, stateUniversalDecomposition, stateLocalXCFormula, stateLocalStationary, stateOccupiedCount, stateLocalCalculation, deriveLocalEffectivePotential, deriveLocalOrbitalEquations, deriveLocalDensityReconstruction, deriveLocalOrbitalAdmissibility, deriveLocalGauge, deriveLocalSolution, deriveLocalNormalization, stateLocalEnergyCalculation, deriveLocalEnergyFormula, stateSlaterCalculation, deriveSlaterComparison, stateSlowlyVarying, stateHighDensity, stateSlowAccuracyCalculation, stateHighAccuracyCalculation, deriveSecondGradientAccuracy, deriveHighDensityReliability, stateSurfaceSetup, stateSurfaceAssessment, deriveSurfaceFailure, stateLargeGap, stateLargeGapAssessment, deriveLargeGapFailure, stateNonlocalDecomposition, stateNonlocalOccupiedCount, stateNonlocalStationary, stateNonlocalCalculation, deriveNonlocalSolution, stateNonlocalEnergyCalculation, deriveNonlocalEnergyFormula, stateNonlocalAssessment, deriveNonlocalSurfaceImproved, deriveCorrelationSurfaceCaveat, stateThermalFoundation, stateThermalDecomposition, stateThermalLocalFormula, stateThermalStationary, stateThermalCalculation, deriveThermalSolution, stateLowTemperature, stateSpecificHeatCalculation, deriveSpecificHeatFormula, stateSpinSetup, stateSpinCalculation, deriveSpinResponseEquation, deriveSusceptibility, deriveLocalSpinKernel, stateRapidSetup, stateSmallModification, stateKernelUnavailable, stateRapidCalculation, stateCorrectionEnergyCalculation, deriveCorrectedXC, deriveCorrectedPotential, deriveFirstOrderEnergy, stateExactFunctional, stateExactCalculation, deriveExactFormulation, deriveExactEnergyFormula, stateExplicitPotentialUnknown, deriveExplicitPotentialObligation
Route identifiers (8)
exactVariationalFoundation, localSelfConsistentEquations, accuracyAndScope, nonlocalExchangeAlternative, finiteTemperatureExtension, spinResponseExtension, rapidOscillationCorrection, exactOneParticleFormulation
Route kinds (8)
importedDensityVariationalFoundation, localDensityApproximation, controlledLimitsAndFailures, exactExchangeLocalCorrelation, thermalDensityFunctional, weakFieldSpinResponse, shortWavelengthCorrection, formalExactReformulation
Checked source-route details
This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.
exactVariationalFoundation
Logical kind: importedDensityVariationalFoundation.
Required predecessor routes: none.
Ordered inference steps: stateExactSetup, stateHkFoundation, stateUniversalDecomposition, realizeSharedVariational.
Exported conclusions: exactSetup, hkFoundation, universalDecomposition, sharedVariational.
localSelfConsistentEquations
Logical kind: localDensityApproximation.
Required predecessor routes: exactVariationalFoundation.
Ordered inference steps: stateLocalXCFormula, stateLocalStationary, stateOccupiedCount, stateLocalCalculation, deriveLocalEffectivePotential, deriveLocalOrbitalEquations, deriveLocalDensityReconstruction, deriveLocalOrbitalAdmissibility, deriveLocalGauge, deriveLocalSolution, deriveLocalNormalization, stateLocalEnergyCalculation, deriveLocalEnergyFormula, stateSlaterCalculation, deriveSlaterComparison.
Exported conclusions: occupiedCount, localSolution, localNormalization, localEnergyFormula, slaterComparison.
accuracyAndScope
Logical kind: controlledLimitsAndFailures.
Required predecessor routes: localSelfConsistentEquations.
Ordered inference steps: stateSlowlyVarying, stateHighDensity, stateSlowAccuracyCalculation, stateHighAccuracyCalculation, deriveSecondGradientAccuracy, deriveHighDensityReliability, stateSurfaceSetup, stateSurfaceAssessment, deriveSurfaceFailure, stateLargeGap, stateLargeGapAssessment, deriveLargeGapFailure.
Exported conclusions: secondGradientAccuracy, highDensityReliability, surfaceFailure, largeGapFailure.
nonlocalExchangeAlternative
Logical kind: exactExchangeLocalCorrelation.
Required predecessor routes: exactVariationalFoundation.
Ordered inference steps: stateNonlocalOccupiedCount, stateNonlocalDecomposition, stateNonlocalStationary, stateNonlocalCalculation, deriveNonlocalSolution, stateNonlocalEnergyCalculation, deriveNonlocalEnergyFormula, stateNonlocalAssessment, deriveNonlocalSurfaceImproved, deriveCorrelationSurfaceCaveat.
Exported conclusions: nonlocalSolution, nonlocalEnergyFormula, nonlocalSurfaceImproved, correlationSurfaceCaveat.
finiteTemperatureExtension
Logical kind: thermalDensityFunctional.
Required predecessor routes: none.
Ordered inference steps: stateThermalFoundation, stateThermalDecomposition, stateThermalLocalFormula, stateThermalStationary, stateThermalCalculation, deriveThermalSolution, stateLowTemperature, stateSpecificHeatCalculation, deriveSpecificHeatFormula.
Exported conclusions: thermalSolution, specificHeatFormula.
spinResponseExtension
Logical kind: weakFieldSpinResponse.
Required predecessor routes: none.
Ordered inference steps: stateSpinSetup, stateSpinCalculation, deriveSpinResponseEquation, deriveSusceptibility, deriveLocalSpinKernel.
Exported conclusions: spinResponseEquation, susceptibility, localSpinKernel.
rapidOscillationCorrection
Logical kind: shortWavelengthCorrection.
Required predecessor routes: none.
Ordered inference steps: stateRapidSetup, stateSmallModification, stateKernelUnavailable, stateRapidCalculation, stateCorrectionEnergyCalculation, deriveCorrectedXC, deriveCorrectedPotential, deriveFirstOrderEnergy.
Exported conclusions: correctedXC, correctedPotential, firstOrderEnergy, kernelUnavailable.
exactOneParticleFormulation
Logical kind: formalExactReformulation.
Required predecessor routes: exactVariationalFoundation.
Ordered inference steps: stateExactFunctional, stateExactCalculation, deriveExactFormulation, deriveExactEnergyFormula, stateExplicitPotentialUnknown, deriveExplicitPotentialObligation.
Exported conclusions: exactFormulation, exactEnergyFormula, explicitPotentialObligation.