`spin0_count`

proved

show as: view math explainer →

module: IndisputableMonolith.StandardModel.Q3Representations
domain: StandardModel
line: 77 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.Q3Representations on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  74   Q3Element.pos_k, Q3Element.neg_k]
  75
  76/-- The spin-0 sector has 2 elements. -/
  77theorem spin0_count : Spin0Sector.length = 2 := by decide
  78
  79/-- The spin-1 sector has 6 elements. -/
  80theorem spin1_count : Spin1Sector.length = 6 := by decide
  81
  82/-- Q₃ has 8 elements total. -/
  83theorem q3_order : Spin0Sector.length + Spin1Sector.length = 8 := by decide
  84
  85/-! ## Casimir Eigenvalues -/
  86
  87/-- Casimir eigenvalue for spin-j representation: C₂ = j(j+1). -/
  88noncomputable def casimir (j : ℕ) : ℝ := (j : ℝ) * ((j : ℝ) + 1)
  89
  90/-- Spin-0 Casimir eigenvalue: j=0, C₂ = 0. -/
  91theorem spin0_casimir : casimir 0 = 0 := by simp [casimir]
  92
  93/-- Spin-1 Casimir eigenvalue: j=1, C₂ = 2. -/
  94theorem spin1_casimir : casimir 1 = 2 := by unfold casimir; norm_num
  95
  96/-- Casimir eigenvalue ratio (spin-1 to spin-0) is undefined (C₂=0 for spin-0).
  97    The mass ratio comes from the POTENTIAL curvature, not the Casimir directly. -/
  98theorem casimir_ratio_undefined : casimir 0 = 0 := spin0_casimir
  99
 100/-! ## The Correct Mass Ratio Derivation -/
 101
 102/-- The φ-forced quartic coupling: λ = J″(1)/2 = 1/2.
 103    J(x) = ½(x + x⁻¹) - 1 → J″(1) = 1 → λ_RS = J″(1)/2 = 1/2. -/
 104noncomputable def lambda_RS : ℝ := 1 / 2
 105
 106theorem lambda_RS_val : lambda_RS = 1 / 2 := rfl
 107

papers checked against this theorem

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