Primitive
plain-language theorem explainer
The inductive type Primitive enumerates fourteen fixed virtues in canonical order to serve as generators for micro-move coefficient tables. Workers on normal-form constructions in ethical micro-moves cite this enumeration when defining aggregation functions over move lists. The declaration proceeds by direct inductive introduction of the constructors followed by deriving instances for decidable equality and string representation.
Claim. The type $P$ is defined inductively by the fourteen constructors Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice and carries decidable equality together with a representation instance.
background
In the module on micro-move normal forms, which supplies canonical representations for coefficient tables that support DREAM scaffolding, the primitive generators are listed in fixed order. This enumeration draws on the reduced-word structure from SectorPrimitive, where a Primitive consists of a word together with a proof that it equals its normal form. It also connects to the Laplacian identification in the continuum bridge, equating a weighted sum of squared differences to a scaled sum over defects.
proof idea
The declaration is a direct inductive definition introducing the fourteen constructors with no additional proof obligations. The deriving clauses for DecidableEq and Repr are supplied automatically by the Lean typeclass mechanism.
why it matters
This enumeration anchors the NormalForm construction in the Ethics.Virtues.NormalForm module, where it is used to index the coefficient tables via functions such as aggCoeff and rowMoves. It supplies the primitive labels that appear in downstream lemmas establishing that aggregation over row moves recovers the stored coefficients, and it appears in the Centering inductive for Bravais lattices via the primitive (P) case. Within the broader framework the fixed order supports the canonical normal forms required for DREAM scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.