`regge_linearity`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.Hadrons
domain: Physics
line: 75 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.Hadrons on GitHub at line 75.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  72  simpa [regge_mass_squared, pdg_regge_slope, mul_comm, mul_left_comm, mul_assoc] using h2
  73
  74/-- Regge trajectory is linear in n. -/
  75theorem regge_linearity (r : ℕ) (n₁ n₂ : ℕ) :
  76    regge_mass_squared r (n₁ + n₂) pdg_regge_slope =
  77    regge_mass_squared r n₁ pdg_regge_slope + regge_mass_squared r n₂ pdg_regge_slope := by
  78  simp [regge_mass_squared]
  79  ring
  80
  81end Physics
  82end IndisputableMonolith

papers checked against this theorem

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