GaugeSkeleton
plain-language theorem explainer
GaugeSkeleton packages the minimal gauge quantum numbers required for kernel-based mass calculations. It records hypercharge as a rational, plus boolean flags for color representation and weak doublet status. Mass formula work in Recognition Science cites this when classifying representations on the phi-ladder. The declaration is a bare structure definition with three fields and no proof obligations.
Claim. A gauge skeleton is a triple $(Y, c, w)$ with $Y : ℚ$, $c : Bool$ marking color representation, and $w : Bool$ marking weak-isospin doublet structure.
background
In the Masses.KernelTypes module the structure supplies the gauge data carrier for subsequent length and mass computations. The field Y stores hypercharge in rational units, colorRep is a boolean flag for color charge, and isWeakDoublet marks SU(2) doublet membership. The module imports only Mathlib; the structure is consumed directly by the downstream WordLength definition that maps a gauge skeleton and a completion to a natural-number length.
proof idea
The declaration is a structure definition that introduces three fields with no lemmas, tactics, or computational reduction.
why it matters
GaugeSkeleton supplies the gauge input consumed by WordLength, which in turn supports rung and gap calculations on the phi-ladder mass formula. It therefore participates in the T8 step that fixes three spatial dimensions and the overall forcing chain from T0 to T8. No open scaffolding is attached to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.