import PhysicsLogicConsumer.UnitaryInfluence

open PhysicsLogicConsumer.UnitaryInfluence
open PhysicsLogic.Framework.QuantumCommutator PhysicsLogic.Framework.QuantumGroundSector
open scoped Matrix Kronecker

example : Qubit = Fin 2 := rfl
example : Basis = (Qubit × Qubit) := rfl
example : StateSpace = EuclideanSpace Complex Basis := rfl
example : Op = (StateSpace →L[Complex] StateSpace) := rfl
example : toOp = Matrix.toEuclideanCLM (n := Basis) (𝕜 := Complex) := rfl
example : flipMatrix = !![0, 1; 1, 0] := rfl
example : yMatrix = !![0, -Complex.I; Complex.I, 0] := rfl
example : operationMatrix = flipMatrix ⊗ₖ 1 := rfl
example : readoutMatrix = 1 ⊗ₖ yMatrix := rfl
example : hamiltonianMatrix = Matrix.diagonal (fun s : Basis => if s = (1, 1) then 1 else 0) := rfl
example : hamiltonian = toOp hamiltonianMatrix := rfl
example : readout = toOp readoutMatrix := rfl
example (q : Qubit) : inputVector q = WithLp.toLp 2
    (fun s : Basis => if s.1 = q then ((Real.sqrt (1 / 2) : Real) : Complex) else 0) := rfl
example : initial = inputVector 0 := rfl
example : (operation : Op) = toOp operationMatrix := rfl
example : dynamics = hamiltonianTimeEvolution ⟨hamiltonian, hamiltonian_is_selfadjoint⟩ := rfl
example (t : Real) : unitaryMatrix t =
    Matrix.diagonal (fun s : Basis => if s = (1, 1) then Complex.exp (Complex.I * t) else 1) := rfl
example (t : Real) : before t = vectorState initial (evolve dynamics t readout) := rfl
example (t : Real) : after t = vectorState ((operation : Op) initial) (evolve dynamics t readout) := rfl