Formal reconstruction · Density determination, variational energy, response kernels, and controlled approximation scope
Inhomogeneous Electron Gas
The nondegenerate density theorem, the representable-density variational principle, universal internal energy, equations (35)-(49) for nearly uniform response, the Friedel obstruction to finite gradient expansions, an assumed slowly varying expansion, and equation-(83)/(84) partial summation with explicit local and Fourier formulas
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.
- inductiveA static additive constant is not an arbitrary time-dependent gauge.
- structureSelected physical roles before any domain or classification is established.
- structureProof-free selected objects and source-sensitive physical relation families. The full description can be a state/potential pair for the static theorem or a time-dependent potential for the fixed-initial-state theorem.
- structureThe actual density/potential classification at its exact physical indices.
- structureA selected density-potential route paired with independent source provenance.
- 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
- structureThe exact state-equality contracts below apply to physical-ray labels or consistently phase-fixed representatives. Instantiating `GroundState` by all normalized wavefunctions does not supply those contracts: global phase leaves density and energy unchanged. `HohenbergKohn1964.GroundStateQuotient` supplies a conditional quotient construction for this entire framework. Concrete continuum domains and phase-invariance inputs remain separate obligations.
- structure
- structure
- structure
- structure
- structure
- inductive
- inductive
- structurePaper-local readouts for the divergence-reduced fourth-order gradient expansion displayed in equation (63). The derivative values remain imported mathematics, but the source's four distinct scalar invariants are retained.
- structureOne selected partial-energy-density readout along the scaled family in equations (59)-(61). Coefficients are independent of the scale.
- structure
- inductiveThe original theorem-I double-variational derivation is not TDDFT.
- inductiveTyped token for Hohenberg and Kohn's original density-minimum derivation.
- structureThe physical ground-state system represented by one variational model.
- structurePaper-local coefficients and remainders for equations (38)-(40) and (44)-(46). The same c2 and c4 readouts are used on both sides of equation (35), so the kernel expansion cannot drift away from the polarizability expansion by renaming a coefficient.
- structurePaper-local readouts for the partial summation displayed in equation (83). The data store values only: the source calculation must separately establish the displayed equality and its integration to the residual functional.
- structure
- structure
- structure
- structure
- structure
- 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
- definition
- definitionAn inhabited physical setup plus the actual source-qualified classification.
- definitionThe source calculation and full iff-classification are independent facts.
- definitionExact validity, fixed conditions, physical branch, and selected density.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionActual reduced-description semantics on the selected physical domain.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- 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.
- definitionEvery route named in the supplied identifier list is semantically certified.
- 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
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPositive box volume and local density do not exclude a zero Fourier mode.
- definitionPositive density and volume do not fix the partial-summation energy.
- definitionPositive local density and a vanishing local gradient do not fix (63).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe two checked theorem-I outputs used by the paper's theorem-II transition: density determines the nondegenerate ground state on the declared admissible class, both directly and as the equality-qualified special case.
- definitionThe paper's B865 move "since Ψ is a functional of n" is retained as an explicit bridge. It is not silently folded into the definition of the universal functional.
- definition
- definitionEquation (83) as the paper's proposed partial-summation formula for every density. Keeping this proposition separate lets the route derive the formula before specializing it to the two limits used for the exactness comparison.
- definitionEquation (83), together with equation (64)'s passage from a local residual energy density to G[n]. The local equality exposes the symmetric half-displacements; the second conjunct prevents the global partialSummationValue from floating free of that local formula.
- definitionThe perturbation n~(r) = n(r) - n0 used in equation (48). The uniform reference value is kept separate from the reference density object so the formula cannot replace n0 by an unrelated scalar.
- definitionEquation (48): G[n] = G[n0] + 2 pi [-c2 integral n~^2 + (c2^2 - c4) integral |grad n~|^2 + ...]. The first conjunct retains that the selected reference density really has the uniform value n0 at every position.
- definitionThe |grad n~(r)|^2 integrand displayed in equation (48).
- definitionEquation (45): the exact kernel derivative diverges to positive infinity at q = 2 k_F.
- definitionEquation (44), obtained from equation (35) and equation (38): K(q) = 2 pi [-c2 + (c2^2 - c4) q^2 + o(q^2)] as q -> 0.
- definitionEquation (40): alpha(q) is asymptotic to a nonzero constant divided by q^4 at large momentum.
- definitionEquation (47), read distributionally on every test function: K(r) = 2 pi [-c2 + (c2^2 - c4) nabla^2 + ...] delta(r). The radial kernel is the same exactPositionKernel later used by equation (49); the embedding into distributions and the distributional Laplacian are explicit imported mathematics.
- definitionEquation (46): K(q) is asymptotic to a nonzero constant times q^2 at large momentum.
- definitionEquation (63), together with equation (64)'s integration of the divergence-reduced local energy density. The local formula retains the four independent second- and fourth-order scalar structures before the global slowlyVaryingGradientExpansionValue can be used.
- definitionEquation (38): alpha(q) = 1 + c2 q^2 + c4 q^4 + o(q^4) as q -> 0.
- definitionEquation (39): the derivative of alpha(q) diverges to negative infinity at q = 2 k_F. The punctured neighborhood retains the two-sided source limit.
- definitionEquation (37), obtained by rewriting equation (35) through equation (36): K(q) = (2 pi / q^2) (1 / (epsilon(q) - 1)). Besides the displayed equation-(37) denominators, the common-domain form retains the equation-(35)/(36) denominator obligations needed for the source's "equivalently" step.
- definitionEquation (36): epsilon(q) = 1 / (1 - alpha(q)).
- definitionThe two displayed formulas in the proposed partial summation: equation (84) fixes the kernel used inside equation (83), while equation (83) fixes the local and integrated residual-energy readouts for every density.
- definitionThe finite gradient construction supplies a polynomial in q^2; its actual analyticity is derived rather than supplied as a label.
- definition
- definitionThe positive local statement in footnote 12: densities in the declared first-order perturbative neighborhood of a normalized uniform density can be realized by an external potential to that same perturbative order.
- definition
- definitionExact relation from polarizability singularity to the Friedel tail.
- definition
- definitionThe stronger generic claim that the authors say they believe, while excluding pathological densities. It is exact ground-state representability, not merely first-order external realizability.
- definitionAuthor-qualified expectation that the nonconvergent series is asymptotic.
- definitionMatching to uniform-gas response functions fixes the gradient coefficients.
- definitionThe exact conclusion of the paper's density variational principle: the correct density attains the physical ground-state energy, and no density in the paper's representable fixed-particle-number domain has lower energy.
- definition
- definition
- definition
- definitionThe original theorem-I source retains the strict double-variational route.
- definitionRaw source premises interpreting the 1964 density-minimum token. The selected nondegenerate ground-state setup, ground-energy identity, universal-functional construction, and wavefunction variational principle remain separate contracts; no established shared minimum is stored here.
- definition
- definitionThe paper's equation-(35) comparison transfers equations (38)-(40) to the kernel behavior displayed in equations (44)-(46). The Fourier and asymptotic analysis is retained as an explicit paper-local calculation contract.
- definitionEquations (44)-(46) retain the small-momentum kernel series, the inherited 2 k_F singularity, and the large-momentum growth as one source block.
- definitionExact output of the almost-constant-density expansion, equations (24)-(35).
- definition
- definition
- definitionExact equality of the chosen state labels, not a claim that all normalized wavefunctions in a one-dimensional eigenspace are equal. The finite consumer's global-phase orbit and sign-change control test this representation boundary.
- definitionPaper calculation behind the two stated atomic predictions.
- definitionDeferred calculation contract for the partial summation in equation (83).
- definitionEquations (38)-(40) retain the small-momentum series, the 2 k_F derivative singularity, and the large-momentum decay as one source block.
- definitionThe power-series kernel block produces equations (47)-(48): a distributional position-space kernel and the corresponding nearly uniform gradient functional. The Fourier/distributional manipulation and integration by parts remain an explicit paper-local calculation contract.
- definitionThe stronger representability statement left unresolved in footnote 12: positivity and normalization at an integer particle number would suffice to realize every candidate density as a ground-state density.
- definition
- definition
- definitionEquations (59)-(64) identify the same shape, scaled observation point, physical partial-energy density, and fourth-order truncation at every scale. This identity carries no small-remainder or convergence assertion.
- definitionThe paper-local premises needed to ground the shared model before using the energy-attainment or minimum conclusion of the 1964 variational theorem.
- definitionPaper-local realization of every shared variational claim.
- definitionThe paper assumes, rather than generally proves, the slowly varying gradient expansion and reduces it using rotational invariance and divergence freedom.
- definition
- definitionThe strict ground-state variational principle used in equations (6)-(7). Nondegeneracy and a distinct physical-state label make the ordinary variational bound strict within the fixed-particle-number sector. Literal inequality of unrestricted wavefunction representatives is insufficient because of phase.
- definition
- definitionThe universal functional is the expectation of the fixed kinetic operator plus the mutual Coulomb-repulsion operator. Neither term takes the external potential as an argument; only the ground state selected by that potential changes.
- definitionThe selected fixed-particle-number form used by theorem II. The paper later notes that particle number is itself a functional of the density; this route does not silently promote one selected sector to every sector.
- definition
- definitionOrdinary wavefunction variational principle at fixed particle number.
- definition
- definition
- definition
- definitionTo capture the Friedel structure, an approximation must retain both the nonanalytic momentum-space feature at `2 k_F` and an oscillatory inverse-cube position-space tail.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe dielectric constant introduced in equation (36). The paper defines this readout from the dimensionless electronic polarizability rather than taking it as an independent response datum.
- definition
- definition
- definition
- definition
- definitionThe Part II response expansion gives the value of the residual universal functional `G[n]` for a density in the nearly uniform regime.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPhysical Review B869-B870, equation (81): the wave number carried by the relative density gradient is parametrically smaller than the local Fermi wave number. The qualitative << relation remains paper-local because the paper states a scale hierarchy rather than a numerical cutoff.
- definition
- definitionThe position-space profile displayed in equation (49). Its Fourier derivation remains an explicit input; its asymptotic meaning is the scaled additive condition in ResponseKernel.FriedelTailAt.
- definition
- definition
- definition
- definitionPointwise fixed-order asymptotics along the scale family. Neither the position nor the truncation order is covered by a uniform error bound.
- definitionThe Part III gradient construction gives the value of `G[n]` in the slowly varying regime. Its existence remains an explicit paper assumption.
- definition
- definitionPointwise order convergence at the selected finite scale, not equality of the series sum with the physical energy-density readout.
- definition
- definitionThe existing multi-paper truncation interface applied to actual local gradient errors. Empirical assessment is caller-supplied and is not inferred from the theoretical source calculation or its asymptotic expectation.
- definitionThe two necessary gradient-expansion conditions in equations (81)-(82). Neither one is folded into the phrase "slowly varying": the paper explicitly requires both relative-gradient and gradient-curvature scale separation.
- definition
- definition
- definition
- definitionCompatibility API with actual real analyticity, not a freely assigned predicate.
- definitionEquation (35): K(q) = (2 pi / q^2) (1 / alpha(q) - 1). The two denominator obligations make the displayed source formula meaningful without treating Lean's totalized division at zero as physical content.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (83) is exact in the nearly uniform limit when its value equals the same residual universal functional `G[n]`.
- definitionEquation (83) is exact in the slowly varying limit by the same value-level criterion. The separate predicates preserve the two distinct regimes.
- definition
- definition
- definition
- definition
- definitionPositive momenta approaching zero, as in the q -> 0 source limits.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA punctured momentum neighborhood for the q -> 2 k_F singularities.
- definition
- definition
- definition
- definition
- definitionPhysical Review B869-B870, equation (82): the wave number for variation of the density gradient is separately parametrically smaller than the local Fermi wave number.
- definitionThe exact shared model selected by the 1964 variational route.
- definition
- definition
- definition
- definitionThe external-potential theorem needs both a physical state and its external potential. Keeping them paired prevents the static source from being mistaken for the fixed-initial-state time-dependent map.
- definition
- definitionThe exact ground-state theorem is the equality special case of determination up to equivalence. The paper's separate potential conclusion remains uniqueness only modulo an additive constant.
- definitionThe 1964 framework is the theory object, while the represented world records the nondegenerate ground state, external potential, and fixed particle number.
- definition
- definitionOnly the physical data used in the exact density-determination argument. This projection does not invent values for the omitted approximation fields.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe paper's position and displacement variables in equation (83). Keeping the three coordinates explicit prevents the two half-displaced density values from collapsing into an opaque scalar approximation label.
- definitionThe source's delta-function formula is distributional. Test functions and distributions stay paper-local here; the analytic facts about them are imported rather than silently treating delta(r) as an ordinary function.
- definitionOne reciprocal-momentum summand in equation (84): (2 pi / q^2) (1 / epsilon_n(q)) exp(-i q . r').
- definitionEquation (84), including its finite-box reciprocal-momentum sum: K_n(r') = (1 / Omega) sum_q (2 pi / q^2) (1 / epsilon_n(q)) exp(-i q . r'). The positive-volume and nonzero-denominator conditions are explicit because the source formula is not meaningful at a zero mode or dielectric zero.
- definitionThe literal local-energy-density content of equation (83). The final two terms retain the paper's qualification that divergence terms or terms higher in the superscript nu may still be present.
- definitionThe symmetric-density-difference integrand in equation (83): K_{n(r)}(r') [n(r+r'/2)-n(r)] [n(r-r'/2)-n(r)].
- definitionThe rotational scalar grad n . grad n used in equation (63).
- definitionThe divergence-reduced local energy density in equation (63): g0(n) + g2^(2)(n) (grad n . grad n) + g4^(2)(n) (laplacian n)^2 + g4^(3)(n) (laplacian n) (grad n . grad n) + g4^(4)(n) (grad n . grad n)^2 + O(grad^6).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionFixed order first, then large scale. No uniformity in order is assumed.
- definition
- definitionConvergence in truncation order at one fixed scale, to some sum. It does not assert that the sum equals the selected physical readout.
- definition
- definition
- definitionA diagnostic expansion, not the electron-gas coefficients. Its bounded small-scale extension has no bearing on its large-scale asymptotics.
- 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 single unit-modulus scalar, shared by every configuration.
- definitionExactly the state-dependent readouts needed to descend the whole model. The density-only and potential-only fields need no additional invariance law.
- definition
- definition
- definition
- definition
- definitionRestriction to the supplied domain, for example normalized fixed-number wavefunctions. No preservation or physical adequacy of that domain is inferred.
- 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
- definitionLocal singular part in a deviation coordinate from the critical momentum, not a global microscopic electron-gas polarizability.
- definition
- definition
- definition
- definitionAdditive inverse-cube accuracy, without dividing by an oscillating profile.
- definitionThe leading oscillatory profile in equation (49).
- definitionDelta(r) represented by evaluation of a test function at the origin.
- definitionEuclidean scalar product q . r' used in equation (84).
- definitionThe squared reciprocal momentum q^2 in equation (84).
- definitionThe origin supporting the delta distribution in equation (47).
- definition
- definition
- definition
- definition
- definitionThe position r - r' / 2 appearing in equation (83).
- definitionThe position r + r' / 2 appearing in equation (83).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA bridge principle derives a macro behavior from any realizing microdescription that supports it.
- 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
- definitionA reduced description determines the full description only on a nonempty admissible domain. Injectivity alone would hold vacuously if the declared physical sector contained no full descriptions.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA reduction classifies full descriptions up to equivalence when the domain is inhabited and equality of reductions is equivalent to the declared physical equivalence. The equivalence laws then follow; they are not an extra premise.
- definition
- 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
- 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
- instance
Source mappings and interpretation choices
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- 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
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- 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
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- 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
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- 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
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statementB865's restricted variational domain must survive the change of state representation. This check neither broadens it nor assumes representability.
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- definition
- structure
- definition
- instance
- checked statementRaw paper inputs construct every declared Hohenberg-Kohn route.
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- recursor
- definition
- checked statementFootnote 12 is represented as a checked scope obstruction: positivity and integer normalization alone do not entail ground-state representability.
- definition
- definition
- checked statement**Alias** of `PhysicsLogic.Papers.HohenbergKohn1964.SemanticContext.all_routes_are_semantically_realizable`. --- Raw paper inputs construct every declared Hohenberg-Kohn route.
- definition
- definition
- checked statement
- checked statementThe source atom for equation (9) has the paper's physical content: on a nondegenerate ground-state density it denotes the fixed kinetic energy plus mutual Coulomb repulsion, not an opaque or potential-dependent internal energy label.
- 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
- definition
- definition
- 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
- 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
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- 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
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- 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 statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementWithout the nondegeneracy restriction, two distinct ground-state labels can occupy the same potential sector and have the same density. Density equality alone therefore does not supply state uniqueness.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (81) alone does not supply equation (82). This is a logical countermodel for collapsing the two necessary scale conditions, not a claim that the paper exhibits a physical density with this behavior.
- checked statementThe local first-order realization statement does not logically establish the authors' stronger generic nonpathological representability expectation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAn energy functional can have a selected global minimizer while its minimum value fails to equal an independently specified physical ground energy. Thus the minimum inequality alone cannot replace equation (10)'s attainment of the value `E`.
- checked statement
- checked statement
- checked statement
- checked statementA named slowly varying gradient expansion can hold while equation (63)'s fourth-order local formula fails. The scalar invariants and remainder must therefore remain explicit propositions rather than prose attached to a name.
- checked statementA named local-density kernel can hold while equation (84)'s positive-volume Fourier formula fails. The reciprocal-momentum construction must therefore remain an explicit proposition rather than a kernel label.
- checked statementA named partial-summation label can hold while the literal local equation-(83) formula fails. The symmetric half-displacement formula must therefore remain an explicit proposition, not prose attached to a name.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementPositivity and integer normalization alone do not logically establish ground-state representability. This is a scope countermodel, not an assertion that the paper exhibits a physical nonrepresentable electron density.
- checked statement
- checked statement
- checked statement
- checked statementIf the purported internal energy varies with the external potential while the density is unchanged, no single density functional can equal it in both systems. This isolates why the fixed kinetic and Coulomb operators belong to the logical scope of theorem II.
- checked statement
- checked statement
- checked statement
- checked 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 smaller argument has exactly the original energy, domain and source premises; the public paper definitions are retained for existing clients.
- checked statement
- checked statement
- checked statementThe global 1964 derivation is instantiated only at the exact selected model consumed by the shared route.
- checked statement
- checked statementAt every local density and displacement, equation (84) retains the reciprocal momentum sum, dielectric denominator, and complex plane wave.
- checked statementThe local equation-(83) readout remains tied to the global residual functional by the paper's equation-(64) integration step.
- checked statementAt every selected position, equation (83) retains the local-density kernel and the two opposite half-displacement density differences.
- checked statementAt each selected position, equation (63) retains its second-order gradient-square term, three distinct fourth-order invariants, and sixth-order remainder after divergences have been removed.
- checked statementEquation (63)'s local energy density remains tied to the global slowly varying gradient value by equation (64)'s spatial integral.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe finite-series obstruction concerns actual local kernel agreement; it does not require the separate Fourier calculation selecting a position tail.
- checked statementThe first-order statement is deliberately scoped to the perturbative neighborhood named in footnote 12.
- checked statement
- checked statement
- checked statementThe broader expectation retains both qualifications: positive normalization and exclusion of pathological densities.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementPhysical Review B865, equations (9)-(13): the source inputs execute the fixed-particle-number variational route and thereby structurally explain why the selected density attains the physical ground energy and minimizes the exact functional over the declared representable domain. The theorem uses the route directly rather than a packaged established endpoint.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementPhysical Review B865, equations (9)-(13): the correct fixed-particle-number density is itself admissible, attains the ground energy, and minimizes the selected functional over the declared density domain.
- checked statementThe selected exact ground density is a physically sound representation.
- checked statementThe exact ground-state functional is descriptively complete only on the paper's representable fixed-particle-number density domain. The selected ground density supplies the required inhabitedness witness; no claim about all positive normalized densities is introduced.
- checked statement
- checked statement
- checked statement
- checked statementThe complete Hohenberg-Kohn variational route transfers every shared claim to the 1964 theory and represented nondegenerate ground system.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquations (44)-(46) are retained only after the equation-(35) kernel formula, the equations-(38)-(40) response structure, and the paper-local asymptotic calculation are all supplied.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe nearly uniform response route retains the paper's dielectric rewrite only after equation (35) and the equation-(36) definition are both available.
- checked statement
- checked statement
- checked statement
- checked statementThe strict-variational theorem classifies actual potential/state pairs.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe partial-summation calculation supplies equation (84)'s local-density Fourier kernel before the two-limit comparison is used.
- checked statementThe partial-summation calculation really supplies the displayed equation-(83) formula for every density before the two-limit comparison is used.
- checked statement
- checked statement
- checked statementEquations (47)-(48) are retained only after the equations-(44)-(46) kernel block and the paper-local position-space gradient calculation are supplied.
- checked statementHohenberg-Kohn theorem I in the paper's nondegenerate scope.
- checked statement
- checked statement
- checked statementThe named paper model retains every shared route-used semantic component.
- checked statement
- checked statement
- checked statementThe slowly varying calculation supplies equation (63)'s displayed local fourth-order structure before the global gradient value is used.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementApply the original strict-variational argument to actual classes, then read its equality back as the declared relation on representatives.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- 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
- 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
- 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
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- 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
Every physical statement, formula-level paraphrase, dependency, and qualifier below comes only from HohenbergKohn1964.lean, SourceMap.lean, and Coverage.lean. Universally quantified laws and implication-valued calculations remain independent proposition-valued source contracts; each routed result is rebuilt from the claim values in its premise map. Variational inequalities, response calculations, Fourier asymptotics, gradient matching, and partial summation are never treated as already-applied conclusions. No Kohn–Sham construction or later density-functional result is imported.
Two exact theorems and five scope or approximation routes coexist without a synthetic master claim
Density determination, density variation, representability scope, nearly uniform response, and slowly varying response begin independently. The finite-gradient obstruction consumes the nearly uniform result. The proposed partial summation consumes both the nearly uniform and slowly varying expansions. The source map names the density minimum as the paper's main conclusion but certifies every route separately.
| Transition | Status | What Lean preserves |
|---|---|---|
| Equal density to potential uniqueness | exact reductio | Strict nondegenerate variation and the potential-difference identity are explicit inputs; no deferred calculation is hidden. |
| Potential uniqueness to state uniqueness | constant-shift transport + nondegenerate uniqueness | The additive-constant exception and nondegeneracy restriction remain visible. |
| Wavefunction variation to density minimum | exact representable-domain transfer | The correct density must attain the independently identified physical energy as well as minimize the functional. |
| Positive normalization to representability | open obligation | The paper does not prove this implication, and the minimum theorem does not depend on it. |
| Uniform-density perturbation to external realization | first-order local result | The conclusion is retained only for the declared perturbative neighborhood and only to first order. |
| Generic nonpathological density to representability | author expectation | Positive normalization and the nonpathological qualifier remain premises; the local result does not establish this broader claim. |
| Nearly uniform density to response kernel | controlled setup + deferred calculation | The small zero-mean perturbation, exact response data, and calculation are distinct inputs. |
| Response singularity to Friedel tail | imported derivative limits + checked nonanalyticity + deferred Fourier asymptotics | Both actual momentum nonanalyticity and the inverse-cube oscillatory envelope limit are retained. |
| Slow variation to gradient expansion | unproved assumption | Rotational invariance and divergence freedom reduce an expansion whose existence is not generally proved. |
| Gradient-series status | finite-scale nonconvergence + large-scale usefulness | Failure of strict convergence is paper-derived; usefulness remains an author expectation. |
| Two exact limits to actual-system accuracy | untested proposal | The partial summation's quantitative usefulness remains uncertain. |
Equal nondegenerate ground-state densities force the external potentials to differ only by a constant
State-representation boundary: the equality-based route applies to physical classes or consistently phase-fixed vectors, not all normalized wavefunctions literally. An independent three-site diagnostic proves a one-dimensional ground eigenspace with unequal unit-phase representatives of identical density and energy.
The checked quotient construction now transports the complete paper framework to actual equivalence classes. Density, kinetic and Coulomb energies, ground-state membership and nondegeneracy must be invariant. Separation, strict variation and uniqueness are supplied only up to the relation. The original HK deduction then gives exact determination on classes, while the original variational deduction retains exactly the same representable densities. Global phase is an explicit single unit-modulus scalar on a supplied domain, not an arbitrary equivalence label. Concrete continuum domains and their invariance inputs, and human semantic review, remain open.
The exact determination review starts with the ten physical fields used in this argument. The public paper proofs call that smaller core, and a checked bridge preserves the original energy, fixed-number domain and source premises. The full 51-field model remains inspectable through the bridge; its response expansions and atomic predictions are not silently replaced by defaults or removed from the paper.
Assume two nondegenerate ground states have the same particle density. If their external potentials are not related by an additive constant, they are distinct states. Strict ground-state variation can therefore be applied in both directions at fixed particle number.
while ΔV12[n] = −ΔV21[n].
Adding the inequalities would give E1 + E2 < E1 + E2, a contradiction. same density; distinct nondegenerate states only if potentials are nonconstant-relative (1)
Thus the potentials differ only by a constant. Such a shift changes energies but preserves the ground state. Nondegenerate ground-state uniqueness then identifies the selected states. This realizes the paper's restricted statement that the full nondegenerate ground state is determined by the density.
The route returns potential uniqueness up to a constant, equality of the selected nondegenerate ground states, and restricted density-to-state determination.
same_density_forces_potentials_to_differ_only_by_constant · same_density_determines_nondegenerate_ground_state · Physical Review p. B865The universal functional contains fixed kinetic and Coulomb operators, not the external potential
For a nondegenerate ground state, the universal functional evaluated at its density is the internal energy: kinetic energy plus mutual Coulomb repulsion. The operators are fixed; dependence on the external potential enters only through which ground state, and hence which density, is selected.
Ev[n] = Vv[n] + F[n]. external-potential dependence appears only in the first term (2)
The ordinary wavefunction variational principle transfers this functional to density space. The transfer is restricted to densities represented by nondegenerate ground states at the same particle number.
Ev[n0] ≤ Ev[n] for every representable density n with the fixed particle number. attainment of the physical energy and minimality are separate conclusions (3)
The correct density attains the physical ground energy and minimizes the total functional on the exact representable domain. Minimality alone is not used to identify the physical energy.
ground_density_realizes_variational_principle · ground_density_attains_ground_energy · ground_density_minimizes_energy_over_representable_densities · Physical Review p. B865The universal functional may then be decomposed into a classical Hartree term and a residual functional.
Ev[n] = Vv[n] + EHartree[n] + G[n]. equations (14)–(15) (4)
Footnote 12 separates an open global converse, a local result, and a broader expectation
An actual nondegenerate ground-state density is a physically sound representation when it is positive and normalized to the selected particle number. The converse is stronger: every positive integer-normalized candidate density would have to arise from some nondegenerate ground state in an external potential. The paper does not prove that converse, but it does make a narrower positive statement for first-order perturbations of a normalized uniform density.
but positive normalized density ⇏ established ground-state representability.
normalized uniform density + first-order perturbation → externally realizable to first order,
while generic nonpathological representability remains expected, not established. three footnote-12 statuses; all independent of the representable-domain minimum (5)
The representation adapter proves soundness for actual ground densities. Paper-local semantics separately retain first-order perturbative realizability and generic nonpathological representability, while countermodels show that neither positivity alone nor the local first-order result establishes the broad converse.
actual_ground_density_is_physically_sound_representation · FirstOrderUniformPerturbationRealizabilityAt · GenericNonpathologicalGroundStateRepresentabilityAtUniform-gas response fixes the nearly uniform kernel and exposes the Friedel tail
Write the density as a uniform background plus a small zero-mean perturbation. Exact uniform-gas response data and the deferred response calculation determine the quadratic residual-functional expansion and its momentum-space kernel. The source then defines the dielectric constant, rewrites the same exact kernel, and records the actual small-momentum, twice-Fermi-momentum, and large-momentum response limits before transferring them to the kernel.
K(q) = (2π/q2)(1/α(q) − 1),
ε(q) = 1/(1 − α(q)), K(q) = (2π/q2)(1/(ε(q) − 1)),
on the explicit common nonzero-denominator domain;
q → 0: α(q) = 1 + c2q2 + c4q4 + o(q4), q → 2kF: dα/dq → −∞, q4α(q) → const ≠ 0,
q → 0: K(q) = 2π[−c2 + (c22 − c4)q2 + o(q2)], q → 2kF: dK/dq → +∞, K(q)/q2 → const ≠ 0. equations (24)–(46); equation (37) is checked from equations (35) and (36), and equations (44)-(46) are transferred from equations (35) and (38)-(40) (6)
G[n] = G[n0] + 2π[−c2 ∫ ñ(r)2dr + (c22 − c4) ∫ |∇ñ(r)|2dr + ...]. equations (47)-(48); delta is retained as a distribution on every test function, with an explicit uniform reference density and higher-gradient remainders (7)
The source response block is not compressed to a bare nonanalyticity label. It retains the positive-small-momentum expansion, derivative divergence at twice the Fermi momentum, and q-4 large-momentum decay of α. A separate paper-local calculation transfers those properties through equation (35) to the kernel's small-momentum expansion, positive derivative divergence, and q2 growth. A second explicit calculation turns that kernel block into equation (47)'s test-function distributional formula and equation (48)'s G[n]−G[n0] gradient formula. The deferred Fourier-asymptotic calculation then produces the oscillatory inverse-cube position-space tail.
as r → ∞, with kF > 0 and A ≠ 0. scaled additive interpretation of the equation-(49) asymptotic display; not an exact profile or a ratio through cosine zeros (8a)
positive_derivative_divergence_excludes_analyticity and negative_derivative_divergence_excludes_analyticity prove failure of actual real analyticity from the two derivative limits. The response and kernel source blocks therefore supply those limits without separately assuming nonanalyticity. the_friedel_calculation_retains_its_actual_scaled_envelope derives the positive Fermi scale and the equivalent limit r3K(r) - A cos(2kFr + phase) → 0 from the source tail. The Fourier calculation selecting the tail remains explicit input.
inverse_cube_small_remainders_preserve_the_friedel_tail permits corrections whose product with r3 tends to zero. Concrete controls retain a nonzero inverse-fourth-power correction, positive-radius nodes of the leading cosine, and the distinction between a nonoscillating inverse-cube decay and a genuine Friedel tail. No uniformity across density families or numerical error budget is inferred.
The route certifies the residual-functional expansion, corrected polarizability kernel, equation-(36) dielectric definition, equation-(37) rewrite, equations (38)-(40)'s independent response-limit block, equations (44)-(46)'s transferred kernel-limit block, equations (47)-(48)'s distributional and gradient-functional formulas, inherited nonanalyticity, and inverse-cube oscillatory tail.
nearly_uniform_functional_is_fixed_by_uniform_response · nearly_uniform_kernel_obeys_equation_35 · dielectric_constant_obeys_equation_36 · equations_35_and_36_yield_equation_37 · nearly_uniform_response_obeys_equation_37 · PolarizabilityResponseAsymptoticStructureAt · kernel_response_calculation_retains_equations_44_to_46 · position_space_gradient_calculation_retains_equations_47_and_48 · polarizability_nonanalyticity_yields_friedel_oscillations · Physical Review pp. B866–B867No finite analytic gradient expansion can reproduce the full Friedel structure
A finite power-series or gradient approximation has an analytic momentum-space kernel. Capturing Friedel behavior requires both nonanalyticity at twice the Fermi momentum and the corresponding inverse-cube oscillatory tail. The analytic finite truncation therefore fails.
The finite-series input now means an actual polynomial in q2, not an assigned analyticity label. a_finite_isotropic_gradient_kernel_is_analytic proves its analyticity. finite_gradient_kernel_cannot_agree_near_two_fermi_momentum directly excludes equality with the exact singular kernel on any neighborhood of 2kF, without a capture predicate or Fourier-tail premise. This does not provide a numerical error bound. An independent eight-theorem response client uses the polynomial 2 - 3q2 + q6, a different oscillation frequency and phase, and a correction 7/r4; it checks six public API dependencies and a nonzero corrected kernel at a leading-profile node. These are independent response-level tests, not microscopic electron-gas solutions.
exact Friedel response → nonanalytic kernel at 2kF + inverse-cube oscillatory tail,
therefore finite gradient truncation cannot capture Friedel or shell oscillations. the source certificate retains both features; failure of the necessary momentum-space condition already excludes their joint reproduction (8b)
The theorem combines the nearly uniform certificate with finite-series analyticity and explicitly returns both pieces of the missed Friedel structure.
finite_gradient_expansion_cannot_capture_friedel_oscillations · friedel_capture_exposes_nonanalytic_kernel_and_inverse_cube_tail · Physical Review p. B867The slowly varying series does not strictly converge at finite scale but is expected to be asymptotically useful
The density has the scaled form n(r) = φ(r/r0) with r0 tending large, while substantial density variation is allowed. The existence of a gradient expansion is a basic unproved assumption. Rotational invariance restricts scalar terms, and energy densities differing by a divergence are identified. After that reduction, equation (63) retains one second-order gradient-square term, three separate fourth-order invariants, and a sixth-order remainder before integration to the global expansion value.
GradientSeries now contains actual coefficients and a scale-dependent readout. Its partial sum is SN(r0,x) = Σj=0…N aj(x)/r0j. Fixed-scale convergence asks whether these sums have a limit as N grows; it does not identify that limit with the physical energy density. Expected asymptotics instead require r0N[g(r0,x) − SN(r0,x)] → 0 for each fixed x and N.
ScaledGradientSeriesIdentificationAt ties the readout to the same density shape at scaled positions and identifies the fourth-order sum with the actual energy density minus its remainder. The fifth-order coefficient is zero. identified_expected_gradient_asymptotics_retain_the_sixth_order_coefficient then gives r06R6 − a6(x) → 0. This conclusion remains conditional on the author's expectation and the source calculation; it is not an independently proved electron-gas asymptotic theorem.
expected_gradient_atom_retains_orderwise_scale_error_budgets gives eventual error below ε/r0N at each fixed position and order. Neither a uniform threshold in position or order, an explicit numerical threshold, nor termwise integration of this limit is inferred. A nine-theorem independent client uses coefficients summing to 3 and a nonzero correction 5 exp(−r0), with four audited public API uses. The former shared two-predicate wrapper has been retired pending independently earned reuse.
integral gbarr[n] dr = slowly varying gradient value. equation (63) after rotational reduction and divergence equivalence; conditional on the unproved expansion assumption (9)
Uniform linear and nonlinear response functions, two explicit scale-validity conditions, and a deferred matching calculation determine all gradient coefficients. The first compares the relative-density-gradient wave number with kF; the second separately compares the gradient-curvature wave number with kF. Lean keeps their qualitative parametric-smallness relation paper-local but requires it to imply strict ordering, and a countermodel prevents the first condition from supplying the pair. Independently, the source map records that the series does not strictly converge for finite r0. That negative result has paper-derivation status. A separate author expectation says the series should nevertheless be asymptotically useful as r0 becomes large.
finite r0 → no strict convergence,
large r0 → asymptotic usefulness expected. equations (81)-(82) are separate necessary inputs; coefficient calculation, finite-scale nonconvergence, and expected usefulness have distinct statuses (10)
The route first derives equation (63)'s local fourth-order structure and integral bridge, then preserves the unproved existence assumption, response inputs, both equation-(81)/(82) scale conditions, coefficient calculation, paper-derived failure of finite-scale strict convergence, and author-qualified asymptotic usefulness. gradient_validity_retains_both_necessary_scale_conditions exposes the conjunction and its strict-order consequence. Paper-local coefficient sums and actual scale limits retain these two distinct assertions.
slowly_varying_calculation_retains_equation_sixty_three_formula · equation_sixty_three_retains_fourth_order_gradient_structure · equation_sixty_three_retains_integrated_gradient_functional_bridge · slowly_varying_density_yields_gradient_expansion_conditionally · gradient_validity_retains_both_necessary_scale_conditions · gradient_coefficients_are_fixed_by_uniform_response_functions · gradient_expansion_retains_nonconvergence_and_expected_asymptotics · finite_scale_nonconvergence_is_not_an_author_expectation · Physical Review pp. B868–B870The slow-gradient result also reuses the established shared finite-truncation interface: expected_identified_gradient_series_realizes_shared_controlled_truncation supplies actual fourth-order error control at sufficiently large scale, and expected_identified_gradient_series_has_an_inhabited_controlled_truncation provides a nonempty controlled regime. The result is conditional on the source expectation and independent of the empirical assessment. It does not certify a measured approximation or justify the separate partial summation discussed next.
The partial summation interpolates exactly between two declared limits but remains untested
Equation (83) is retained before its limit claims: at every three-dimensional position it sums the uniform-gas residual-energy density and a spatial integral of the local-density kernel times the two symmetric half-displacement density differences, apart from possible divergence or higher-order terms. Equation (84) then fixes that kernel through the dielectric reciprocal-momentum Fourier series with explicit volume, denominator, and summability conditions. Equation (64) integrates the local readout to the global residual functional. Under the established nearly uniform expansion and the conditional slowly varying expansion, the proposed value equals the same residual functional in each corresponding limit.
Kn(r') = (1/Omega) sumq (2 pi/q2) epsilonn(q)-1 exp(-i q.r'),
integral gbarr[n] dr = partial-summation value,
displayed formula + nearly uniform expansion + slowly varying expansion → exact residual-functional value in both declared limits,
and a separate atomic calculation → finite nuclear density + atomic shell oscillations. the spatial integral and summable reciprocal-mode calculation remain explicit paper inputs; quantitative use is not yet tested on actual physical systems (11)
The route first derives equation (84)'s local-density Fourier kernel and equation (83)'s local formula for every density, including opposite half-displacements, qualified remainders, and the global integral bridge. Only then does it specialize to the two declared limits, certify exactness there, and retain the two stated atomic predictions together with the absence of actual-system tests.
partial_summation_retains_equation_eighty_four_kernel_formula · equation_eighty_four_retains_local_density_fourier_kernel · partial_summation_retains_equation_eighty_three_formula · equation_eighty_three_retains_symmetric_half_displacements · equation_eighty_three_retains_integrated_functional_bridge · partial_summation_is_exact_in_both_declared_limits · partial_summation_reproduces_both_limiting_expansions · partial_summation_gives_stated_atomic_predictions · Physical Review pp. B870–B871Concept guide
Density determination
Uniqueness of the external potential up to a constant and of the nondegenerate ground state at fixed particle number.
NondegenerateGroundStateAtParticleNumberUniversal internal functional
The density functional built from fixed kinetic and mutual Coulomb energies, independent of the selected external potential, after the theorem-I density-determination bridge is supplied in the selected particle-number sector.
DensityDeterminationSuppliesUniversalFunctionalAt · UniversalFunctionalConstructionAtParticleNumberGround-density minimum
Attainment of the physical ground energy and minimization over representable densities at fixed particle number.
GroundDensityVariationalPrincipleGround-state representability
Existence of a nondegenerate ground state and potential realizing a candidate density at the selected particle number. Footnote 12 keeps this exact notion separate from first-order external realizability near a uniform density and from the authors' broader nonpathological expectation.
DensityRepresentableAtParticleNumber · FirstOrderUniformPerturbationRealizabilityAt · GenericNonpathologicalGroundStateRepresentabilityAtHartree–residual decomposition
Separation of the universal functional into classical Coulomb and residual terms.
UniversalHartreeDecompositionNearly uniform response
A controlled small zero-mean density perturbation whose residual-functional kernel is fixed by uniform-gas response, with equations (35)-(37) retaining the polarizability formula, dielectric definition, and checked dielectric rewrite, equations (38)-(40) retaining α's small-q, 2kF, and q-4 limits, equations (44)-(46) retaining the transferred kernel limits, and equations (47)-(48) retaining the distributional position kernel and explicit residual-functional gradient formula.
NearlyUniformResponseCalculation · EquationThirtySixDielectricFormulaAt · EquationThirtySevenKernelFormulaAt · PolarizabilityResponseAsymptoticStructureAt · KernelResponseAsymptoticStructureAt · EquationFortySevenPositionKernelDistributionFormulaAt · EquationFortyEightNearlyUniformGradientFunctionalFormulaAtFriedel structure
Nonanalyticity at twice the Fermi momentum together with an oscillatory inverse-cube real-space tail.
HasFriedelTailFinite-gradient obstruction
The incompatibility between an analytic finite gradient kernel and the full nonanalytic Friedel structure.
FiniteGradientMissesFriedelOscillationsSlowly varying expansion
A fourth-order gradient construction conditional on an unproved expansion assumption, with equation (63)'s gradient-square, Laplacian-square, mixed, quartic, and sixth-order-remainder terms retained explicitly.
EquationSixtyThreeGradientExpansionFormulaAt · SlowlyVaryingGradientCalculationGradient validity
The conjunction of the two necessary scale conditions in equations (81)-(82): relative-density-gradient and gradient-curvature wave numbers are each parametrically smaller than the local Fermi wave number.
gradientValidityConditions · firstGradientValidityConditionAt · secondGradientValidityConditionAtNonconvergent asymptotic status
Strict convergence is denied at finite scale as a paper-derived result, while usefulness at large scale remains an author expectation.
gradientExpansionAsymptoticallyUsefulPartial summation
Equation (83) as a local three-dimensional energy-density formula with symmetric half-displacement density differences and a global integral bridge, together with equation (84)'s summable local-density dielectric Fourier kernel. The equation-(84) 1/epsilon subseries remains distinct from equation (37)'s 1/(epsilon-1) exact-kernel rewrite; the resulting proposal is exact in the two encoded limits, predictive for atomic features, and untested on actual systems.
EquationEightyFourLocalDensityKernelFormula · EquationEightyThreePartialSummationFormulaAt · PartialSummationCalculationShared density semantics
Separate representation, restricted determination, and variational models with explicit grounding.
toSharedDensityFunctionalContextComplete route inventory, formal separations, and provenance
The source map declares seven routes and sixty-five claims. Coverage gives every atom paper-local semantics, certifies every route under its explicit dependencies, and proves semantic realization exhaustive from raw paper-local inputs rather than assumed route certificates.
| Route | Direct dependency | Output | Profile |
|---|---|---|---|
| Density determination | — | Potential, state, and restricted density determination | exact theorem |
| Density variational | Density determination | Ground-energy minimum and decomposed functional | exact representable-domain theorem |
| Representability scope | — | Open global converse, first-order local result, expected nonpathological scope | open + controlled + expected |
| Nearly uniform response | — | Expansion, kernel, nonanalyticity, and Friedel tail | controlled + deferred |
| Finite-gradient limitation | Nearly uniform | Failure to capture Friedel oscillations | analyticity obstruction |
| Slowly varying response | — | Equation-(63) formula, conditional expansion, coefficients, expected usefulness | assumed + expected |
| Partial summation | Nearly uniform; slowly varying | Equation-(84) kernel, equation-(83) formula, two-limit exactness, atomic predictions, untested status | proposed interpolation |
Density determination · density_determination_route_is_semantically_realized
Density variation · density_variational_route_is_semantically_realized
Representability scope · representability_scope_route_is_semantically_realized
Nearly uniform response · nearly_uniform_route_is_semantically_realized
Finite-gradient limit · finite_gradient_limitation_route_is_semantically_realized
Slowly varying response · slowly_varying_route_is_semantically_realized
Partial summation · partial_summation_route_is_semantically_realized
Concrete counterexamples
The gradient-series examples are actual sums and limits. A geometric diagnostic has all-order large-scale asymptotics but divergent partial sums at scale one; it is not the electron-gas series. A nonzero exponential correction is invisible to every inverse-power coefficient. Consequently, even convergent asymptotic coefficients need not sum to the target readout. These three new registered boundaries supplement the response and density-functional controls below.
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| A continuous local critical response with a divergent derivative | Analyticity at the critical point | the_continuous_critical_response_has_a_divergent_derivative |
| An actual finite isotropic gradient polynomial | The source's divergent derivative | a_finite_gradient_control_does_not_have_the_source_derivative_singularity |
| A nonzero oscillatory inverse-cube tail | Exact equality with its leading profile | a_subleading_correction_preserves_the_tail_but_not_exact_equality |
| Positive frequency and nonzero leading amplitude | A nonvanishing leading profile at every positive radius | a_nonzero_oscillatory_leading_tail_has_positive_radius_nodes |
| Nonoscillating inverse-cube decay | A Friedel tail with nonzero frequency | inverse_cube_decay_without_nonzero_frequency_is_not_a_friedel_tail |
| Equation (81)'s first gradient scale condition | The conjunction with equation (82)'s second condition | first_gradient_condition_alone_does_not_supply_full_gradient_validity |
| A named slowly varying gradient expansion | Equation (63)'s local fourth-order formula | named_gradient_expansion_does_not_supply_equation_sixty_three_formula |
| A common density for degenerate ground states | Ground-state identity | common_density_does_not_identify_degenerate_ground_states |
| A positive normalized candidate density | Ground-state representability | positive_normalized_density_need_not_be_ground_state_representable |
| Positive normalization alone | The universal representability implication | positive_normalization_alone_does_not_entail_ground_state_representability |
| First-order perturbative realizability | Generic nonpathological exact representability | first_order_representability_does_not_establish_generic_nonpathological_representability |
| A named local-density kernel | Equation (84)'s reciprocal-momentum Fourier formula | named_local_density_kernel_does_not_supply_equation_eighty_four_formula |
| A named partial-summation label | Equation (83)'s local symmetric half-displacement formula | named_partial_summation_does_not_supply_equation_eighty_three_formula |
| Exactness in two limits | Accuracy on an actual system | exactness_in_two_limits_does_not_imply_actual_system_accuracy |
| A global functional minimizer | Equality of the minimum with physical ground energy | minimization_alone_does_not_identify_physical_ground_energy |
| Potential-dependent internal energy | A universal density functional | potential_dependent_internal_energy_cannot_be_a_universal_density_functional |
Value-level countermodels retain the physical scope
The gradient witness keeps both wave-number comparisons, so the relative-density-gradient condition can hold while the gradient-curvature condition fails. Degeneracy, normalization, representability, and footnote-12 witnesses retain state index, potential sector, density integral, particle number, ground energy, external-potential witness, perturbative order, linear-response obstruction, and pathology separately. The formula witnesses keep positive density and box volume while a displayed energy relation or the nonzero-mode domain fails; the two exact limits use different scale data and leave an actual-system error. These are physical non-implications, not truth-value labels.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify graph structure. routes_have_exact_predecessor_graph, the source-contract and local-input guards, the selected-input result guards, dependent_steps_name_inherited_outputs, density_variational_route_consumes_certified_determination, and dependent_routes_consume_certified_predecessor_outputs pin the theorem-I-to-theorem-II bridge and the later approximation dependencies. dielectric_rewrite_depends_on_equations_35_and_36 separately guards the equation-(35)/(36) to equation-(37) step, response_asymptotic_chain_depends_on_equations_38_to_46 guards the response-to-kernel limit chain, and position_space_gradient_formulas_depend_on_equations_44_to_46 guards the position-space formulas' dependence on that kernel block. every_source_claim_has_semantics covers all sixty-five claims, and route_semantic_realization_is_exhaustive constructs and covers all seven routes from raw paper-local inputs. Coverage additionally reconstructs every routed result from its premise map instead of accepting a precomputed conclusion or extracting a predecessor result from a route certificate. Dedicated status theorems preserve the density minimum's physical and imported inputs, its local ground-energy identification, independence from all three representability-scope outputs, the local first-order result and expected generic scope, absence of deferred calculation in density determination, the unproved gradient assumption, paper-derived finite-scale nonconvergence, expected asymptotic usefulness, dependence on full Friedel structure, the explicit equation-(63), equation-(84), and equation-(83) formula dependencies, and untested partial summation.
Lean-encoded bibliographic record
P. Hohenberg and W. Kohn, Inhomogeneous Electron Gas (1964), Physical Review pp. B864–B871.
TraceComplete Lean semantic identifier ledger
Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.
Primary semantic theorems (110)
positive_derivative_divergence_excludes_analyticitynegative_derivative_divergence_excludes_analyticitya_finite_isotropic_gradient_kernel_is_analytica_finite_gradient_kernel_cannot_agree_near_a_nonanalytic_kernelthe_leading_profile_has_its_own_friedel_taila_friedel_tail_is_an_actual_scaled_envelope_limitinverse_cube_small_remainders_preserve_the_friedel_tailthe_continuous_critical_response_has_a_divergent_derivativea_finite_gradient_control_does_not_have_the_source_derivative_singularitya_subleading_correction_preserves_the_tail_but_not_exact_equalitya_nonzero_oscillatory_leading_tail_has_positive_radius_nodesinverse_cube_decay_without_nonzero_frequency_is_not_a_friedel_tailpartialSum_succasymptotic_series_has_an_eventual_orderwise_error_budgetbeyond_all_orders_remainders_preserve_the_expansionsame_asymptotic_coefficients_allow_only_beyond_all_orders_differencesthe_constant_partial_sums_are_onethe_constant_series_is_asymptotica_nonzero_exponential_correction_is_invisible_at_every_gradient_orderconvergent_asymptotic_coefficients_need_not_sum_to_the_targetthe_geometric_series_has_an_exact_orderwise_remainderthe_geometric_series_is_asymptoticasymptotic_usefulness_does_not_give_convergence_at_every_finite_scalegradient_control_does_not_depend_on_the_empirical_assessmentground_density_representation_is_soundactual_ground_density_is_physically_sound_representationgradient_validity_retains_both_necessary_scale_conditionsdielectric_constant_obeys_equation_36equations_35_and_36_yield_equation_37polarizability_derivative_singularity_derives_actual_nonanalyticitykernel_derivative_singularity_derives_actual_nonanalyticityfirst_order_uniform_perturbation_realizability_retains_scopegeneric_nonpathological_representability_retains_scopecomparison_core_preserves_exact_source_conditionspotential_difference_integral_is_antisymmetricstrict_variational_inequalities_for_common_densitysame_density_forces_potentials_to_differ_only_by_constantsame_density_determines_nondegenerate_ground_stateground_density_realization_has_derivation_bridgenondegenerate_density_uniqueness_realizes_strict_microreductionshared_ground_density_model_retains_exact_semanticspaper_setup_realizes_shared_selected_ground_density_setupnondegenerate_density_uniqueness_realizes_restricted_determinationnondegenerate_density_uniqueness_realizes_equality_qualified_determinationnondegenerate_ground_state_inputs_realize_nonvacuous_static_density_potential_determinationhohenberg_kohn_strict_variational_source_realizes_density_potential_explanationshared_source_hohenberg_kohn_density_route_retains_original_derivationdensity_determination_and_bridge_construct_universal_functionalglobal_universal_functional_construction_restricts_to_particle_numberuniversal_functional_has_fixed_kinetic_coulomb_contentground_density_minimizes_energy_over_representable_densitiesground_density_attains_ground_energyground_density_realizes_variational_principledensity_variational_bridge_realizeddensity_variational_calculation_realizedground_density_inputs_make_shared_variational_route_applicableground_density_inputs_realize_structural_ground_density_variational_explanationhohenberg_kohn_source_inputs_realize_source_structural_ground_density_variational_explanationground_density_variational_route_establishes_shared_contextground_density_route_exhibits_nonvacuous_shared_variational_principleground_density_setup_realizes_physically_sound_shared_representationground_density_setup_realizes_scoped_descriptive_completenessground_density_model_inputs_establish_theory_model_groundingground_density_variational_route_establishes_theory_model_grounded_shared_contextground_density_variational_route_transfers_every_shared_claimground_density_variational_principle_realizes_shared_contexttotal_energy_uses_hartree_residual_decompositionnearly_uniform_functional_is_fixed_by_uniform_responsenearly_uniform_kernel_obeys_equation_35nearly_uniform_response_obeys_equation_37kernel_response_calculation_retains_equations_44_to_46position_space_gradient_calculation_retains_equations_47_and_48polarizability_nonanalyticity_yields_friedel_oscillationsfriedel_tail_exposes_the_fermi_scale_and_actual_envelope_limitthe_friedel_calculation_retains_its_actual_scaled_envelopeanalytic_momentum_kernel_excludes_friedel_capturefinite_gradient_kernel_cannot_agree_near_two_fermi_momentumfinite_gradient_expansion_cannot_capture_friedel_oscillationsfriedel_capture_exposes_nonanalytic_kernel_and_inverse_cube_tailslowly_varying_density_yields_gradient_expansion_conditionallyslowly_varying_calculation_retains_equation_sixty_three_formulaequation_sixty_three_retains_fourth_order_gradient_structureequation_sixty_three_retains_integrated_gradient_functional_bridgegradient_coefficients_are_fixed_by_uniform_response_functionsgradient_expansion_usefulness_retains_asymptotic_expectationgradient_expansion_retains_nonconvergence_and_expected_asymptoticsslowly_varying_calculation_identifies_the_scaled_gradient_seriesidentified_expected_gradient_asymptotics_control_the_actual_sixth_order_remainderexpected_identified_gradient_series_realizes_shared_controlled_truncationexpected_identified_gradient_series_has_an_inhabited_controlled_truncationidentified_expected_gradient_asymptotics_retain_the_sixth_order_coefficientpartial_summation_is_exact_in_both_declared_limitspartial_summation_retains_equation_eighty_four_kernel_formulaequation_eighty_four_retains_local_density_fourier_kernelpartial_summation_retains_equation_eighty_three_formulaequation_eighty_three_retains_symmetric_half_displacementsequation_eighty_three_retains_integrated_functional_bridgepartial_summation_reproduces_both_limiting_expansionspartial_summation_gives_stated_atomic_predictionsfirst_gradient_condition_alone_does_not_supply_full_gradient_validitynamed_gradient_expansion_does_not_supply_equation_sixty_three_formulacommon_density_does_not_identify_degenerate_ground_statespositive_normalized_density_need_not_be_ground_state_representablepositive_normalization_alone_does_not_entail_ground_state_representabilityfirst_order_representability_does_not_establish_generic_nonpathological_representabilitynamed_local_density_kernel_does_not_supply_equation_eighty_four_formulanamed_partial_summation_does_not_supply_equation_eighty_three_formulaexactness_in_two_limits_does_not_imply_actual_system_accuracyminimization_alone_does_not_identify_physical_ground_energypotential_dependent_internal_energy_cannot_be_a_universal_density_functional
Coverage theorems (12)
every_source_claim_has_semanticsuniversal_functional_atom_exposes_fixed_kinetic_coulomb_contentdensity_determination_route_is_semantically_realizeddensity_variational_route_is_semantically_realizedrepresentability_scope_route_is_semantically_realizednearly_uniform_route_is_semantically_realizedfinite_gradient_limitation_route_is_semantically_realizedslowly_varying_route_is_semantically_realizedpartial_summation_route_is_semantically_realizedexpected_gradient_atom_retains_orderwise_scale_error_budgetsfriedel_tail_atom_retains_the_actual_scaled_envelopeall_routes_are_semantically_realizable
Source-map audit theorems (30)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphroutes_have_exact_dependency_closureexact_source_contracts_are_independent_hypothesesresponse_and_gradient_source_contracts_are_independent_hypothesesexact_and_scope_inputs_are_independent_hypothesesapproximation_local_inputs_are_independent_hypothesespartial_summation_source_inputs_are_independent_hypothesesexact_result_steps_apply_selected_inputs_and_contractsresponse_and_gradient_result_steps_apply_selected_inputs_and_contractspartial_summation_result_steps_apply_selected_inputs_and_contractsdependent_steps_name_inherited_outputsdensity_variational_route_consumes_certified_determinationdependent_routes_consume_certified_predecessor_outputsdensity_minimum_retains_representability_and_variational_inputsdensity_minimum_depends_on_local_ground_energy_identificationrepresentability_scope_retains_open_obligation_statusrepresentability_scope_retains_local_result_and_expected_global_scopedensity_minimum_is_independent_of_representability_scopedensity_determination_does_not_hide_deferred_calculationdielectric_rewrite_depends_on_equations_35_and_36response_asymptotic_chain_depends_on_equations_38_to_46position_space_gradient_formulas_depend_on_equations_44_to_46gradient_results_retain_unproved_expansion_assumptionasymptotic_usefulness_retains_author_expectationfinite_scale_nonconvergence_is_not_an_author_expectationfinite_gradient_failure_depends_on_full_friedel_structurepartial_summation_retains_untested_status
Semantic atoms (65)
selectedNondegenerateSameDensitySetupgroundStateEnergyEquationstrictNondegenerateVariationalPrinciplepotentialEnergyDifferenceEquationnonconstantPotentialsGiveDistinctGroundStatesstrictVariationalInequalitiesEq6Eq7potentialDifferenceAntisymmetrypotentialsDifferOnlyByConstantconstantShiftPreservesGroundStatesnondegenerateGroundStateUniquenessselectedGroundStatesEqualrestrictedDensityDeterminationcorrectGroundStateSetupvariationalGroundStateEnergyEquationdensityDeterminationUniversalFunctionalBridgeuniversalFunctionalConstructionwavefunctionVariationalPrinciplegroundDensityEnergyMinimumpositiveNormalizationDoesNotEstablishRepresentabilityfirstOrderPerturbativeDensitiesExternallyRealizablegenericNonpathologicalRepresentabilityExpecteduniversalHartreeDecompositiondecomposedTotalEnergynearlyUniformSetupnearlyUniformResponseCalculationexactNearlyUniformExpansionkernelFromPolarizabilitydielectricDefinitionEquationThirtySixdielectricKernelEquationThirtySevenpolarizabilityResponseEquationsThirtyEightToFortykernelResponseAsymptoticCalculationkernelResponseEquationsFortyFourToFortySixpositionSpaceGradientExpansionCalculationpositionKernelEquationFortySevennearGradientFunctionalEquationFortyEighttwoFermiMomentumNonanalyticityfriedelOscillationCalculationnonanalyticFunctionalKernelfriedelOscillationsfiniteGradientSetupfiniteGradientAnalyticityCalculationanalyticFriedelObstructionfiniteGradientMissesFriedelOscillationsslowlyVaryingSetupgradientExpansionAssumptionrotationalInvariancedivergenceFreedomslowlyVaryingGradientCalculationslowlyVaryingEquationSixtyThreeFormulaslowlyVaryingGradientExpansionuniformResponseDatagradientValidityConditionsgradientResponseMatchingCalculationgradientCoefficientsFromResponsesgradientExpansionStrictlyConvergesAtFiniteScalegradientAsymptoticExpectationgradientExpansionAsymptoticallyUsefulpartialSummationSetuppartialSummationCalculationpartialSummationEquationEightyFourKernelFormulapartialSummationEquationEightyThreeFormulaexactInBothLimitsatomicPredictionCalculationfiniteNuclearDensityAndShellOscillationspartialSummationTestedOnActualSystems
Claim identifiers (65)
densitySetupgroundEnergyEquationstrictVariationalPrinciplepotentialDifferenceEquationnonconstantDistinctStatesstrictInequalitiesdifferenceAntisymmetrypotentialUniquenessconstantShiftTransportnondegenerateUniquenessselectedStateUniquenessgenericRestrictedDeterminationvariationalSetupvariationalGroundEnergyEquationdensityToUniversalBridgeuniversalConstructionwavefunctionVariationaldensityMinimumrepresentabilityScopefirstOrderRepresentabilitygenericRepresentabilityExpectationhartreeDecompositiondecomposedEnergynearSetupnearCalculationnearExpansionpolarizabilityKerneldielectricDefinitiondielectricKernelresponseAsymptoticskernelAsymptoticCalculationkernelAsymptoticspositionGradientCalculationpositionKernelFormulanearGradientFunctionalFormularesponseNonanalyticityfriedelCalculationkernelNonanalyticityfriedelTailfiniteGradientgradientAnalyticityfriedelObstructiongradientFailureslowSetupgradientAssumptionrotationalReductiondivergenceReductionslowCalculationslowFormulaslowExpansionresponseInputsvalidityInputsresponseMatchingresponseDeterminedCoefficientsfiniteScaleNonconvergenceasymptoticExpectationasymptoticUsefulnesspartialSetuppartialCalculationpartialKernelFormulapartialFormulatwoLimitExactnessatomicCalculationatomicPredictionsuntestedActualSystems
Step identifiers (65)
stateDensitySetupstateGroundStateEnergyEquationinvokeStrictVariationalPrincipledefinePotentialDifferenceEquationderiveDistinctStatesForNonconstantPotentialsderiveStrictVariationalInequalitiesderivePotentialDifferenceAntisymmetryderivePotentialUniquenessstateConstantShiftGroundStateTransportinvokeNondegenerateGroundStateUniquenessderiveSelectedStateUniquenessrealizeRestrictedDeterminationstateVariationalSetupstateVariationalGroundStateEnergyEquationstateDensityToUniversalBridgeconstructUniversalFunctionalinvokeWavefunctionVariationalPrinciplederiveDensityMinimumrecordRepresentabilityScoperecordFirstOrderRepresentabilityrecordGenericRepresentabilityExpectationseparateHartreeTermderiveDecomposedEnergystateNearlyUniformSetupstateNearlyUniformCalculationderiveNearlyUniformExpansionderivePolarizabilityKernelstateDielectricDefinitionderiveDielectricKernelstateResponseAsymptoticsderiveResponseNonanalyticitystateKernelAsymptoticCalculationderiveKernelAsymptoticsstatePositionGradientCalculationderivePositionKernelFormuladeriveNearGradientFunctionalFormulastateFriedelCalculationderiveKernelNonanalyticityderiveFriedelTailchooseFiniteGradientApproximationstateFiniteGradientAnalyticitystateAnalyticFriedelObstructionexcludeFriedelCapturestateSlowlyVaryingSetupassumeGradientExpansionimposeRotationalInvariancequotientByDivergencesstateSlowlyVaryingCalculationderiveSlowlyVaryingFormuladeriveSlowlyVaryingExpansionstateUniformResponseInputsstateGradientValidityInputsstateResponseMatchingCalculationderiveResponseDeterminedCoefficientsrecordFiniteScaleNonconvergencestateAsymptoticExpectationinferAsymptoticUsefulnessintroducePartialSummationstatePartialSummationCalculationderivePartialSummationKernelFormuladerivePartialSummationFormuladeriveTwoLimitExactnessstateAtomicPredictionCalculationderiveAtomicPredictionsrecordUntestedActualSystems
Route identifiers (7)
densityDeterminationdensityVariationalrepresentabilityScopenearlyUniformfiniteGradientLimitationslowlyVaryingpartialSummation
Route kinds (7)
exactGroundStateTheoremexactVariationalTheoremqualifiedRepresentabilityScopecontrolledResponseExpansionapproximationObstructionassumedAsymptoticExpansionproposedInterpolation
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.
densityDetermination
Logical kind: exactGroundStateTheorem.
Required predecessor routes: none.
Ordered inference steps: stateDensitySetup, stateGroundStateEnergyEquation, invokeStrictVariationalPrinciple, definePotentialDifferenceEquation, deriveDistinctStatesForNonconstantPotentials, deriveStrictVariationalInequalities, derivePotentialDifferenceAntisymmetry, derivePotentialUniqueness, stateConstantShiftGroundStateTransport, invokeNondegenerateGroundStateUniqueness, deriveSelectedStateUniqueness, realizeRestrictedDetermination.
Exported conclusions: potentialUniqueness, selectedStateUniqueness, genericRestrictedDetermination.
densityVariational
Logical kind: exactVariationalTheorem.
Required predecessor routes: densityDetermination.
Ordered inference steps: stateVariationalSetup, stateVariationalGroundStateEnergyEquation, stateDensityToUniversalBridge, constructUniversalFunctional, invokeWavefunctionVariationalPrinciple, deriveDensityMinimum, separateHartreeTerm, deriveDecomposedEnergy.
Exported conclusions: densityMinimum, decomposedEnergy.
representabilityScope
Logical kind: qualifiedRepresentabilityScope.
Required predecessor routes: none.
Ordered inference steps: recordRepresentabilityScope, recordFirstOrderRepresentability, recordGenericRepresentabilityExpectation.
Exported conclusions: representabilityScope, firstOrderRepresentability, genericRepresentabilityExpectation.
nearlyUniform
Logical kind: controlledResponseExpansion.
Required predecessor routes: none.
Ordered inference steps: stateNearlyUniformSetup, stateNearlyUniformCalculation, deriveNearlyUniformExpansion, derivePolarizabilityKernel, stateDielectricDefinition, deriveDielectricKernel, stateResponseAsymptotics, deriveResponseNonanalyticity, stateKernelAsymptoticCalculation, deriveKernelAsymptotics, statePositionGradientCalculation, derivePositionKernelFormula, deriveNearGradientFunctionalFormula, stateFriedelCalculation, deriveKernelNonanalyticity, deriveFriedelTail.
Exported conclusions: nearExpansion, polarizabilityKernel, dielectricKernel, responseAsymptotics, kernelAsymptotics, positionKernelFormula, nearGradientFunctionalFormula, kernelNonanalyticity, friedelTail.
finiteGradientLimitation
Logical kind: approximationObstruction.
Required predecessor routes: nearlyUniform.
Ordered inference steps: chooseFiniteGradientApproximation, stateFiniteGradientAnalyticity, stateAnalyticFriedelObstruction, excludeFriedelCapture.
Exported conclusions: gradientFailure.
slowlyVarying
Logical kind: assumedAsymptoticExpansion.
Required predecessor routes: none.
Ordered inference steps: stateSlowlyVaryingSetup, assumeGradientExpansion, imposeRotationalInvariance, quotientByDivergences, stateSlowlyVaryingCalculation, deriveSlowlyVaryingFormula, deriveSlowlyVaryingExpansion, stateUniformResponseInputs, stateGradientValidityInputs, stateResponseMatchingCalculation, deriveResponseDeterminedCoefficients, recordFiniteScaleNonconvergence, stateAsymptoticExpectation, inferAsymptoticUsefulness.
Exported conclusions: slowFormula, slowExpansion, responseDeterminedCoefficients, finiteScaleNonconvergence, asymptoticUsefulness.
partialSummation
Logical kind: proposedInterpolation.
Required predecessor routes: nearlyUniform, slowlyVarying.
Ordered inference steps: introducePartialSummation, statePartialSummationCalculation, derivePartialSummationKernelFormula, derivePartialSummationFormula, deriveTwoLimitExactness, stateAtomicPredictionCalculation, deriveAtomicPredictions, recordUntestedActualSystems.
Exported conclusions: partialKernelFormula, partialFormula, twoLimitExactness, atomicPredictions, untestedActualSystems.