quantumOpticalCount

formal source

  25  | fock | coherent | squeezed | thermal | entangled
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem quantumOpticalCount : Fintype.card QuantumOpticalState = 5 := by decide
  29
  30/-- Coherent state: J = 0 (classical light limit). -/
  31theorem coherent_state : Jcost 1 = 0 := Jcost_unit0
  32
  33/-- Nonclassical state: J > 0. -/
  34theorem nonclassical_state {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  35    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  36
  37structure QuantumOpticsCert where
  38  five_states : Fintype.card QuantumOpticalState = 5
  39  coherent_zero : Jcost 1 = 0
  40  nonclassical_pos : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  41
  42def quantumOpticsCert : QuantumOpticsCert where
  43  five_states := quantumOpticalCount
  44  coherent_zero := coherent_state
  45  nonclassical_pos := nonclassical_state
  46
  47end IndisputableMonolith.Physics.QuantumOpticsFromRS