Spin0Sector
plain-language theorem explainer
Spin0Sector enumerates the two elements {+1, -1} of the quaternion group Q3 as the spin-0 sector. Researchers modeling electroweak symmetry breaking via Q3 representations in Recognition Science cite this partition when separating scalar Higgs generators from gauge bosons. The definition is a direct list construction from the Q3Element inductive type.
Claim. The spin-0 sector of the quaternion group $Q_3$ is the list consisting of the positive and negative unit elements, denoted $[+1, -1]$.
background
Q3Element is the inductive type with eight constructors for the quaternion group elements $Q_3 = {+1, -1, +i, -i, +j, -j, +k, -k}$. The module sets up the representation theory of this group as the symmetry of the 8-tick cycle in Recognition Science and its role in electroweak symmetry breaking SU(2)×U(1) → U(1). Under this breaking the four complex degrees of freedom of the Higgs doublet split into three Goldstone modes (longitudinal W± and Z) and one physical spin-0 Higgs boson.
proof idea
Direct definition that constructs the list by enumerating the two constructors Q3Element.pos_one and Q3Element.neg_one. No lemmas or tactics are invoked; the body is a literal list expression.
why it matters
This definition supplies the spin-0 partition required by the downstream theorems spin0_count and q3_order, which verify that the two sectors together exhaust the eight elements of Q3. It supports the module's derivation of Casimir eigenvalues (0 for spin-0, 2 for spin-1) that enter the Higgs-to-W mass ratio via the forced curvature J″(1) = 1 of the J-cost potential. The construction sits inside the eight-tick octave structure (T7) and the φ-ladder mass assignments for the electroweak sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.