stringModeCount

formal source

  25  | tachyonSuppressed | massless | massive | winding | momentum
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem stringModeCount : Fintype.card StringMode = 5 := by decide
  29
  30/-- J ≥ 0 always: tachyon-free condition. -/
  31theorem jcost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ Jcost r := by
  32  by_cases h : r = 1
  33  · rw [h, Jcost_unit0]
  34  · exact le_of_lt (Jcost_pos_of_ne_one r hr h)
  35
  36/-- Massless state: J = 0. -/
  37theorem massless_state : Jcost 1 = 0 := Jcost_unit0
  38
  39structure TachyonFreeCert where
  40  five_modes : Fintype.card StringMode = 5
  41  nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ Jcost r
  42  massless : Jcost 1 = 0
  43
  44def tachyonFreeCert : TachyonFreeCert where
  45  five_modes := stringModeCount
  46  nonneg := jcost_nonneg
  47  massless := massless_state
  48
  49end IndisputableMonolith.Physics.TachyonFreeTachyonFromRS