IndisputableMonolith.Ethics.Virtues.NormalForm
IndisputableMonolith/Ethics/Virtues/NormalForm.lean · 517 lines · 31 declarations
show as:
view math explainer →
1import Mathlib
2
3/-!
4# Micro-Move Normal Forms
5
6Canonical normal form for micro-move coefficient tables supporting DREAM scaffolding.
7-/
8
9namespace IndisputableMonolith
10namespace Ethics
11namespace Virtues
12
13open scoped Classical BigOperators
14
15open Finset
16
17/-- Primitive generators in fixed canonical order. -/
18inductive Primitive
19 | Love | Justice | Forgiveness | Wisdom | Courage | Temperance | Prudence
20 | Compassion | Gratitude | Patience | Humility | Hope | Creativity | Sacrifice
21 deriving DecidableEq, Repr
22
23/-- Canonical primitive order as a list. -/
24def primitiveOrderList : List Primitive :=
25 [ Primitive.Love, Primitive.Justice, Primitive.Forgiveness,
26 Primitive.Wisdom, Primitive.Courage, Primitive.Temperance,
27 Primitive.Prudence, Primitive.Compassion, Primitive.Gratitude,
28 Primitive.Patience, Primitive.Humility, Primitive.Hope,
29 Primitive.Creativity, Primitive.Sacrifice ]
30
31lemma primitive_mem_order (p : Primitive) : p ∈ primitiveOrderList := by
32 cases p <;> simp [primitiveOrderList]
33
34lemma primitiveOrderList_nodup : primitiveOrderList.Nodup := by
35 unfold primitiveOrderList
36 decide
37
38/-- Micro moves: (pair scope, primitive, coefficient). -/
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. -/
47@[ext]
48structure NormalForm where
49 supportPairs : Finset ℕ
50 coeff : ℕ → Primitive → ℝ
51 zero_outside : ∀ {pair prim}, pair ∉ supportPairs → coeff pair prim = 0
52 nontrivial : ∀ {pair}, pair ∈ supportPairs → ∃ prim, coeff pair prim ≠ 0
53
54namespace NormalForm
55
56/-- Canonical ordered list of supported pairs (ascending). -/
57noncomputable def pairList (nf : NormalForm) : List ℕ :=
58 nf.supportPairs.sort (· ≤ ·)
59
60lemma pairList_mem {nf : NormalForm} {pair : ℕ} :
61 pair ∈ pairList nf ↔ pair ∈ nf.supportPairs := by
62 unfold pairList
63 simp only [mem_sort]
64
65lemma pairList_nodup (nf : NormalForm) : (pairList nf).Nodup := by
66 unfold pairList
67 simp only [sort_nodup]
68
69/-- Micro-moves for a single pair. -/
70noncomputable def rowMoves (nf : NormalForm) (pair : ℕ) : List MicroMove :=
71 primitiveOrderList.filterMap (fun prim =>
72 if nf.coeff pair prim = 0 then none
73 else some ⟨pair, prim, nf.coeff pair prim⟩)
74
75/-- Canonical ordered list of micro-moves. -/
76noncomputable def toMoves (nf : NormalForm) : List MicroMove :=
77 (pairList nf).flatMap (rowMoves nf)
78
79/-- Aggregate coefficient for `(pair, primitive)` extracted from a move list. -/
80noncomputable def aggCoeff (moves : List MicroMove) (pair : ℕ) (prim : Primitive) : ℝ :=
81 ((moves.filter fun m => m.pair = pair ∧ m.primitive = prim).map (·.coeff)).sum
82
83/-- **NormalForm construction**: The ofMicroMoves construction is well-formed.
84
85Proof by contraposition: if aggCoeff is nonzero, pair must be in the filtered set.
86-/
87theorem ofMicroMoves_zero_outside (moves : List MicroMove) :
88 ∀ {pair prim}, pair ∉ (moves.map (·.pair)).toFinset.filter (fun k =>
89 ∃ prim, aggCoeff moves k prim ≠ 0) → aggCoeff moves pair prim = 0 := by
90 intro pair prim h_not_mem
91 by_contra h_ne
92 apply h_not_mem
93 rw [Finset.mem_filter, List.mem_toFinset]
94 constructor
95 · -- Show pair ∈ moves.map (·.pair)
96 -- If aggCoeff ≠ 0, there's a move with matching pair and prim
97 have h_filter_ne : (moves.filter fun m => m.pair = pair ∧ m.primitive = prim) ≠ [] := by
98 intro h_empty
99 unfold aggCoeff at h_ne
100 rw [h_empty] at h_ne
101 simp at h_ne
102 obtain ⟨m, hm⟩ := List.exists_mem_of_ne_nil _ h_filter_ne
103 rw [List.mem_filter] at hm
104 simp only [decide_eq_true_eq] at hm
105 rw [List.mem_map]
106 exact ⟨m, hm.1, hm.2.1⟩
107 · -- Show ∃ prim', aggCoeff moves pair prim' ≠ 0
108 exact ⟨prim, h_ne⟩
109
110theorem ofMicroMoves_nontrivial (moves : List MicroMove) :
111 ∀ {pair}, pair ∈ (moves.map (·.pair)).toFinset.filter (fun k =>
112 ∃ prim, aggCoeff moves k prim ≠ 0) → ∃ prim, aggCoeff moves pair prim ≠ 0 := by
113 intro pair h_mem
114 rw [Finset.mem_filter] at h_mem
115 exact h_mem.2
116
117/-- Build NormalForm from a move list (aggregates coefficients). -/
118noncomputable def ofMicroMoves (moves : List MicroMove) : NormalForm where
119 supportPairs := (moves.map (·.pair)).toFinset.filter (fun k =>
120 ∃ prim, aggCoeff moves k prim ≠ 0)
121 coeff := aggCoeff moves
122 zero_outside := ofMicroMoves_zero_outside moves
123 nontrivial := ofMicroMoves_nontrivial moves
124
125/-- Every micro-move generated for `pair` stays within that pair scope.
126
127Proof: rowMoves constructs MicroMove.mk with pair as first argument,
128so any move in the list has m.pair = pair by construction. -/
129theorem rowMoves_pair {nf : NormalForm} {pair : ℕ} {m : MicroMove}
130 (hm : m ∈ rowMoves nf pair) : m.pair = pair := by
131 classical
132 unfold rowMoves at hm
133 simp only [List.mem_filterMap] at hm
134 obtain ⟨prim, _, heq⟩ := hm
135 by_cases h : nf.coeff pair prim = 0 <;> simp only [h, ite_true, ite_false] at heq
136 · cases heq
137 · cases heq; rfl
138
139/-- If a coefficient is non-zero, the corresponding micro-move appears in the row.
140
141Proof: rowMoves uses filterMap which includes moves for non-zero coefficients. -/
142theorem rowMoves_mem_of_coeff_ne_zero {nf : NormalForm} {pair : ℕ} {prim : Primitive}
143 (hcoeff : nf.coeff pair prim ≠ 0) :
144 ⟨pair, prim, nf.coeff pair prim⟩ ∈ rowMoves nf pair := by
145 classical
146 unfold rowMoves
147 simp only [List.mem_filterMap]
148 use prim, primitive_mem_order prim
149 simp only [hcoeff, ite_false]
150
151/-- Auxiliary lemma: sum over a primitive list.
152
153This proof involves complex list manipulations with filterMap and filter.
154The proof strategy:
155- If coeff = 0: the filterMap excludes this primitive, so sum = 0
156- If coeff ≠ 0: exactly one move matches, contributing the coefficient -/
157theorem aggCoeff_rowMoves_aux_theorem
158 (nf : NormalForm) (pair : ℕ) (prim : Primitive) :
159 (((primitiveOrderList.filterMap fun q =>
160 if nf.coeff pair q = 0 then none
161 else some (MicroMove.mk pair q (nf.coeff pair q))).filter
162 (fun m => m.pair = pair ∧ m.primitive = prim)).map
163 (·.coeff)).sum
164 = if prim ∈ primitiveOrderList then nf.coeff pair prim else 0 := by
165 -- Since all primitives are in primitiveOrderList, the else branch is never reached
166 have hmem : prim ∈ primitiveOrderList := primitive_mem_order prim
167 simp only [hmem, ite_true]
168 -- Let moves = filterMap result
169 set moves := primitiveOrderList.filterMap fun q =>
170 if nf.coeff pair q = 0 then none
171 else some (MicroMove.mk pair q (nf.coeff pair q)) with hmoves_def
172 -- All moves in `moves` have m.pair = pair (by construction)
173 have h_all_pair : ∀ m ∈ moves, m.pair = pair := by
174 intro m hm
175 simp only [hmoves_def, List.mem_filterMap] at hm
176 obtain ⟨q, _, h_some⟩ := hm
177 by_cases hcoeff : nf.coeff pair q = 0
178 · simp [hcoeff] at h_some
179 · simp only [hcoeff, ite_false, Option.some.injEq] at h_some
180 rw [← h_some]
181 -- The filter condition `m.pair = pair ∧ m.primitive = prim` simplifies to `m.primitive = prim`
182 have h_filter_eq : moves.filter (fun m => m.pair = pair ∧ m.primitive = prim) =
183 moves.filter (fun m => m.primitive = prim) := by
184 apply List.filter_congr
185 intro m hm
186 simp only [decide_eq_decide]
187 constructor
188 · intro ⟨_, hp⟩; exact hp
189 · intro hp; exact ⟨h_all_pair m hm, hp⟩
190 rw [h_filter_eq]
191 -- Now we need to show the sum of coeffs for moves with primitive = prim equals nf.coeff pair prim
192 -- Case split on whether coeff is zero
193 by_cases hcoeff : nf.coeff pair prim = 0
194 · -- If coeff = 0, no move for prim was created, so filter is empty
195 have h_prim_not_in : ∀ m ∈ moves, m.primitive ≠ prim := by
196 intro m hm
197 simp only [hmoves_def, List.mem_filterMap] at hm
198 obtain ⟨q, _, h_some⟩ := hm
199 by_cases hq : nf.coeff pair q = 0
200 · simp [hq] at h_some
201 · simp only [hq, ite_false, Option.some.injEq] at h_some
202 rw [← h_some]
203 intro h_eq
204 simp at h_eq
205 rw [h_eq] at hq
206 exact hq hcoeff
207 have h_filter_nil : moves.filter (fun m => m.primitive = prim) = [] := by
208 rw [List.filter_eq_nil_iff]
209 intro m hm
210 simp only [decide_eq_true_eq]
211 exact h_prim_not_in m hm
212 simp [h_filter_nil, hcoeff]
213 · -- If coeff ≠ 0, exactly one move with primitive = prim was created
214 have h_prim_in_moves : ⟨pair, prim, nf.coeff pair prim⟩ ∈ moves := by
215 simp only [hmoves_def, List.mem_filterMap]
216 use prim, hmem
217 simp [hcoeff]
218 -- Show the filtered list is exactly this one element
219 have h_unique : ∀ m ∈ moves, m.primitive = prim → m = ⟨pair, prim, nf.coeff pair prim⟩ := by
220 intro m hm h_prim_eq
221 simp only [hmoves_def, List.mem_filterMap] at hm
222 obtain ⟨q, _, h_some⟩ := hm
223 by_cases hq : nf.coeff pair q = 0
224 · simp [hq] at h_some
225 · simp only [hq, ite_false, Option.some.injEq] at h_some
226 rw [← h_some] at h_prim_eq ⊢
227 simp at h_prim_eq
228 subst h_prim_eq
229 rfl
230 -- The filtered list equals [target] because target is the unique element matching the predicate
231 have h_filter_singleton : moves.filter (fun m => m.primitive = prim) =
232 [⟨pair, prim, nf.coeff pair prim⟩] := by
233 -- Show all elements in the filtered list equal the target
234 have h_all_eq : ∀ m ∈ moves.filter (fun m => m.primitive = prim),
235 m = ⟨pair, prim, nf.coeff pair prim⟩ := by
236 intro m hm
237 rw [List.mem_filter] at hm
238 simp only [decide_eq_true_eq] at hm
239 exact h_unique m hm.1 hm.2
240 -- The filtered list is nonempty (contains target)
241 have h_mem_filter : ⟨pair, prim, nf.coeff pair prim⟩ ∈ moves.filter (fun m => m.primitive = prim) := by
242 rw [List.mem_filter]
243 exact ⟨h_prim_in_moves, by simp⟩
244 -- Any element in the list equals target, so list is either [] or [target]
245 -- Since target ∈ list, it must be [target]
246 cases hfilt : moves.filter (fun m => m.primitive = prim) with
247 | nil =>
248 exfalso
249 rw [hfilt] at h_mem_filter
250 simp at h_mem_filter
251 | cons head tail =>
252 -- head = target by h_all_eq
253 have h_head_eq : head = ⟨pair, prim, nf.coeff pair prim⟩ := by
254 apply h_all_eq
255 rw [hfilt]
256 simp
257 -- tail = [] because any element in tail would also equal target,
258 -- meaning target appears twice in a nodup list
259 have h_tail_nil : tail = [] := by
260 by_contra h_tail_ne
261 obtain ⟨x, rest, h_tail_eq⟩ := List.exists_cons_of_ne_nil h_tail_ne
262 have h_x_mem : x ∈ moves.filter (fun m => m.primitive = prim) := by
263 rw [hfilt, h_tail_eq]
264 simp
265 have h_x_eq : x = ⟨pair, prim, nf.coeff pair prim⟩ := h_all_eq x h_x_mem
266 -- Now head = x = target, so we have duplicate in filtered list
267 have h_moves_prim_unique : ∀ a b, a ∈ moves → b ∈ moves → a.primitive = b.primitive → a = b := by
268 intro a b ha hb h_prim_eq
269 simp only [hmoves_def, List.mem_filterMap] at ha hb
270 obtain ⟨pa, _, ha_some⟩ := ha
271 obtain ⟨pb, _, hb_some⟩ := hb
272 by_cases hpa : nf.coeff pair pa = 0 <;> simp [hpa] at ha_some
273 by_cases hpb : nf.coeff pair pb = 0 <;> simp [hpb] at hb_some
274 rw [← ha_some, ← hb_some] at h_prim_eq ⊢
275 simp at h_prim_eq
276 subst h_prim_eq
277 rfl
278 -- head and x are both in moves with same primitive, so head = x
279 have h_head_in : head ∈ moves := by
280 have : head ∈ moves.filter (fun m => m.primitive = prim) := by rw [hfilt]; simp
281 rw [List.mem_filter] at this
282 exact this.1
283 have h_x_in : x ∈ moves := by
284 rw [List.mem_filter] at h_x_mem
285 exact h_x_mem.1
286 have h_head_prim : head.primitive = prim := by
287 have : head ∈ moves.filter (fun m => m.primitive = prim) := by rw [hfilt]; simp
288 rw [List.mem_filter] at this
289 simp only [decide_eq_true_eq] at this
290 exact this.2
291 have h_x_prim_eq_val_p : x.primitive = prim := by
292 rw [List.mem_filter] at h_x_mem
293 simp only [decide_eq_true_eq] at h_x_mem
294 exact h_x_mem.2
295 have h_head_x_eq : head = x := h_moves_prim_unique head x h_head_in h_x_in (by rw [h_head_prim, h_x_prim_eq_val_p])
296 -- Filter of nodup is nodup, contradicting head = x appearing at indices 0 and 1
297 have h_filter_nodup : (moves.filter (fun m => m.primitive = prim)).Nodup := by
298 apply List.Nodup.filter
299 simp only [hmoves_def]
300 apply List.Nodup.filterMap _ primitiveOrderList_nodup
301 intro a a' m hma hma'
302 -- hma : m ∈ (if coeff a = 0 then none else some ...)
303 -- hma' : m ∈ (if coeff a' = 0 then none else some ...)
304 by_cases ha : nf.coeff pair a = 0 <;> by_cases ha' : nf.coeff pair a' = 0 <;>
305 simp [ha, ha'] at hma hma'
306 -- Both coeffs nonzero, so m = MicroMove for a and m = MicroMove for a'
307 rw [← hma] at hma'
308 simp only [MicroMove.mk.injEq, true_and] at hma'
309 exact hma'.1.symm
310 rw [hfilt, h_tail_eq] at h_filter_nodup
311 simp only [List.nodup_cons] at h_filter_nodup
312 have ⟨h_head_not_in_tail, _⟩ := h_filter_nodup
313 rw [h_head_x_eq] at h_head_not_in_tail
314 simp at h_head_not_in_tail
315 rw [h_head_eq, h_tail_nil]
316 simp [h_filter_singleton]
317
318/-- Backward compatibility alias -/
319theorem aggCoeff_rowMoves_aux_axiom
320 (nf : NormalForm) (pair : ℕ) (prim : Primitive) :
321 (((primitiveOrderList.filterMap fun q =>
322 if nf.coeff pair q = 0 then none
323 else some (MicroMove.mk pair q (nf.coeff pair q))).filter
324 (fun m => m.pair = pair ∧ m.primitive = prim)).map
325 (·.coeff)).sum
326 = if prim ∈ primitiveOrderList then nf.coeff pair prim else 0 :=
327 aggCoeff_rowMoves_aux_theorem nf pair prim
328
329private lemma aggCoeff_rowMoves_aux
330 (nf : NormalForm) (pair : ℕ) (prim : Primitive) :
331 (((primitiveOrderList.filterMap fun q =>
332 if nf.coeff pair q = 0 then none
333 else some (MicroMove.mk pair q (nf.coeff pair q))).filter
334 (fun m => m.pair = pair ∧ m.primitive = prim)).map
335 (·.coeff)).sum
336 = if prim ∈ primitiveOrderList then nf.coeff pair prim else 0 :=
337 aggCoeff_rowMoves_aux_axiom nf pair prim
338
339/-- Aggregated coefficient for a row equals the stored table value. -/
340lemma aggCoeff_rowMoves (nf : NormalForm) (pair : ℕ) (prim : Primitive) :
341 aggCoeff (rowMoves nf pair) pair prim = nf.coeff pair prim := by
342 classical
343 have hmem : prim ∈ primitiveOrderList := primitive_mem_order prim
344 simpa [aggCoeff, rowMoves, hmem] using aggCoeff_rowMoves_aux nf pair prim
345
346/-- Rows for distinct pairs contribute nothing to another pair's aggregation.
347
348Proof: All moves in rowMoves nf k have m.pair = k (by rowMoves_pair),
349so the filter for pair ≠ k yields an empty list. -/
350theorem aggCoeff_rowMoves_of_ne (nf : NormalForm) {pair k : ℕ} {prim : Primitive}
351 (hkp : k ≠ pair) : aggCoeff (rowMoves nf k) pair prim = 0 := by
352 classical
353 unfold aggCoeff
354 -- All moves in rowMoves nf k have m.pair = k, so none satisfy m.pair = pair when k ≠ pair
355 have h_filter_empty : (rowMoves nf k).filter (fun m => m.pair = pair ∧ m.primitive = prim) = [] := by
356 rw [List.filter_eq_nil_iff]
357 intro m hm
358 simp only [decide_eq_true_eq, not_and]
359 intro h_pair
360 -- m ∈ rowMoves nf k implies m.pair = k
361 have := rowMoves_pair hm
362 -- But we assumed m.pair = pair, so k = pair, contradiction with hkp
363 rw [h_pair] at this
364 exact absurd this.symm hkp
365 simp only [h_filter_empty, List.filter_nil, List.map_nil, List.sum_nil]
366
367/-- Aggregation distributes over concatenation of move lists. -/
368lemma aggCoeff_append (xs ys : List MicroMove) (pair : ℕ) (prim : Primitive) :
369 aggCoeff (xs ++ ys) pair prim = aggCoeff xs pair prim + aggCoeff ys pair prim := by
370 classical
371 unfold aggCoeff
372 simp only [List.filter_append, List.map_append, List.sum_append]
373
374/-- Aggregation over a flat-mapped list of row moves. -/
375theorem aggCoeff_flatMap (nf : NormalForm) (pair : ℕ) (prim : Primitive)
376 (l : List ℕ) (hl : l.Nodup) :
377 aggCoeff (l.flatMap (rowMoves nf)) pair prim
378 = if pair ∈ l then aggCoeff (rowMoves nf pair) pair prim else 0 := by
379 induction l with
380 | nil =>
381 simp only [List.flatMap_nil, List.not_mem_nil, ↓reduceIte]
382 unfold aggCoeff
383 simp
384 | cons h t ih =>
385 simp only [List.flatMap_cons]
386 rw [aggCoeff_append]
387 have hnodup_t : t.Nodup := hl.of_cons
388 have h_not_mem : h ∉ t := hl.not_mem
389 by_cases hpair : pair = h
390 · -- pair = h: contribution comes from rowMoves nf h, and pair ∉ t (since h ∉ t)
391 subst hpair
392 simp only [List.mem_cons, true_or, ↓reduceIte]
393 have h_pair_not_in_t : pair ∉ t := h_not_mem
394 rw [ih hnodup_t]
395 simp only [h_pair_not_in_t, ↓reduceIte, add_zero]
396 · -- pair ≠ h: contribution from rowMoves nf h is 0
397 have h_ne : h ≠ pair := Ne.symm hpair
398 rw [aggCoeff_rowMoves_of_ne nf h_ne]
399 simp only [zero_add]
400 rw [ih hnodup_t]
401 -- pair ∈ h :: t ↔ pair = h ∨ pair ∈ t, but pair ≠ h, so pair ∈ h :: t ↔ pair ∈ t
402 simp only [List.mem_cons, hpair, false_or]
403
404/-- Aggregated coefficient extracted from `toMoves` equals the canonical table. -/
405lemma sumCoeffs_toMoves (nf : NormalForm) (pair : ℕ) (prim : Primitive) :
406 aggCoeff (toMoves nf) pair prim = nf.coeff pair prim := by
407 classical
408 unfold toMoves
409 have hflat := aggCoeff_flatMap (nf := nf) (pair := pair) (prim := prim)
410 (l := pairList nf) (hl := pairList_nodup nf)
411 by_cases hpair : pair ∈ pairList nf
412 · have := aggCoeff_rowMoves (nf := nf) (pair := pair) (prim := prim)
413 simpa [hflat, hpair] using this
414 · have hsupp : pair ∉ nf.supportPairs := by
415 simpa [pairList_mem] using hpair
416 have hzero := nf.zero_outside (pair := pair) (prim := prim) hsupp
417 simp [hflat, hpair, hzero]
418
419/-- Non-zero coefficients guarantee the corresponding move appears in `toMoves`. -/
420lemma mem_toMoves_of_coeff_ne_zero (nf : NormalForm) {pair : ℕ} {prim : Primitive}
421 (hsupp : pair ∈ nf.supportPairs) (hcoeff : nf.coeff pair prim ≠ 0) :
422 ⟨pair, prim, nf.coeff pair prim⟩ ∈ toMoves nf := by
423 classical
424 unfold toMoves
425 have hpair : pair ∈ pairList nf := (pairList_mem).2 hsupp
426 exact List.mem_flatMap.mpr
427 ⟨pair, hpair, rowMoves_mem_of_coeff_ne_zero (nf := nf) (pair := pair) (prim := prim) hcoeff⟩
428
429/-- The mapped pair list produced by `toMoves` contains any supported pair with non-zero coeff. -/
430lemma pair_mem_toMoves_map (nf : NormalForm) {pair : ℕ} {prim : Primitive}
431 (hsupp : pair ∈ nf.supportPairs) (hcoeff : nf.coeff pair prim ≠ 0) :
432 pair ∈ ((toMoves nf).map (·.pair)).toFinset := by
433 classical
434 have hmove := mem_toMoves_of_coeff_ne_zero (nf := nf) hsupp hcoeff
435 have hmap : pair ∈ (toMoves nf).map (·.pair) := by
436 refine List.mem_map.mpr ?_
437 refine ⟨⟨pair, prim, nf.coeff pair prim⟩, hmove, ?_⟩
438 simp
439 exact List.mem_toFinset.mpr hmap
440
441/-- Normal forms round-trip through `toMoves` and `ofMicroMoves`. -/
442theorem of_toMoves (nf : NormalForm) :
443 ofMicroMoves (toMoves nf) = nf := by
444 classical
445 ext pair prim
446 · constructor
447 · intro hmem
448 rcases Finset.mem_filter.mp hmem with ⟨hmap, hex⟩
449 rcases hex with ⟨prim', hagg⟩
450 have hcoeff : nf.coeff pair prim' ≠ 0 := by
451 simpa [sumCoeffs_toMoves] using hagg
452 have : pair ∈ nf.supportPairs := by
453 by_contra hnot
454 have := nf.zero_outside (pair := pair) (prim := prim') hnot
455 exact hcoeff (by simpa [sumCoeffs_toMoves] using this)
456 exact this
457 · intro hmem
458 obtain ⟨prim', hcoeff⟩ := nf.nontrivial hmem
459 have hcoeff' : nf.coeff pair prim' ≠ 0 := hcoeff
460 have hmap := pair_mem_toMoves_map (nf := nf) hmem hcoeff'
461 have : aggCoeff (toMoves nf) pair prim' ≠ 0 := by
462 simpa [sumCoeffs_toMoves] using hcoeff'
463 refine Finset.mem_filter.mpr ⟨hmap, ?_⟩
464 exact ⟨prim', this⟩
465 · simpa [ofMicroMoves, sumCoeffs_toMoves]
466
467/-- The canonical pair list matches the 16-window filtered enumeration. -/
468theorem pairList_eq_filtered_range_theorem (nf : NormalForm)
469 (hw : nf.supportPairs ⊆ Finset.range 16) :
470 pairList nf = (List.range 16).filter (fun k => k ∈ nf.supportPairs) := by
471 unfold pairList
472 -- Both sides are sorted lists of the same elements
473 have h_elements : ∀ x, x ∈ nf.supportPairs.sort (· ≤ ·) ↔ x ∈ (List.range 16).filter (fun k => k ∈ nf.supportPairs) := by
474 intro x
475 simp [mem_sort, List.mem_filter, List.mem_range]
476 intro hx
477 have : x < 16 := by
478 have : x ∈ range 16 := hw hx
479 simpa using this
480 exact this
481 -- Show both lists are sorted using SortedLT (strictly increasing)
482 have h_sorted_lhs : (nf.supportPairs.sort (· ≤ ·)).SortedLT := Finset.sortedLT_sort _
483 have h_sorted_rhs : ((List.range 16).filter (fun k => k ∈ nf.supportPairs)).SortedLT := by
484 have h_range_sorted : (List.range 16).SortedLT := List.sortedLT_range 16
485 exact (h_range_sorted.pairwise.filter _).sortedLT
486 -- Show both lists have no duplicates
487 have h_nodup_lhs : (nf.supportPairs.sort (· ≤ ·)).Nodup := Finset.sort_nodup _ _
488 have h_nodup_rhs : ((List.range 16).filter (fun k => k ∈ nf.supportPairs)).Nodup := by
489 apply List.Nodup.filter
490 exact List.nodup_range
491 -- Build permutation from element equivalence (both lists are nodup)
492 have h_perm : List.Perm (nf.supportPairs.sort (· ≤ ·)) ((List.range 16).filter (fun k => k ∈ nf.supportPairs)) := by
493 rw [List.perm_ext_iff_of_nodup h_nodup_lhs h_nodup_rhs]
494 intro x
495 exact h_elements x
496 -- Apply uniqueness of sorted lists
497 exact h_perm.eq_of_sortedLE h_sorted_lhs.sortedLE h_sorted_rhs.sortedLE
498
499/-- Backward compatibility alias -/
500theorem pairList_eq_filtered_range_axiom (nf : NormalForm)
501 (hw : nf.supportPairs ⊆ Finset.range 16) :
502 pairList nf = (List.range 16).filter (fun k => k ∈ nf.supportPairs) :=
503 pairList_eq_filtered_range_theorem nf hw
504
505lemma pairList_eq_filtered_range (nf : NormalForm)
506 (hw : nf.supportPairs ⊆ Finset.range 16) :
507 pairList nf = (List.range 16).filter (fun k => k ∈ nf.supportPairs) :=
508 pairList_eq_filtered_range_theorem nf hw
509
510end NormalForm
511
512end MicroMove
513
514end Virtues
515end Ethics
516end IndisputableMonolith
517