  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.