WordLength
plain-language theorem explainer
WordLength defines a structure that assigns a natural number to each pair consisting of a gauge skeleton and a completion. Researchers computing mass spectra on the phi-ladder would cite this when specifying rung lengths for kernel types. The declaration is a direct structure definition introducing a single mapping field with no proof obligations.
Claim. A structure consisting of a map that sends each gauge skeleton (with hypercharge $Y : ℚ$, color representation flag, and weak doublet status) and completion (with integer shifts $n_Y, n_3, n_2$) to a natural number.
background
The KernelTypes module supplies basic structures for mass kernels. GaugeSkeleton records the gauge quantum numbers of a representation via its hypercharge $Y$ as a rational, a boolean colorRep flag, and a boolean isWeakDoublet indicator. Completion supplies the three integer quantum numbers nY, n3, n2 that complete the representation. The module imports only Mathlib and focuses on type definitions that later support rung specifications.
proof idea
Direct structure definition with no body or tactics. It simply declares the len field as a function GaugeSkeleton → Completion → Nat.
why it matters
This supplies the foundational type for word lengths that will feed into rung specifications and mass formulas on the phi-ladder. No downstream theorems yet reference it, so its precise role in the full mass formula remains open for later closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.