Ground-State Classes and Density Determination

Exact root statement

∀ {Potential : Type u} {State : Type v} {Density : Type w} {Approximation : Type z}
  (framework : DensityFunctionalFramework Potential State Density Approximation) (relation : Setoid State)
  (invariant : Invariant framework relation) (selected : State) (particleNumber : ℕ),
  framework.NondegenerateGroundStateAtParticleNumber selected particleNumber →
    NonconstantSeparationUpTo framework relation →
      framework.GroundStateEnergyEquation →
        framework.PotentialEnergyDifferenceEquation →
          StrictVariationUpTo framework relation →
            framework.ConstantShiftPreservesGroundStates →
              NondegenerateUniquenessUpTo framework relation →
                (onClasses framework relation invariant).toDeterminationContext.ReducedDeterminesFullAt particleNumber