spin0_casimir
plain-language theorem explainer
Spin-0 Casimir eigenvalue vanishes under the definition C₂ = j(j + 1). Recognition Science analyses of electroweak symmetry breaking cite this when isolating the potential curvature contribution to the Higgs mass. The term-mode proof applies simplification directly to the casimir definition.
Claim. $C_2(0) = 0$ where $C_2(j) = j(j+1)$ is the Casimir eigenvalue for the spin-$j$ representation of $Q_3$.
background
The Q3Representations module formalizes the quaternion group Q3 as the symmetry group of the eight-tick cycle in Recognition Science. Under SU(2)×U(1) → U(1) breaking the Higgs doublet splits into one physical spin-0 mode and three spin-1 Goldstone modes. The upstream Spin structure from SpinStatistics encodes the quantum number as a non-negative integer via its twice field. The sibling casimir definition returns the standard eigenvalue j(j+1) for natural-number j.
proof idea
The proof is a one-line wrapper that applies the definition of casimir via the simp tactic.
why it matters
This result is invoked by the downstream casimir_ratio_undefined theorem, which states that the spin-1 to spin-0 Casimir ratio is undefined and that the physical mass ratio instead follows from the quartic coupling λ_RS = J''(1)/2 = 1/2. The module documentation ties the construction to the eight-tick octave and the forced J-cost potential curvature rather than representation theory alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.