primitive_mem_order
plain-language theorem explainer
Every constructor of the inductive type Primitive belongs to the explicit list primitiveOrderList. Authors working on micro-move coefficient tables cite the fact when discharging membership obligations inside aggregation lemmas. The proof is a one-line wrapper that performs exhaustive case analysis on Primitive and simplifies against the list definition.
Claim. For every primitive generator $p$, $p$ belongs to the canonical ordered list of the fourteen primitives.
background
The module develops canonical normal forms for micro-move coefficient tables that support DREAM scaffolding. Primitive is the inductive type with fourteen constructors in fixed order: Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice. primitiveOrderList is the definition that materializes this order as the explicit list containing exactly those constructors.
proof idea
The proof is a one-line wrapper that applies case analysis to the inductive type Primitive and then simplifies using the definition of primitiveOrderList.
why it matters
The lemma supplies the membership fact required by aggCoeff_rowMoves and rowMoves_mem_of_coeff_ne_zero when proving that aggregated coefficients match stored table values. It closes the interface between the fixed primitive order and the micro-move construction inside the normal-form development. The surrounding module supports DREAM scaffolding for coefficient tables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.