NormalForm
plain-language theorem explainer
NormalForm encodes the canonical finite-support coefficient table for micro-moves over the ordered list of primitives. Researchers formalizing virtue aggregation or DREAM scaffolding cite the structure when they need a unique normal form for coefficient tables. The declaration is a direct structure with four fields that enforce zero coefficients outside the support and nontriviality inside it.
Claim. A normal form consists of a finite set $Ssubseteqmathbb{N}$ of supported pairs together with a map $c:mathbb{N}tomathcal{P}tomathbb{R}$, where $mathcal{P}$ is the set of primitive virtues, such that $c(p,pi)=0$ for all $pnotin S$ and for every $p in S$ there exists $pi$ with $c(p,pi)neq0$.
background
Primitive is the inductive type that enumerates the fourteen canonical virtues in fixed order: Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice. The module defines micro-move normal forms as the standard representation for coefficient tables that support DREAM scaffolding. Upstream structures such as LedgerFactorization.of and PhiForcingDerived.of supply the J-cost calibration context, while SpectralEmergence.of fixes the gauge and generation content that the underlying physics respects.
proof idea
Direct structure definition. The four fields are introduced without computational reduction, tactic steps, or auxiliary lemmas.
why it matters
NormalForm is the parent type for the aggregation machinery in this module, including aggCoeff, aggCoeff_rowMoves, and the row-moves auxiliary theorems. It supplies the canonical representation required by DREAM scaffolding, ensuring every list of micro-moves collapses to a unique finite-support table that satisfies the zero-outside and nontriviality conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.