Torsion8
plain-language theorem explainer
Torsion8 supplies the mod-8 torsion class for ribbon windings in the mass model. Researchers deriving particle generations from recognition costs cite this when labeling quarks and leptons by their winding numbers. The declaration is a direct abbreviation to ZMod 8 with no additional construction.
Claim. The torsion class $T_8$ is the cyclic group of integers modulo 8, written $T_8 := ZMod 8$.
background
The module records a placeholder mass-ribbon construction treated as a narrative scaffold; RS derivations remain non-formalised and the module is categorised as Model. Torsion8 serves as the codomain for the torsion8 function that extracts the winding number of a Word and coerces it into ZMod 8. The upstream via structure from Derivations.MassToLight supplies recognition-weighted stellar assembly as the broader derivation context.
proof idea
Direct abbreviation that names ZMod 8 as Torsion8.
why it matters
This definition supplies the domain for genOfTorsion, which maps the mod-8 value to one of three generation classes g1, g2, g3. It aligns with the eight-tick octave (period 2^3) in the forcing chain and provides the torsion input needed for ribbon-based mass assignments. The module remains scaffolding pending full formalisation of the phi-ladder ribbon machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.