def
definition
halfInt
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.SpinStatistics on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
58def ofInt (n : ℕ) : Spin := ⟨2 * n, by omega⟩
59
60/-- Create a half-integer spin (s = n/2). -/
61def halfInt (n : ℕ) : Spin := ⟨n, by omega⟩
62
63/-- Spin 0. -/
64def zero : Spin := ofInt 0
65
66/-- Spin 1/2 (electron, quarks). -/
67def half : Spin := halfInt 1
68
69/-- Spin 1 (photon, W/Z, gluon). -/
70def one : Spin := ofInt 1
71
72/-- Spin 3/2 (hypothetical gravitino). -/
73def threeHalves : Spin := halfInt 3
74
75/-- Spin 2 (graviton). -/
76def two : Spin := ofInt 2
77
78/-- The actual spin value as a real number. -/
79noncomputable def value (s : Spin) : ℝ := s.twice / 2
80
81/-- Is this a half-integer spin (fermion)? -/
82def isHalfInteger (s : Spin) : Prop := s.twice % 2 = 1
83
84/-- Is this an integer spin (boson)? -/
85def isInteger (s : Spin) : Prop := s.twice % 2 = 0
86
87/-- Decidable instance for half-integer check. -/
88instance : DecidablePred isHalfInteger := fun s =>
89 if h : s.twice % 2 = 1 then isTrue h else isFalse h
90
91/-- Decidable instance for integer check. -/