import PhysicsLogicConsumer.ThermalProbeCompleteness

open PhysicsLogicConsumer.ThermalProbeCompleteness
open PhysicsLogic.Framework.ThermalTransitionSpectrum
open PhysicsLogic.Philosophy.Measurement
open MeasureTheory
open scoped ComplexOrder

noncomputable section

example : Level = Fin 4 := rfl
example : Population = (Fin 4 → Real) := rfl
example : Operator = Matrix (Fin 4) (Fin 4) Complex := rfl
example (i : Fin 4) : energy i = (i.val : Real) * Real.log 2 := rfl
example : ensemble = ({
  State := Fin 4
  stateMeasurable := ⊤
  stateMeasure := Measure.count
  energy := energy
  inverseTemperature := 1 } : CanonicalEnsemble) := rfl
example : gibbs = ![(8 / 15 : Real), 4 / 15, 2 / 15, 1 / 15] := rfl
example : alternative = ![(8 / 15 : Real), 4 / 15, 1 / 10, 1 / 10] := rfl
example (p : Population) : Admissible p ↔ (∀ i, 0 ≤ p i) ∧ ∑ i, p i = 1 := Iff.rfl
example (p : Population) : density p = Matrix.diagonal (fun i => (p i : Complex)) := rfl
example : hamiltonian = Matrix.diagonal (fun i => (energy i : Complex)) := rfl
example (t : Real) : propagator t =
    Matrix.diagonal (fun i => Complex.exp (-Complex.I * (energy i * t : Real))) := rfl
example (a : Operator) (t : Real) : evolved a t = propagator (-t) * a * propagator t := rfl
example (e : Fin 3) : lower e = (⟨e.val, Nat.lt_trans e.isLt (by decide)⟩ : Fin 4) := rfl
example (e : Fin 3) : upper e = e.succ := rfl
example (e : Fin 3) (i j : Fin 4) : probe e i j =
    if (i = lower e ∧ j = upper e) ∨ (i = upper e ∧ j = lower e) then 1 else 0 := rfl
example (p : Population) (e : Fin 3) (t : Real) : ordered p e t =
    Matrix.trace (density p * probe e * evolved (probe e) t) := rfl
example (p : Population) (e : Fin 3) (t : Real) : reverseOrdered p e t =
    Matrix.trace (density p * evolved (probe e) t * probe e) := rfl
example (p : Population) (e : Fin 3) (t : Real) : noise p e t =
    (ordered p e t + reverseOrdered p e t) / 2 := rfl
example (p : Population) (e : Fin 3) (t : Real) : response p e t =
    if t < 0 then 0 else Complex.I * (ordered p e t - reverseOrdered p e t) := rfl
example (p : Population) (e : Fin 3) : forwardLine p e =
    p (lower e) * Complex.normSq (probe e (lower e) (upper e)) := rfl
example (p : Population) (e : Fin 3) : backwardLine p e =
    p (upper e) * Complex.normSq (probe e (upper e) (lower e)) := rfl
example (p : Population) (e : Fin 3) : Balanced p e ↔
    backwardLine p e = (1 / 2) * forwardLine p e := Iff.rfl
example : recordAccess = ({
  admissible := Admissible
  recordAt := fun _ p t => (noise p 0 t, response p 0 t)
  valueAt := id } : RecordAccessContext Population Unit (Real → Complex × Complex) Population) := rfl
example : thermalSlice = ({
  ensemble := ensemble
  Transition := Unit
  transitionMeasurable := ⊤
  transitionMeasure := Measure.count
  initial := fun _ => 0
  final := fun _ => 1
  firstOperator := probe 0
  secondOperator := probe 0 } : TransitionSlice) := rfl

example : coherent = density gibbs + Matrix.single (0 : Level) 2 (1 / 30 : Complex) +
    Matrix.single 2 0 (1 / 30) := rfl
example (s : Operator) (e : Fin 3) (t : Real) : stateOrdered s e t =
    Matrix.trace (s * probe e * evolved (probe e) t) := rfl
example (s : Operator) (e : Fin 3) (t : Real) : stateReverseOrdered s e t =
    Matrix.trace (s * evolved (probe e) t * probe e) := rfl
example : fullProbeAccess = ({
  admissible := fun s => s.PosSemidef ∧ Matrix.trace s = 1
  recordAt := fun _ s e t =>
    ((stateOrdered s e t + stateReverseOrdered s e t) / 2,
      if t < 0 then 0 else Complex.I * (stateOrdered s e t - stateReverseOrdered s e t))
  valueAt := id } : RecordAccessContext Operator Unit (Fin 3 → Real → Complex × Complex) Operator) := rfl

end