module module high

`IndisputableMonolith.Ethics.Virtues.NormalForm`

This module defines the primitive generators for virtues and fixes them in a canonical order for use in normal-form representations. Researchers formalizing ethical structures or virtue aggregation would cite it to ensure consistent ordering of base elements. The module supplies only definitions and elementary list lemmas establishing membership and uniqueness.

claimLet $P$ denote the type of primitive generators. The canonical ordering is the list $L = $ primitiveOrderList such that primitive_mem_order$(p, L)$ holds for every $p : P$, primitiveOrderList_nodup asserts $L$ contains no duplicates, and pairList, rowMoves, toMoves, aggCoeff supply the associated move and coefficient structures.

background

The module sits inside the Ethics.Virtues.NormalForm hierarchy and imports only Mathlib for list and membership primitives. Primitive is introduced as the base type of generators; primitiveOrderList supplies the fixed sequence used by all downstream normal-form constructions. The sibling declarations primitive_mem_order, primitiveOrderList_nodup, MicroMove, NormalForm, pairList, pairList_mem, pairList_nodup, rowMoves, toMoves and aggCoeff together encode the ordered generators, their moves, and the aggregation coefficients required for canonical representation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ordered primitive basis required by any NormalForm construction in the Ethics domain. It therefore feeds directly into theorems that aggregate virtues or reduce ethical expressions to canonical form. No parent theorem is listed in the used_by edges, indicating the module functions as an interface layer whose ordering convention is presupposed by later ethics results.

scope and limits

Does not prove completeness of the primitive set.
Does not define the full virtue theory or its axioms.
Does not contain any aggregation or reduction theorems.
Does not address non-canonical or dynamic orderings.

declarations in this module (31)

inductive Primitive L18
def primitiveOrderList L24
lemma primitive_mem_order L31
lemma primitiveOrderList_nodup L34
structure MicroMove L39
structure NormalForm L47
def pairList L57
lemma pairList_mem L60
lemma pairList_nodup L65
def rowMoves L70
def toMoves L76
def aggCoeff L80
theorem ofMicroMoves_zero_outside L87
theorem ofMicroMoves_nontrivial L110
def ofMicroMoves L118
theorem rowMoves_pair L129
theorem rowMoves_mem_of_coeff_ne_zero L142
theorem aggCoeff_rowMoves_aux_theorem L157
theorem aggCoeff_rowMoves_aux_axiom L319
lemma aggCoeff_rowMoves_aux L329
lemma aggCoeff_rowMoves L340
theorem aggCoeff_rowMoves_of_ne L350
lemma aggCoeff_append L368
theorem aggCoeff_flatMap L375
lemma sumCoeffs_toMoves L405
lemma mem_toMoves_of_coeff_ne_zero L420
lemma pair_mem_toMoves_map L430
theorem of_toMoves L442
theorem pairList_eq_filtered_range_theorem L468
theorem pairList_eq_filtered_range_axiom L500
lemma pairList_eq_filtered_range L505