module module high

`IndisputableMonolith.StandardModel.Q3Representations`

Module Q3Representations defines the quaternion group Q₃ and its spin-0 and spin-1 sectors for the Standard Model in Recognition Science. It computes Casimir invariants and supplies the RS Weinberg angle prediction (3-φ)/6. Electroweak modelers and Higgs mass assignments cite these objects. The module consists of direct definitions and algebraic evaluations with no tactic proofs.

claimThe quaternion group is given by the eight elements $Q_3 = {±1, ±i, ±j, ±k}$. Its representations partition into Spin0Sector and Spin1Sector, with Casimir ratio yielding the RS Weinberg angle $sin^2 θ_W = (3-φ)/6$, where φ is the golden-ratio fixed point.

background

Recognition Science models discrete symmetries of the Standard Model via the quaternion group Q₃. The module defines Q3Element as the listed eight elements, Spin0Sector and Spin1Sector as the two representation classes, and evaluates spin0_count, spin1_count, spin0_casimir, spin1_casimir together with their ratio lambda_RS_val. Upstream, the Constants module supplies the base time quantum τ₀ = 1 tick that sets the RS-native scale for all derived quantities.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies sin2ThetaW_RS to the WeinbergAngleScoreCard for direct comparison of the predicted (3-φ)/6 against the observed value ≈0.2229. It also supplies the Q₃ geometry to HiggsRungAssignment for placing the Higgs mass on the φ-ladder. This completes the electroweak parameter table and links the quaternion structure to the self-similar fixed point φ from the forcing chain.

scope and limits

Does not derive the group law or multiplication table for Q₃.
Does not address representations beyond spin 0 and spin 1.
Does not connect directly to the mass formula or Berry threshold.
Does not include numerical verification against PDG data.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.WeinbergAngleScoreCard module_import
IndisputableMonolith.StandardModel.HiggsRungAssignment module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

inductive Q3Element L56
def Spin0Sector L68
def Spin1Sector L71
theorem spin0_count L77
theorem spin1_count L80
theorem q3_order L83
def casimir L88
theorem spin0_casimir L91
theorem spin1_casimir L94
theorem casimir_ratio_undefined L98
def lambda_RS L104
theorem lambda_RS_val L106
def higgsMassSq_over_vev L110
theorem higgsMassSq_simplifies L112
def wMassSq_over_vev L118
def higgsMassRatio L121
def sin2ThetaW_RS L134
theorem sin2ThetaW_RS_val L136
theorem sin2ThetaW_RS_pos L139
theorem sin2ThetaW_RS_lt_half L146
theorem sin2ThetaW_RS_approx L152
def w_rung L163
def higgs_rung_prediction L184
theorem higgs_rung_prediction_pos L191