Primitive
plain-language theorem explainer
A sector primitive packages a ribbon word together with the witness that it is already fixed by normalization. Modelers of mass ladders via ribbon reductions cite this record when building canonical elements for aggregation. The declaration is a bare structure definition with two fields and no computational body.
Claim. A primitive consists of a ribbon word $w$ together with a proof that the normalization map satisfies $normalForm(w)=w$.
background
In the SectorPrimitive module this structure acts as a placeholder record for normalized ribbon words that populate mass ladders. A Word is an abbreviation for List Ribbon, a sequence of ribbon syllables. The normalForm operation performs at most length-many bounded rewrite passes, returning the input unchanged once no further length reduction is possible. The upstream Ethics.Virtues.NormalForm.Primitive supplies an unrelated inductive list of canonical generators (Love, Justice, etc.), while the ribbon normalization here is drawn directly from Ribbons.normalForm and Ribbons.Word.
proof idea
The declaration is a structure definition. It introduces the type by naming the two fields word and reduced; no lemmas, tactics, or reductions are invoked.
why it matters
The structure supplies the basic datum consumed by aggregation routines such as aggCoeff, aggCoeff_rowMoves, and aggCoeff_flatMap inside Ethics.Virtues.NormalForm. It is also referenced by CrystalSymmetry.Centering when distinguishing primitive lattice types. Within the Recognition framework it provides the witness records needed for ribbon-based mass ladders that ultimately feed the phi-ladder mass formula; the module documentation explicitly labels it a documentation-only placeholder, leaving open the concrete mapping from normalized words to physical masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.