primitive_mem_order
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness or minimality of the listed order.
- Does not address coefficient values or aggregation rules.
- Does not apply to elements outside the Primitive inductive type.
formal statement (Lean)
31lemma primitive_mem_order (p : Primitive) : p ∈ primitiveOrderList := by
proof body
One-line wrapper that applies cases.
32 cases p <;> simp [primitiveOrderList]
33