import PhysicsLogicConsumer.StatePositivity

open PhysicsLogicConsumer.StatePositivity

example : PhysicsLogicConsumer.StatePositivity.Algebra = (Complex × Complex) := rfl
example : distorted.expectation =
    (1 / 2 + Complex.I) • ContinuousLinearMap.fst Complex Complex Complex +
      (1 / 2 - Complex.I) • ContinuousLinearMap.snd Complex Complex Complex := rfl
example : distorted.groundTerm = 0 := rfl
example : mixture.expectation =
    (1 / 2 : Complex) • ContinuousLinearMap.fst Complex Complex Complex +
      (1 / 2 : Complex) • ContinuousLinearMap.snd Complex Complex Complex := rfl
example : mixture.groundTerm = 0 := rfl
example : yes = (1, 0) := rfl