MicroMove
MicroMove records a natural-number pair index, one of fourteen fixed primitive virtues, and a real coefficient as the atomic unit for ethical coefficient tables. Workers building normal forms for DREAM scaffolding cite this record when assembling move lists that feed aggregation functions. The declaration is a direct three-field structure with no proof obligations.
claimA micro-move is a triple $(n, p, c)$ where $n$ is a pair index in the naturals, $p$ is a primitive generator drawn from the ordered list of virtues, and $c$ is a real coefficient.
background
The module introduces micro-move normal forms as the canonical representation for coefficient tables supporting DREAM scaffolding. Primitive is the inductive type that enumerates fourteen virtues in fixed canonical order: Love, Justice, Forgiveness, Wisdom, Courage, Temperance, Prudence, Compassion, Gratitude, Patience, Humility, Hope, Creativity, Sacrifice. The coeff field draws on the gap-series definition from Pipelines, which computes dimensionless coefficients via the series for log(1+x) evaluated at z/φ.
proof idea
The declaration is a direct structure definition that introduces the three fields pair, primitive, and coeff with no lemmas or tactics applied.
why it matters in Recognition Science
MicroMove supplies the atomic elements for ofMicroMoves, which builds NormalForm instances by aggregating coefficients over move lists via aggCoeff. It fills the interface between primitive generators and finite-support tables in the Ethics domain, enabling downstream results such as aggCoeff_append and the zero-outside property. The structure closes the construction path for canonical normal forms under DREAM scaffolding.
scope and limits
- Does not compute or constrain coefficient values.
- Does not restrict pair indices to any bounded range.
- Does not enforce nonzero coefficients or finite support.
- Does not connect to physical constants or spatial dimensions.
Lean usage
def sample : List MicroMove := [{pair := 0, primitive := Primitive.Love, coeff := 1}]formal statement (Lean)
39structure MicroMove where
40 pair : ℕ
41 primitive : Primitive
42 coeff : ℝ
43
44namespace MicroMove
45
46/-- Canonical micro-move normal form: coefficient table with finite support. -/