ofMicroMoves_nontrivial
plain-language theorem explainer
The theorem shows that for any list of micro-moves, membership of a pair index in the filtered Finset of pairs with at least one nonzero aggregated coefficient implies that the pair has a nonzero coefficient for some primitive under aggregation. It is invoked inside the ofMicroMoves constructor to discharge the nontrivial field of the resulting NormalForm. The term proof rewrites Finset.mem_filter and projects the existential witness from the membership hypothesis.
Claim. Let $moves$ be a list of micro-moves. Let $S$ be the Finset of pair indices $k$ such that there exists a primitive $p$ with aggregated coefficient $aggCoeff(moves, k, p) ≠ 0$. Then for every $k ∈ S$ there exists a primitive $p$ such that $aggCoeff(moves, k, p) ≠ 0$.
background
The module defines Micro-Move Normal Forms as canonical coefficient tables for DREAM scaffolding. The NormalForm structure packages a Finset of support pairs, a coefficient map from pairs and primitives to reals, a zero_outside axiom, and a nontrivial axiom requiring each supported pair to carry a nonzero coefficient for at least one primitive. The aggCoeff definition sums the coefficients of all micro-moves that match a given pair and primitive. The upstream from theorem in PrimitiveDistinction supplies the seven-axiom foundation that yields the four structural conditions plus definitional facts used here.
proof idea
The term proof introduces the pair and the membership hypothesis, rewrites Finset.mem_filter to expose the conjunction of Finset membership and the existential predicate, then applies exact to the second conjunct, which is exactly the required witness that some primitive has nonzero aggCoeff.
why it matters
The result supplies the nontrivial field required by the ofMicroMoves definition, guaranteeing that every NormalForm constructed from a micro-move list satisfies the full set of structural axioms. It thereby supports the canonical normal-form construction used in the Ethics.Virtues domain for DREAM scaffolding. The parent ofMicroMoves construction depends directly on this lemma to produce well-formed objects consistent with the structural conditions derived from PrimitiveDistinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.