import PhysicsLogicConsumer.CondensedMatter.SpatialScreening

open PhysicsLogic.Framework.SpatialCurrentResponse
open PhysicsLogic.Philosophy.SymmetryAndGauge
open PhysicsLogicConsumer.CondensedMatter.SpatialScreening
open PhysicsLogicConsumer.CondensedMatter.SpatialScreening.GaugeValues

example : direction = ![(1 : Real), 1, 0] := rfl
example : kernel = !![(-3 / 2 : Complex), 3 / 2, 0; 3 / 2, -3 / 2, 0; 0, 0, -5] := rfl
example : probe = ![1 + Complex.I, -(1 + Complex.I), 0] := rfl
example : otherProbe = ![0, 0, 2 * Complex.I] := rfl
example : partialKernel = !![(0 : Complex), 0, 0; 0, 0, 0; 0, 0, -5] := rfl
example : magneticAmplitude = fun potential : Amplitude =>
    ![Complex.I * potential 2, -Complex.I * potential 2,
      Complex.I * (potential 1 - potential 0)] := rfl
example (response : Kernel) : representation response =
    ({ represents := fun potential field => magneticAmplitude potential = field
       relatedByRedundancy := fun first second =>
         ∃ gaugeAmplitude : Complex, second = first + gaugeAmplitude • complexWavevector direction
       valueAt := fun _ potential => response.mulVec potential } :
      RepresentationContext Amplitude Amplitude Unit Amplitude) := rfl

example (wavevector : Wavevector) : complexWavevector wavevector =
    fun index => (wavevector index : Complex) := rfl
example (wavevector : Wavevector) (amplitude : Amplitude) : Transverse wavevector amplitude =
    (dotProduct (fun index => (wavevector index : Complex)) amplitude = 0) := rfl
example (response : Kernel) (wavevector : Wavevector) : WardContractionAt response wavevector =
    (response.mulVec (complexWavevector wavevector) = 0) := rfl
example (response : Kernel) (wavevector : Wavevector) : GaugeInvariantAt response wavevector =
    (∀ (potential : Amplitude) (gaugeAmplitude : Complex),
      response.mulVec (potential + gaugeAmplitude • complexWavevector wavevector) =
        response.mulVec potential) := rfl