Spin1Sector
plain-language theorem explainer
Spin1Sector enumerates the six non-real elements of the quaternion group Q3 as the list {+i, -i, +j, -j, +k, -k}. Electroweak model builders cite it when mapping the gauge-boson degrees of freedom that arise from the eight-tick cycle symmetry. The definition is a direct list construction drawn from the Q3Element inductive type.
Claim. Let $S_1 = [+i, -i, +j, -j, +k, -k]$ denote the spin-1 sector of the quaternion group $Q_3 = {±1, ±i, ±j, ±k}$.
background
The module formalizes the representation theory of the quaternion group Q3, which Recognition Science identifies as the symmetry group of the fundamental 8-tick cycle. Under SU(2)×U(1) → U(1) breaking the four complex degrees of freedom of the Higgs doublet split into three longitudinal modes of the W± and Z bosons (spin-1 sector) and one physical Higgs (spin-0 sector). The module doc states that the mass ratio m_H / m_W follows from the ratio of Casimir eigenvalues of these two sectors together with the forced curvature J″(1) = 1.
proof idea
One-line definition by explicit enumeration of the six imaginary units supplied by the Q3Element inductive type, excluding the two real elements that form the spin-0 sector.
why it matters
Spin1Sector supplies the gauge-boson content required by the downstream theorems spin1_count (length equals 6) and q3_order (total order 8). It realizes the T7 eight-tick octave inside the Standard Model sector and supplies the three imaginary directions that become the longitudinal polarizations of W± and Z. The module doc links the construction directly to the φ-ladder mass law and the EW geometry that fixes the Weinberg angle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.