import PhysicsLogicConsumer.CondensedMatter.DensityVariational

/- Definition-only contracts for the finite diagnostic model, not human approval.
No theorem from the consumer is used to justify these characterizations. -/
set_option autoImplicit false

open PhysicsLogic.Framework
open PhysicsLogicConsumer.CondensedMatter.DensityVariational
open scoped BigOperators

example : Wave = (Fin 3 -> Complex) := rfl
example : Density = (Fin 3 -> Real) := rfl

example (first second : Fin 3) :
    kineticMatrix first second = if first = second then 2 else -1 := rfl

example (wave : Wave) (site : Fin 3) : density wave site = Complex.normSq (wave site) := rfl

example (wave : Wave) : mass wave = ∑ site, density wave site := rfl

example (wave : Wave) : NormalizedAt wave ↔ (∑ site, density wave site) = 1 := Iff.rfl

example (wave : Wave) :
    kineticEnergy wave = (∑ site, star (wave site) * ∑ other, kineticMatrix site other * wave other).re := rfl

example (charge : Density) :
    AdmissibleAt charge ↔ (∀ site, 0 ≤ charge site) ∧ (∑ site, charge site) = 1 := Iff.rfl

example (charge : Density) : positiveWave charge = fun site => (Real.sqrt (charge site) : Complex) := rfl

example (charge : Density) : constrainedKinetic charge = 3 - (∑ site, Real.sqrt (charge site)) ^ 2 := rfl

example : uniformDensity = fun _ => (1 / 3 : Real) := rfl
example : uniformWave = positiveWave uniformDensity := rfl
example : phaseChangedWave = fun site =>
    if site = 1 then -(Real.sqrt (1 / 3) : Complex) else (Real.sqrt (1 / 3) : Complex) := rfl

example (left right : Wave) : GlobalPhaseEquivalent left right ↔
    ∃ phase : Complex, Complex.normSq phase = 1 ∧ ∀ site, right site = phase * left site := Iff.rfl

example : globallyNegatedWave = fun site => -uniformWave site := rfl

example : context = ({
    selectedState := uniformWave
    selectedPotential := ()
    selectedParticleNumber := 1
    densityOf := density
    particleNumber := fun _ => 1
    groundStateAt := fun wave _ number => number = 1 ∧ NormalizedAt wave ∧ kineticMatrix.mulVec wave = 0
    admissibleDensityAt := fun charge number => number = 1 ∧ AdmissibleAt charge
    externalPotentialEnergy := fun _ _ => 0
    universalInternalEnergy := constrainedKinetic
    physicalGroundEnergy := fun _ => kineticEnergy uniformWave
  } : DensityFunctionalContext Unit Wave Density) := rfl

example : localizedDensity = ![1, 0, 0] := rfl
example : localizedWave = ![1, 0, 0] := rfl

example (potential : Fin 3 → Real) (energy : Real) (wave : Wave) :
    LocalPotentialEigenstateAt potential energy wave ↔
      ∀ site, (∑ other, kineticMatrix site other * wave other) +
          (potential site : Complex) * wave site = (energy : Complex) * wave site := Iff.rfl

example (potential : Fin 3 -> Real) (wave : Wave) : totalEnergy potential wave =
    kineticEnergy wave + ∑ site, potential site * Complex.normSq (wave site) := rfl

example (left right : Fin 3 -> Real) : ConstantShiftEquivalent left right ↔
    ∃ shift : Real, ∀ site, right site = left site + shift := Iff.rfl

example (potential : Fin 3 -> Real) (energy : Real) (wave : Wave) :
    NondegenerateGroundAt potential energy wave ↔
      mass wave = 1 ∧
        (∀ site, (∑ other, kineticMatrix site other * wave other) +
          (potential site : Complex) * wave site = (energy : Complex) * wave site) ∧
        ∀ candidate : Wave, mass candidate = 1 ->
          kineticEnergy wave + (∑ site, potential site * Complex.normSq (wave site)) ≤
            kineticEnergy candidate + (∑ site, potential site * Complex.normSq (candidate site)) ∧
          (kineticEnergy wave + (∑ site, potential site * Complex.normSq (wave site)) =
              kineticEnergy candidate + (∑ site, potential site * Complex.normSq (candidate site)) ->
            ∃ phase : Complex, Complex.normSq phase = 1 ∧ ∀ site, candidate site = phase * wave site) := Iff.rfl

example (potential : Fin 3 -> Real) (energy : Real) (wave : Wave) :
    (PotentialState.mk potential energy wave).potential = potential := rfl
example (potential : Fin 3 -> Real) (energy : Real) (wave : Wave) :
    (PotentialState.mk potential energy wave).energy = energy := rfl
example (potential : Fin 3 -> Real) (energy : Real) (wave : Wave) :
    (PotentialState.mk potential energy wave).wave = wave := rfl

example : potentialDetermination = ({
    reduce := fun state => density state.wave
    admissible := fun state _ => NondegenerateGroundAt state.potential state.energy state.wave
    equivalent := fun left right _ => ∃ shift : Real, ∀ site,
      right.potential site = left.potential site + shift
  } : PhysicsLogic.Philosophy.Determination.EquivalenceQualifiedDeterminationContext PotentialState Density Unit) := rfl

example : excitedPotential = ![-2, -4, -2] := rfl

example (coupling : Real) : penalizedDensityModel coupling = ({
    state := uniformWave
    potential := ()
    density := density uniformWave
    particleNumber := 1
    densityOf := density
    particleNumberOf := fun _ => 1
    groundStateAt := fun wave _ number => number = 1 ∧ NormalizedAt wave ∧ kineticMatrix.mulVec wave = 0
    admissibleDensityAt := fun charge number => number = 1 ∧ AdmissibleAt charge
    externalPotentialEnergy := fun _ _ => 0
    universalInternalEnergy := fun charge => constrainedKinetic charge + coupling * (charge 0 - 1 / 3) ^ 2
    physicalGroundEnergy := fun _ => kineticEnergy uniformWave
  } : GroundDensityModel Unit Wave Density) := rfl