spin1_casimir
plain-language theorem explainer
The declaration establishes that the quadratic Casimir eigenvalue for the spin-1 irreducible representation of the quaternion group Q3 equals 2. Particle physicists deriving electroweak boson masses on the phi-ladder cite this when separating the three longitudinal modes of W and Z from the physical Higgs. The proof is a one-line term wrapper that unfolds the casimir definition and normalizes the resulting integer.
Claim. The quadratic Casimir eigenvalue satisfies $C_2(1) = 2$ for the spin-1 sector of the quaternion group $Q_3$.
background
The module formalizes Q3 representations for the 8-tick cycle that appears as the fundamental period of the recognition operator. Under SU(2) x U(1) to U(1) breaking the Higgs doublet yields three spin-1 Goldstone modes eaten by the gauge bosons and one spin-0 physical Higgs; the casimir function returns the eigenvalue of the quadratic Casimir operator on these sectors. Upstream results supply the underlying distinction axioms and forcing structures that embed Q3 into the Recognition Science symmetry group.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the casimir definition to expose the explicit representation-theoretic formula for j=1 and applies norm_num to obtain the integer 2.
why it matters
This supplies the spin-1 Casimir value required for the mass-ratio discussion in the Q3 sector. It sits inside the eight-tick octave structure (T7) and the Q3 symmetry of the fundamental period. The module documentation notes that the physical Higgs mass offset arises from potential curvature J''(1) rather than from the Casimir ratio itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.