spin0_count
plain-language theorem explainer
The spin-0 sector of the quaternion group Q₃ consists of exactly two elements. Model builders in Recognition Science use this count to fix the Higgs sector cardinality when computing the ratio of Casimir eigenvalues between spin-0 and spin-1 sectors. The proof evaluates the length of the explicit two-element list definition via a decision procedure.
Claim. The spin-0 sector, defined as the set $S = {+1, -1}$, satisfies $|S| = 2$.
background
The module formalizes the quaternion group Q₃ = {±1, ±i, ±j, ±k} as the symmetry group of the 8-tick cycle in Recognition Science. Under electroweak symmetry breaking SU(2)×U(1) → U(1), the Higgs doublet splits into three Goldstone modes (spin-1) and one physical Higgs (spin-0). Spin0Sector is the explicit list [pos_one, neg_one] whose elements generate the scalar sector.
proof idea
One-line wrapper that applies the decide tactic to the length of the list [Q3Element.pos_one, Q3Element.neg_one].
why it matters
This count anchors the spin-0 sector cardinality in the Q₃ representation theory used for electroweak symmetry breaking. It supports derivations of the Higgs mass from the rung offset in the φ-ladder, consistent with the eight-tick octave period of the recognition operator. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.