import PhysicsLogicConsumer.ThermalProbeCompleteness

open PhysicsLogicConsumer.ThermalProbeCompleteness
open PhysicsLogicConsumer.ThermalProbeCompleteness.Calibration
open PhysicsLogic.Philosophy.Measurement
open scoped ComplexOrder

noncomputable section

example (c : Configuration) : c = ⟨c.state, c.detectorGain, c.driveGain⟩ := rfl
example (s : Operator) (g h : Fin 3 → Real) : (Configuration.mk s g h).state = s := rfl
example (s : Operator) (g h : Fin 3 → Real) : (Configuration.mk s g h).detectorGain = g := rfl
example (s : Operator) (g h : Fin 3 → Real) : (Configuration.mk s g h).driveGain = h := rfl
example (c : Configuration) (e : Fin 3) : detector c e = (c.detectorGain e : Complex) • probe e := rfl
example (c : Configuration) (e : Fin 3) : drive c e = (c.driveGain e : Complex) • probe e := rfl
example (c : Configuration) (e : Fin 3) (t : Real) : records c e t =
    ((Matrix.trace (c.state * detector c e * evolved (detector c e) t) +
        Matrix.trace (c.state * evolved (detector c e) t * detector c e)) / 2,
      if t < 0 then 0 else Complex.I *
        (Matrix.trace (c.state * drive c e * evolved (detector c e) t) -
          Matrix.trace (c.state * evolved (detector c e) t * drive c e))) := rfl
example : access = ({
    admissible := fun c => c.state.PosSemidef ∧ Matrix.trace c.state = 1 ∧
      c.state * hamiltonian = hamiltonian * c.state ∧
      (∀ e, 0 < c.detectorGain e) ∧ (∀ e, 0 < c.driveGain e)
    recordAt := fun _ => records
    valueAt := Configuration.state } :
      RecordAccessContext Configuration Unit (Fin 3 → Real → Complex × Complex) Operator) := rfl
example : reference = (⟨density gibbs, fun _ => 1, fun _ => 1⟩ : Configuration) := rfl
example : differentPopulation = ![(27 / 40 : Real), 9 / 40, 3 / 40, 1 / 40] := rfl
example (e : Fin 3) : alternativeGain e = Real.sqrt ((![8 / 9, 4 / 3, 2] : Fin 3 → Real) e) := rfl
example : miscalibrated = (⟨density differentPopulation, alternativeGain,
    fun e => (2 / 3) * alternativeGain e⟩ : Configuration) := rfl

end