theorem proved term proof

`D2_no_spinor_structure`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 235theorem D2_no_spinor_structure : ¬HasRSSpinorStructure 2 := by

Term-mode proof.

 236  intro ⟨_, hna, _⟩
 237  norm_num at hna
 238
 239/-- D = 4 does not have RS spinor structure (product Spin(4) ≅ SU(2) × SU(2)). -/

Lean names referenced from this declaration's body.

HasRSSpinorStructure in IndisputableMonolith.Foundation.DimensionForcing decl_use
Spin in IndisputableMonolith.QFT.SpinStatistics decl_use