Q3Element
plain-language theorem explainer
The inductive definition enumerates the eight elements of the quaternion group Q₃ as ±1, ±i, ±j, ±k. Researchers modeling electroweak symmetry breaking in Recognition Science cite it when separating the Higgs generators from the gauge boson directions. It is realized as a direct inductive type declaration that derives decidable equality with no further proof obligations.
Claim. Let $Q_3$ be the quaternion group whose eight elements are $+1$, $-1$, $+i$, $-i$, $+j$, $-j$, $+k$, $-k$.
background
In the Recognition Science treatment of the electroweak sector, the quaternion group Q₃ serves as the symmetry group of the eight-tick cycle that underlies the fundamental period of the recognition operator. The module partitions its elements into a spin-0 sector consisting of ±1, which generate the Higgs field, and a spin-1 sector consisting of ±i, ±j, ±k, which correspond to the longitudinal modes of the W and Z bosons. This separation determines the distinct Casimir eigenvalues that enter the mass ratio between the physical Higgs and the gauge bosons after symmetry breaking.
proof idea
The declaration is a direct inductive definition that lists the eight constructors corresponding to the group elements, together with the deriving clause for decidable equality and representation.
why it matters
This definition supplies the carrier set for Spin0Sector and Spin1Sector, which partition the elements into the Higgs generators {+1, -1} and the gauge directions {±i, ±j, ±k}. It thereby anchors the computation of Casimir eigenvalues used to fix the Higgs mass relative to the W boson within the Recognition Science framework. The construction realizes the eight-tick octave symmetry required by the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.