IndisputableMonolith.Loom.Core
IndisputableMonolith/Loom/Core.lean · 806 lines · 106 declarations
show as:
view math explainer →
1import Mathlib.Data.ZMod.Basic
2import Mathlib.Data.List.Perm.Basic
3import Mathlib.Data.List.Sort
4import Mathlib.Tactic.Ring
5import Mathlib.Tactic.LinearCombination
6
7/-!
8# Loom: a certificate language for configurations of closed recognition walks
9
10A recognition history is a walk across states, and a finished history closes. On the
11eight state, three axis window the forcing chain gives us, the closed walks up to
12homotopy form a free group of rank `E - V + 1 = 5`, so a closed walk is a word in five
13signed generators and a finished utterance is a finite LIST of such words sharing one
14basepoint.
15
16Two premises fix what counts as content, and both say something is NOT content.
17Spelling is not content, so words are read up to free reduction. Where the utterance
18started is not content, because a received meaning arrives whole rather than word by
19word, so one SIMULTANEOUS conjugation of every loop by the same word is not content
20either. That second premise was carried as phenomenological rather than proved, and this
21header said everything below was conditional on it. `Loom.BasepointForced` has since
22removed it from the load path, and the honest statement now has two parts. Closure gives
23conjugation by prefixes of the walk as a theorem (`rotate_is_conjugation`), since a closed
24history is a map from a circle and names no vertex of itself as first. The step from
25prefixes to arbitrary words is vertex homogeneity, which is not proved there either; it is
26the same refusal to let an observable depend on a label the description supplies that
27already motivates quotienting by the 48 automorphisms of the window. So a reader who
28accepts that quotient is committed to this one, and a reader who rejects it is not. The
29phenomenological observation now agrees with the argument instead of carrying it.
30
31This module supplies three things and nothing else: a total checker for
32well-formedness, a computable invariant of a configuration, and the theorems that the
33invariant is blind to exactly the two non-content operations. It carries no model and
34no search, so it can be trusted with a finished object it did not build.
35
36The invariant reads traces in `SL(2, ZMod 3)`. Trace is a class function, which is the
37whole reason it is usable here: blindness to conjugation is a ring identity rather than
38a canonicalisation. Loop traces alone do not separate the intended witness (measured:
39they collide on two of the forty eight automorphism images), so the invariant also
40reads the traces of the pairwise COMMUTATORS of the loop images, which is the depth two
41data of the lower central series and is exactly what an abelianised reading destroys.
42-/
43
44namespace IndisputableMonolith
45namespace Loom
46
47/-- A closed walk up to homotopy: a word in the five signed cotree generators. -/
48abbrev Word := List Int
49
50/-- An utterance: a finite list of closed walks sharing one basepoint. -/
51abbrev Config := List Word
52
53-- ---------------------------------------------------------------------------
54-- free reduction, and the checker
55-- ---------------------------------------------------------------------------
56
57/-- Prepend one act to an already reduced word, cancelling if it cancels. -/
58def consRed (x : Int) : Word → Word
59 | [] => [x]
60 | y :: r => if x + y = 0 then r else x :: y :: r
61
62/-- Free reduction. Total and linear, which is why every question this language can
63ask is cheap and always answerable. -/
64def reduceWord : Word → Word
65 | [] => []
66 | x :: t => consRed x (reduceWord t)
67
68/-- No adjacent cancelling pair. This is what the checker checks. -/
69def isReduced : Word → Bool
70 | [] => true
71 | [_] => true
72 | x :: y :: t => (x + y != 0) && isReduced (y :: t)
73
74/-- Reversing a walk and negating every act. Per loop this is a content operation
75(it is how denial is encoded); applied to every loop at once it is gauge. -/
76def invWord : Word → Word
77 | [] => []
78 | x :: t => invWord t ++ [-x]
79
80/-- Moving the basepoint of the whole utterance by one word. -/
81def conjWord (g w : Word) : Word := reduceWord (g ++ w ++ invWord g)
82
83theorem reduceWord_cons (x : Int) (t : Word) :
84 reduceWord (x :: t) = consRed x (reduceWord t) := rfl
85
86theorem invWord_cons (x : Int) (t : Word) : invWord (x :: t) = invWord t ++ [-x] := rfl
87
88theorem isReduced_cons_cons (x y : Int) (t : Word) :
89 isReduced (x :: y :: t) = ((x + y != 0) && isReduced (y :: t)) := rfl
90
91theorem isReduced_tail (y : Int) (r : Word) (h : isReduced (y :: r) = true) :
92 isReduced r = true := by
93 cases r with
94 | nil => rfl
95 | cons z t =>
96 rw [isReduced_cons_cons] at h
97 exact (Bool.and_eq_true _ _ ▸ h).2
98
99theorem isReduced_consRed (x : Int) (u : Word) (h : isReduced u = true) :
100 isReduced (consRed x u) = true := by
101 cases u with
102 | nil => rfl
103 | cons y r =>
104 by_cases hxy : x + y = 0
105 · rw [consRed, if_pos hxy]
106 exact isReduced_tail y r h
107 · rw [consRed, if_neg hxy, isReduced_cons_cons]
108 refine Bool.and_eq_true _ _ ▸ ⟨?_, h⟩
109 simpa only [bne_iff_ne, ne_eq] using hxy
110
111/-- The checker's specification: reduction really reduces. Without this the checker's
112verdict would be a wish rather than a fact. -/
113theorem isReduced_reduceWord (w : Word) : isReduced (reduceWord w) = true := by
114 induction w with
115 | nil => rfl
116 | cons x t ih => exact isReduced_consRed x (reduceWord t) ih
117
118/-- The frame generator: the cotree edge that closes the Gray cycle, so the loop that
119is the complete recognition window. The census measured all ninety six Hamiltonian
120walks as a single class under gauge, which is what lets this loop supply an orientation
121reference without contributing content of its own. -/
122def frameGen : Int := 2
123
124/-- The total checker. An utterance is well formed when every loop is a reduced word
125and the frame loop is present. Both conditions are decidable in linear time. -/
126def wellFormed (c : Config) : Bool :=
127 c.all isReduced && c.contains [frameGen]
128
129-- ---------------------------------------------------------------------------
130-- two by two matrices over ZMod 3, by components
131-- ---------------------------------------------------------------------------
132
133/-- Components rather than `Matrix`, because a later module evaluates several thousand
134products inside the kernel and `Finset.sum` does not reduce cheaply. -/
135structure Mat where
136 a : ZMod 3
137 b : ZMod 3
138 c : ZMod 3
139 d : ZMod 3
140deriving DecidableEq, Repr
141
142namespace Mat
143
144theorem eq_of (X Y : Mat) (ha : X.a = Y.a) (hb : X.b = Y.b) (hc : X.c = Y.c)
145 (hd : X.d = Y.d) : X = Y := by
146 cases X
147 cases Y
148 subst ha
149 subst hb
150 subst hc
151 subst hd
152 rfl
153
154def one : Mat := ⟨1, 0, 0, 1⟩
155
156def mul (X Y : Mat) : Mat :=
157 ⟨X.a * Y.a + X.b * Y.c, X.a * Y.b + X.b * Y.d,
158 X.c * Y.a + X.d * Y.c, X.c * Y.b + X.d * Y.d⟩
159
160def det (X : Mat) : ZMod 3 := X.a * X.d - X.b * X.c
161
162/-- The adjugate. It is a total function, and it is the inverse exactly when the
163determinant is one, which is the case for every matrix this module evaluates. -/
164def adj (X : Mat) : Mat := ⟨X.d, -X.b, -X.c, X.a⟩
165
166def tr (X : Mat) : ZMod 3 := X.a + X.d
167
168/-- The trace as a natural number, so invariants are lists of `Nat` and can be sorted
169by a hand rolled comparison that no library change can move. -/
170def trN (X : Mat) : Nat := (tr X).val
171
172theorem mul_assoc' (X Y Z : Mat) : mul (mul X Y) Z = mul X (mul Y Z) := by
173 cases X; cases Y; cases Z
174 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [mul] <;> ring
175
176theorem one_mul' (X : Mat) : mul one X = X := by
177 cases X
178 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [mul, one] <;> ring
179
180theorem mul_one' (X : Mat) : mul X one = X := by
181 cases X
182 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [mul, one] <;> ring
183
184instance : Mul Mat := ⟨mul⟩
185instance : One Mat := ⟨one⟩
186
187instance : Monoid Mat where
188 mul_assoc := mul_assoc'
189 one_mul := one_mul'
190 mul_one := mul_one'
191
192theorem mul_def (X Y : Mat) : X * Y = mul X Y := rfl
193theorem one_def : (1 : Mat) = one := rfl
194
195theorem det_mul (X Y : Mat) : det (X * Y) = det X * det Y := by
196 cases X; cases Y
197 simp only [mul_def, mul, det]
198 ring
199
200theorem det_one : det (1 : Mat) = 1 := by
201 simp only [one_def, one, det]
202 ring
203
204/-- An identity for two by two matrices over any commutative ring, with no
205determinant hypothesis. This is the lemma that makes the conjugation argument short:
206without it the components blow up and nothing closes. -/
207theorem adj_mul (X Y : Mat) : adj (X * Y) = adj Y * adj X := by
208 cases X; cases Y
209 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [mul_def, mul, adj] <;> ring
210
211theorem adj_adj (X : Mat) : adj (adj X) = X := by
212 cases X
213 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [adj] <;> ring
214
215theorem tr_adj (X : Mat) : tr (adj X) = tr X := by
216 cases X
217 simp only [adj, tr]
218 ring
219
220theorem tr_mul_comm (X Y : Mat) : tr (X * Y) = tr (Y * X) := by
221 cases X; cases Y
222 simp only [mul_def, mul, tr]
223 ring
224
225theorem mul_adj_of_det_one (X : Mat) (h : det X = 1) : X * adj X = 1 := by
226 cases X
227 simp only [det] at h
228 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [mul_def, mul, adj, one_def, one]
229 · linear_combination h
230 · ring
231 · ring
232 · linear_combination h
233
234theorem adj_mul_of_det_one (X : Mat) (h : det X = 1) : adj X * X = 1 := by
235 cases X
236 simp only [det] at h
237 refine eq_of _ _ ?_ ?_ ?_ ?_ <;> simp only [mul_def, mul, adj, one_def, one]
238 · linear_combination h
239 · ring
240 · ring
241 · linear_combination h
242
243/-- Moving the basepoint: conjugation by a matrix of determinant one. -/
244def cj (G X : Mat) : Mat := G * X * adj G
245
246/-- Conjugation commutes with the adjugate, with no hypothesis at all, because
247`adj_mul` and `adj_adj` are identities. -/
248theorem adj_cj (G X : Mat) : adj (cj G X) = cj G (adj X) := by
249 simp only [cj, adj_mul, adj_adj, mul_assoc]
250
251theorem adj_one : adj (1 : Mat) = 1 := by decide
252
253theorem cj_mul (G X Y : Mat) (h : det G = 1) : cj G X * cj G Y = cj G (X * Y) := by
254 have hGG : adj G * G = 1 := adj_mul_of_det_one G h
255 simp only [cj, mul_assoc]
256 rw [← mul_assoc (adj G) G, hGG, one_mul]
257
258
259theorem tr_cj (G X : Mat) (h : det G = 1) : tr (cj G X) = tr X := by
260 have hGG : adj G * G = 1 := adj_mul_of_det_one G h
261 calc tr (cj G X) = tr (G * (X * adj G)) := by simp only [cj, mul_assoc]
262 _ = tr (X * adj G * G) := tr_mul_comm _ _
263 _ = tr (X * (adj G * G)) := by simp only [mul_assoc]
264 _ = tr X := by rw [hGG, mul_one]
265
266/-- The commutator of two loop images: the depth two coordinate. An abelianised
267reading is blind to this by construction, which is why it is here. -/
268def comm (X Y : Mat) : Mat := X * Y * (adj X * adj Y)
269
270theorem comm_cj (G X Y : Mat) (h : det G = 1) :
271 comm (cj G X) (cj G Y) = cj G (comm X Y) := by
272 simp only [comm, adj_cj]
273 rw [cj_mul G X Y h, cj_mul G (adj X) (adj Y) h, cj_mul G (X * Y) (adj X * adj Y) h]
274
275theorem det_adj (X : Mat) : det (adj X) = det X := by
276 cases X
277 simp only [adj, det]
278 ring
279
280/-- The commutator trace is symmetric in its two loops, with no hypothesis. For two by
281two matrices `tr (X * adj Y) = det (X + Y) - det X - det Y`, which is symmetric, and
282that is what makes the invariant blind to the ORDER of the loops. Without this the
283invariant would be reading the order in which loops happened to be listed, which is
284not content. -/
285theorem tr_comm_symm (X Y : Mat) : tr (comm X Y) = tr (comm Y X) := by
286 cases X
287 cases Y
288 simp only [comm, mul_def, mul, adj, tr]
289 ring
290
291theorem trN_comm_symm (X Y : Mat) : trN (comm X Y) = trN (comm Y X) := by
292 simp only [trN, tr_comm_symm]
293
294/-- Reversing every loop at once cannot be seen by any trace, because in this group
295the inverse is the adjugate. The gate takes the hostile position that reversal IS
296gauge, and this theorem is why that position costs nothing. -/
297theorem trN_comm_adj (X Y : Mat) : trN (comm (adj X) (adj Y)) = trN (comm X Y) := by
298 have h1 : comm (adj X) (adj Y) = adj (Y * X) * (X * Y) := by
299 simp only [comm, adj_adj, adj_mul, mul_assoc]
300 have h2 : comm X Y = X * Y * adj (Y * X) := by
301 simp only [comm, adj_mul, mul_assoc]
302 simp only [trN, h1, h2, tr_mul_comm (adj (Y * X)) (X * Y)]
303
304end Mat
305
306-- ---------------------------------------------------------------------------
307-- the homomorphism, given as a table
308-- ---------------------------------------------------------------------------
309
310/-- For each generator, the matrix it goes to and the matrix its inverse goes to. -/
311abbrev Table := List (Mat × Mat)
312
313def entryOk (e : Mat × Mat) : Bool :=
314 (Mat.mul e.1 e.2 == Mat.one) && (Mat.mul e.2 e.1 == Mat.one) &&
315 (Mat.det e.1 == 1) && (Mat.det e.2 == 1)
316
317/-- A table defines a homomorphism from the free group exactly when each pair really
318is an inverse pair inside the determinant one subgroup. Decidable, so the data can be
319checked rather than trusted. -/
320def Table.ok (T : Table) : Bool := T.all entryOk
321
322def matAt : Table → Nat → Mat × Mat
323 | [], _ => (Mat.one, Mat.one)
324 | e :: _, 0 => e
325 | _ :: t, (n + 1) => matAt t n
326
327theorem entryOk_one : entryOk (Mat.one, Mat.one) = true := by decide
328
329theorem entryOk_matAt (T : Table) (hT : Table.ok T = true) (n : Nat) :
330 entryOk (matAt T n) = true := by
331 induction T generalizing n with
332 | nil => simpa only [matAt] using entryOk_one
333 | cons e t ih =>
334 simp only [Table.ok, List.all_cons, Bool.and_eq_true] at hT
335 cases n with
336 | zero => simpa only [matAt] using hT.1
337 | succ m => exact ih (by simpa only [Table.ok] using hT.2) m
338
339def letterMat (T : Table) (x : Int) : Mat :=
340 if 0 < x then (matAt T (x.natAbs - 1)).1
341 else if x < 0 then (matAt T (x.natAbs - 1)).2
342 else Mat.one
343
344theorem det_letterMat (T : Table) (hT : Table.ok T = true) (x : Int) :
345 Mat.det (letterMat T x) = 1 := by
346 have h := entryOk_matAt T hT (x.natAbs - 1)
347 simp only [entryOk, Bool.and_eq_true, beq_iff_eq] at h
348 simp only [letterMat]
349 by_cases hx : 0 < x
350 · simp only [hx, if_pos]
351 exact h.1.2
352 · simp only [hx, if_neg]
353 by_cases hx' : x < 0
354 · simp only [hx', if_pos]
355 exact h.2
356 · simp only [hx', if_neg]
357 exact Mat.det_one
358
359theorem letterMat_mul_neg (T : Table) (hT : Table.ok T = true) (x : Int) :
360 letterMat T x * letterMat T (-x) = 1 := by
361 have h := entryOk_matAt T hT (x.natAbs - 1)
362 simp only [entryOk, Bool.and_eq_true, beq_iff_eq] at h
363 have habs : (-x).natAbs = x.natAbs := Int.natAbs_neg x
364 simp only [letterMat, habs]
365 by_cases hx : 0 < x
366 · have hneg : ¬ (0 < -x) := by omega
367 have hneg' : -x < 0 := by omega
368 simp only [hx, if_pos, hneg, if_neg, hneg', if_pos, Mat.mul_def]
369 exact h.1.1.1
370 · by_cases hx' : x < 0
371 · have hneg : (0 : Int) < -x := by omega
372 simp only [hx, if_neg, hx', if_pos, hneg, if_pos, Mat.mul_def]
373 exact h.1.1.2
374 · have hx0 : x = 0 := by omega
375 subst hx0
376 simp only [Mat.mul_def]
377 norm_num
378 exact Mat.mul_one' Mat.one
379
380/-- The image of a word. Structural on the head, so appending is an easy induction. -/
381def evalWord (T : Table) : Word → Mat
382 | [] => 1
383 | x :: t => letterMat T x * evalWord T t
384
385def evalConfig (T : Table) (c : Config) : List Mat := c.map (evalWord T)
386
387theorem evalWord_cons (T : Table) (x : Int) (t : Word) :
388 evalWord T (x :: t) = letterMat T x * evalWord T t := rfl
389
390theorem evalWord_singleton (T : Table) (x : Int) : evalWord T [x] = letterMat T x := by
391 simp only [evalWord, mul_one]
392
393theorem evalWord_append (T : Table) (u v : Word) :
394 evalWord T (u ++ v) = evalWord T u * evalWord T v := by
395 induction u with
396 | nil => simp only [List.nil_append, evalWord, one_mul]
397 | cons x t ih => simp only [List.cons_append, evalWord, ih, mul_assoc]
398
399theorem det_evalWord (T : Table) (hT : Table.ok T = true) (w : Word) :
400 Mat.det (evalWord T w) = 1 := by
401 induction w with
402 | nil => simpa only [evalWord] using Mat.det_one
403 | cons x t ih =>
404 simp only [evalWord, Mat.det_mul, ih, det_letterMat T hT x, one_mul]
405
406/-- One letter's inverse image is its adjugate. This is the only place the determinant
407one hypothesis is really used. -/
408theorem letterMat_neg (T : Table) (hT : Table.ok T = true) (x : Int) :
409 letterMat T (-x) = Mat.adj (letterMat T x) := by
410 have hx : Mat.det (letterMat T x) = 1 := det_letterMat T hT x
411 have h := letterMat_mul_neg T hT x
412 calc letterMat T (-x) = 1 * letterMat T (-x) := (one_mul _).symm
413 _ = Mat.adj (letterMat T x) * letterMat T x * letterMat T (-x) := by
414 rw [Mat.adj_mul_of_det_one _ hx]
415 _ = Mat.adj (letterMat T x) * (letterMat T x * letterMat T (-x)) := by
416 rw [mul_assoc]
417 _ = Mat.adj (letterMat T x) := by rw [h, mul_one]
418
419theorem evalWord_invWord (T : Table) (hT : Table.ok T = true) (w : Word) :
420 evalWord T (invWord w) = Mat.adj (evalWord T w) := by
421 induction w with
422 | nil => simp only [invWord, evalWord, Mat.adj_one]
423 | cons x t ih =>
424 rw [invWord_cons, evalWord_append, ih, evalWord_singleton,
425 letterMat_neg T hT x, evalWord_cons, Mat.adj_mul]
426
427theorem evalWord_consRed (T : Table) (hT : Table.ok T = true) (x : Int) (u : Word) :
428 evalWord T (consRed x u) = letterMat T x * evalWord T u := by
429 cases u with
430 | nil => rw [consRed, evalWord_singleton, evalWord, mul_one]
431 | cons y r =>
432 by_cases hxy : x + y = 0
433 · have hy : y = -x := by omega
434 subst hy
435 rw [consRed, if_pos hxy, evalWord_cons, ← mul_assoc,
436 letterMat_mul_neg T hT x, one_mul]
437 · rw [consRed, if_neg hxy]
438 exact evalWord_cons T x (y :: r)
439
440theorem evalWord_reduceWord (T : Table) (hT : Table.ok T = true) (w : Word) :
441 evalWord T (reduceWord w) = evalWord T w := by
442 induction w with
443 | nil => rfl
444 | cons x t ih =>
445 rw [reduceWord_cons, evalWord_consRed T hT, ih, evalWord_cons]
446
447-- ---------------------------------------------------------------------------
448-- relabelling the generators: the automorphism half of the gauge group
449-- ---------------------------------------------------------------------------
450
451/-- An automorphism of the recognition window acts on the five generators by sending
452each to a word. A relabelling is that data. -/
453abbrev Subst := List Word
454
455def getWord : Subst → Nat → Word
456 | [], _ => []
457 | g :: _, 0 => g
458 | _ :: t, (n + 1) => getWord t n
459
460def substLetter (σ : Subst) (x : Int) : Word :=
461 if 0 < x then getWord σ (x.natAbs - 1)
462 else if x < 0 then invWord (getWord σ (x.natAbs - 1))
463 else []
464
465def substWord (σ : Subst) : Word → Word
466 | [] => []
467 | x :: t => substLetter σ x ++ substWord σ t
468
469theorem substWord_cons (σ : Subst) (x : Int) (t : Word) :
470 substWord σ (x :: t) = substLetter σ x ++ substWord σ t := rfl
471
472def substConfig (σ : Subst) (c : Config) : Config := c.map (substWord σ)
473
474/-- Pushing a relabelling through a homomorphism gives another homomorphism, and this
475computes it. Because Lean builds this itself from the relabelling, the composite
476tables are not trusted data. -/
477def tableOfSubst (T : Table) (σ : Subst) : Table :=
478 σ.map (fun g => (evalWord T g, evalWord T (invWord g)))
479
480theorem ok_tableOfSubst (T : Table) (hT : Table.ok T = true) (σ : Subst) :
481 Table.ok (tableOfSubst T σ) = true := by
482 simp only [Table.ok, List.all_eq_true, tableOfSubst, List.mem_map]
483 rintro e ⟨g, -, rfl⟩
484 have hM : Mat.det (evalWord T g) = 1 := det_evalWord T hT g
485 have hinv : evalWord T (invWord g) = Mat.adj (evalWord T g) := evalWord_invWord T hT g
486 have h1 : Mat.mul (evalWord T g) (evalWord T (invWord g)) = Mat.one := by
487 rw [hinv, ← Mat.mul_def, Mat.mul_adj_of_det_one _ hM, Mat.one_def]
488 have h2 : Mat.mul (evalWord T (invWord g)) (evalWord T g) = Mat.one := by
489 rw [hinv, ← Mat.mul_def, Mat.adj_mul_of_det_one _ hM, Mat.one_def]
490 have h3 : Mat.det (evalWord T (invWord g)) = 1 := by
491 rw [hinv, Mat.det_adj]; exact hM
492 simp only [entryOk, h1, h2, h3, hM, beq_self_eq_true, Bool.and_self]
493
494theorem matAt_tableOfSubst (T : Table) (σ : Subst) (n : Nat) :
495 matAt (tableOfSubst T σ) n
496 = (evalWord T (getWord σ n), evalWord T (invWord (getWord σ n))) := by
497 induction σ generalizing n with
498 | nil => cases n with
499 | zero => rfl
500 | succ m => rfl
501 | cons g t ih => cases n with
502 | zero => rfl
503 | succ m => exact ih m
504
505theorem evalWord_substLetter (T : Table) (σ : Subst) (x : Int) :
506 evalWord T (substLetter σ x) = letterMat (tableOfSubst T σ) x := by
507 rw [substLetter, letterMat, matAt_tableOfSubst]
508 by_cases hx : 0 < x
509 · rw [if_pos hx, if_pos hx]
510 · rw [if_neg hx, if_neg hx]
511 by_cases hx' : x < 0
512 · rw [if_pos hx', if_pos hx']
513 · rw [if_neg hx', if_neg hx']
514 rfl
515
516/-- Reading a relabelled utterance under a homomorphism is reading the original
517utterance under the relabelled homomorphism. This is what lets the forty eight
518automorphisms of the window be checked by changing the table rather than by rewriting
519every word, and it is a theorem rather than an assumption. -/
520theorem evalWord_substWord (T : Table) (σ : Subst) (w : Word) :
521 evalWord T (substWord σ w) = evalWord (tableOfSubst T σ) w := by
522 induction w with
523 | nil => rfl
524 | cons x t ih =>
525 rw [substWord_cons, evalWord_append, ih, evalWord_substLetter, evalWord_cons]
526
527-- ---------------------------------------------------------------------------
528-- the invariant
529-- ---------------------------------------------------------------------------
530
531def insertNat (x : Nat) : List Nat → List Nat
532 | [] => [x]
533 | y :: t => if x ≤ y then x :: y :: t else y :: insertNat x t
534
535/-- Hand rolled, so no library rename can silently change what the invariant is. -/
536def sortNat : List Nat → List Nat
537 | [] => []
538 | x :: t => insertNat x (sortNat t)
539
540/-- Traces of the pairwise commutators, over index pairs in order. Because both sides
541of every theorem below build this list in the same order, no permutation reasoning is
542needed anywhere. -/
543def pairTraces : List Mat → List Nat
544 | [] => []
545 | M :: rest => rest.map (fun N => Mat.trN (Mat.comm M N)) ++ pairTraces rest
546
547/-- Depth one and depth two, together. The first component is what an amplitude style
548reading can see and the second is what it cannot. -/
549def invariantOf (Ms : List Mat) : List Nat × List Nat :=
550 (sortNat (Ms.map Mat.trN), sortNat (pairTraces Ms))
551
552def invariant (T : Table) (c : Config) : List Nat × List Nat :=
553 invariantOf (evalConfig T c)
554
555-- ---------------------------------------------------------------------------
556-- the sort is honest: the invariant reads a multiset, not a list
557-- ---------------------------------------------------------------------------
558
559theorem insertNat_perm (x : Nat) (l : List Nat) :
560 List.Perm (insertNat x l) (x :: l) := by
561 induction l with
562 | nil => exact List.Perm.refl _
563 | cons y t ih =>
564 by_cases h : x ≤ y
565 · rw [insertNat, if_pos h]
566 · rw [insertNat, if_neg h]
567 exact (List.Perm.cons y ih).trans (List.Perm.swap x y t)
568
569theorem sortNat_perm (l : List Nat) : List.Perm (sortNat l) l := by
570 induction l with
571 | nil => exact List.Perm.refl _
572 | cons x t ih => exact (insertNat_perm x (sortNat t)).trans (List.Perm.cons x ih)
573
574theorem pairwise_insertNat (x : Nat) (l : List Nat) (h : l.Pairwise (· ≤ ·)) :
575 (insertNat x l).Pairwise (· ≤ ·) := by
576 induction l with
577 | nil => simp only [insertNat, List.pairwise_cons, List.not_mem_nil, false_implies,
578 implies_true, List.Pairwise.nil, and_self]
579 | cons y t ih =>
580 rw [List.pairwise_cons] at h
581 by_cases hxy : x ≤ y
582 · rw [insertNat, if_pos hxy, List.pairwise_cons]
583 refine ⟨?_, List.pairwise_cons.mpr h⟩
584 intro b hb
585 rcases List.mem_cons.mp hb with rfl | hb
586 · exact hxy
587 · exact le_trans hxy (h.1 b hb)
588 · rw [insertNat, if_neg hxy, List.pairwise_cons]
589 refine ⟨?_, ih h.2⟩
590 intro b hb
591 rcases List.mem_cons.mp ((insertNat_perm x t).mem_iff.mp hb) with rfl | hb
592 · exact le_of_not_le hxy
593 · exact h.1 b hb
594
595theorem pairwise_sortNat (l : List Nat) : (sortNat l).Pairwise (· ≤ ·) := by
596 induction l with
597 | nil => exact List.Pairwise.nil
598 | cons x t ih => exact pairwise_insertNat x (sortNat t) ih
599
600theorem sortNat_eq_of_perm {l₁ l₂ : List Nat} (h : List.Perm l₁ l₂) :
601 sortNat l₁ = sortNat l₂ :=
602 List.Perm.eq_of_pairwise'
603 (pairwise_sortNat l₁) (pairwise_sortNat l₂)
604 ((sortNat_perm l₁).trans (h.trans (sortNat_perm l₂).symm))
605
606theorem perm_append_left_comm (A B P : List Nat) :
607 List.Perm (A ++ (B ++ P)) (B ++ (A ++ P)) := by
608 rw [← List.append_assoc A B P, ← List.append_assoc B A P]
609 exact List.Perm.append_right P List.perm_append_comm
610
611/-- The pairwise commutator traces of a reordered utterance are the same multiset. The
612swap case is where the symmetry of the commutator trace is spent. -/
613theorem pairTraces_perm {Ms Ns : List Mat} (h : List.Perm Ms Ns) :
614 List.Perm (pairTraces Ms) (pairTraces Ns) := by
615 induction h with
616 | nil => exact List.Perm.refl _
617 | cons M h ih =>
618 simp only [pairTraces]
619 exact List.Perm.append (h.map _) ih
620 | swap M N l =>
621 simp only [pairTraces, List.map_cons, List.cons_append]
622 rw [Mat.trN_comm_symm N M]
623 exact List.Perm.cons _ (perm_append_left_comm _ _ _)
624 | trans h₁ h₂ ih₁ ih₂ => exact ih₁.trans ih₂
625
626/-- SOUNDNESS, the multiset half. An utterance is a multiset of loops, and the
627invariant reads it as one: no ordering of the loops is content. -/
628theorem invariantOf_perm {Ms Ns : List Mat} (h : List.Perm Ms Ns) :
629 invariantOf Ms = invariantOf Ns := by
630 simp only [invariantOf, sortNat_eq_of_perm (h.map Mat.trN),
631 sortNat_eq_of_perm (pairTraces_perm h)]
632
633theorem invariant_perm (T : Table) {c d : Config} (h : List.Perm c d) :
634 invariant T c = invariant T d :=
635 invariantOf_perm (h.map (evalWord T))
636
637/-- THE SOUNDNESS THEOREM. There is no first word: moving the basepoint of the whole
638utterance leaves the invariant alone. -/
639theorem invariantOf_cj (G : Mat) (h : Mat.det G = 1) (Ms : List Mat) :
640 invariantOf (Ms.map (Mat.cj G)) = invariantOf Ms := by
641 have hloops : (Ms.map (Mat.cj G)).map Mat.trN = Ms.map Mat.trN := by
642 simp only [List.map_map]
643 apply List.map_congr_left
644 intro M _
645 simp only [Function.comp_apply, Mat.trN, Mat.tr_cj G M h]
646 have hpairs : ∀ Ns : List Mat, pairTraces (Ns.map (Mat.cj G)) = pairTraces Ns := by
647 intro Ns
648 induction Ns with
649 | nil => simp only [List.map_nil, pairTraces]
650 | cons M rest ih =>
651 simp only [List.map_cons, pairTraces, ih]
652 congr 1
653 simp only [List.map_map]
654 apply List.map_congr_left
655 intro N _
656 simp only [Function.comp_apply, Mat.comm_cj G M N h, Mat.trN, Mat.tr_cj _ _ h]
657 simp only [invariantOf, hloops, hpairs]
658
659/-- Reversing every loop at once is invisible too, and this one needs no hypothesis:
660in the determinant one subgroup the inverse is the adjugate, and no trace can see an
661adjugate. So the gate's hostile choice, putting time reversal into the gauge group,
662costs the carrier nothing. -/
663theorem invariantOf_adj (Ms : List Mat) :
664 invariantOf (Ms.map Mat.adj) = invariantOf Ms := by
665 have hloops : (Ms.map Mat.adj).map Mat.trN = Ms.map Mat.trN := by
666 simp only [List.map_map]
667 apply List.map_congr_left
668 intro M _
669 simp only [Function.comp_apply, Mat.trN, Mat.tr_adj]
670 have hpairs : ∀ Ns : List Mat, pairTraces (Ns.map Mat.adj) = pairTraces Ns := by
671 intro Ns
672 induction Ns with
673 | nil => simp only [List.map_nil, pairTraces]
674 | cons M rest ih =>
675 simp only [List.map_cons, pairTraces, ih]
676 congr 1
677 simp only [List.map_map]
678 apply List.map_congr_left
679 intro N _
680 simp only [Function.comp_apply, Mat.trN_comm_adj]
681 simp only [invariantOf, hloops, hpairs]
682
683/-- Moving one loop's basepoint is conjugating its image. -/
684theorem evalWord_conjWord (T : Table) (hT : Table.ok T = true) (g w : Word) :
685 evalWord T (conjWord g w) = Mat.cj (evalWord T g) (evalWord T w) := by
686 simp only [conjWord, evalWord_reduceWord T hT, evalWord_append,
687 evalWord_invWord T hT, Mat.cj, mul_assoc]
688
689/-- Nesting is invisible at depth one. A loop that sits inside a binder is a CONJUGATE
690of the same loop outside it, and a trace cannot see a conjugation, which is exactly why
691the invariant has to read the commutators as well. -/
692theorem trN_conjWord (T : Table) (hT : Table.ok T = true) (g w : Word) :
693 Mat.trN (evalWord T (conjWord g w)) = Mat.trN (evalWord T w) := by
694 rw [evalWord_conjWord T hT]
695 simp only [Mat.trN, Mat.tr_cj _ _ (det_evalWord T hT g)]
696
697/-- The two soundness statements as one fact about utterances: respelling every loop
698and moving the shared basepoint leave the invariant alone. -/
699theorem invariant_conjWord (T : Table) (hT : Table.ok T = true) (g : Word)
700 (c : Config) : invariant T (c.map (conjWord g)) = invariant T c := by
701 have hev : ∀ w : Word, evalWord T (conjWord g w)
702 = Mat.cj (evalWord T g) (evalWord T w) := evalWord_conjWord T hT g
703 have hmap : evalConfig T (c.map (conjWord g))
704 = (evalConfig T c).map (Mat.cj (evalWord T g)) := by
705 simp only [evalConfig, List.map_map]
706 apply List.map_congr_left
707 intro w _
708 simp only [Function.comp_apply, hev w]
709 simp only [invariant, hmap,
710 invariantOf_cj (evalWord T g) (det_evalWord T hT g) (evalConfig T c)]
711
712/-- Reversing every loop of an utterance at once leaves the invariant alone. -/
713theorem invariant_map_invWord (T : Table) (hT : Table.ok T = true) (c : Config) :
714 invariant T (c.map invWord) = invariant T c := by
715 have hmap : evalConfig T (c.map invWord) = (evalConfig T c).map Mat.adj := by
716 simp only [evalConfig, List.map_map]
717 apply List.map_congr_left
718 intro w _
719 simp only [Function.comp_apply, evalWord_invWord T hT w]
720 simp only [invariant, hmap, invariantOf_adj]
721
722/-- SOUNDNESS, the relabelling half. Reading a relabelled utterance is reading the
723original one under the relabelled homomorphism, so the forty eight automorphisms of the
724window are checked by forty eight tables and no word is rewritten. -/
725theorem invariant_substConfig (T : Table) (σ : Subst) (c : Config) :
726 invariant T (substConfig σ c) = invariant (tableOfSubst T σ) c := by
727 have h : evalConfig T (substConfig σ c) = evalConfig (tableOfSubst T σ) c := by
728 simp only [evalConfig, substConfig, List.map_map]
729 apply List.map_congr_left
730 intro w _
731 simp only [Function.comp_apply, evalWord_substWord]
732 simp only [invariant, h]
733
734-- ---------------------------------------------------------------------------
735-- the checker, at the level of an utterance
736-- ---------------------------------------------------------------------------
737
738/-- Freely reduce every loop. Total, linear in the size of the utterance. -/
739def reduceConfig (c : Config) : Config := c.map reduceWord
740
741theorem all_isReduced_reduceConfig (c : Config) :
742 (reduceConfig c).all isReduced = true := by
743 simp only [reduceConfig, List.all_eq_true, List.mem_map]
744 rintro w ⟨v, -, rfl⟩
745 exact isReduced_reduceWord v
746
747/-- The checker accepts every framed, normalised utterance. This is the checker's
748specification: it never rejects an honest utterance, and by `isReduced_reduceWord` its
749verdict is a fact about the words rather than a wish. -/
750theorem wellFormed_reduceConfig_frame (c : Config) :
751 wellFormed (reduceConfig ([frameGen] :: c)) = true := by
752 have h : reduceConfig ([frameGen] :: c) = [frameGen] :: reduceConfig c := rfl
753 rw [wellFormed, h]
754 refine Bool.and_eq_true _ _ ▸ ⟨?_, ?_⟩
755 · rw [List.all_cons, all_isReduced_reduceConfig]
756 rfl
757 · simp
758
759/-- Spelling is not content: normalising the loops leaves the invariant alone. -/
760theorem invariant_reduceConfig (T : Table) (hT : Table.ok T = true) (c : Config) :
761 invariant T (reduceConfig c) = invariant T c := by
762 have h : evalConfig T (reduceConfig c) = evalConfig T c := by
763 simp only [evalConfig, reduceConfig, List.map_map]
764 apply List.map_congr_left
765 intro w _
766 simp only [Function.comp_apply, evalWord_reduceWord T hT]
767 simp only [invariant, h]
768
769-- ---------------------------------------------------------------------------
770-- the depth one reading, for comparison
771-- ---------------------------------------------------------------------------
772
773/-- Exponent sums: the abelianisation, which is the unique canonical quotient and the
774reading that a bag of faces performs. -/
775def abel (w : Word) : List Int :=
776 (List.range 5).map (fun i =>
777 (w.filter (fun x => x = (i + 1 : Int))).length -
778 (w.filter (fun x => x = -(i + 1 : Int))).length)
779
780def leLexInt : List Int → List Int → Bool
781 | [], _ => true
782 | _ :: _, [] => false
783 | x :: xs, y :: ys => if x < y then true else if y < x then false else leLexInt xs ys
784
785def insertLex (v : List Int) : List (List Int) → List (List Int)
786 | [] => [v]
787 | u :: t => if leLexInt v u then v :: u :: t else u :: insertLex v t
788
789def sortLex : List (List Int) → List (List Int)
790 | [] => []
791 | v :: t => insertLex v (sortLex t)
792
793/-- The depth one reading of an utterance: the multiset of abelianised loops. -/
794def abelBag (c : Config) : List (List Int) := sortLex (c.map abel)
795
796#print axioms isReduced_reduceWord
797#print axioms wellFormed_reduceConfig_frame
798#print axioms invariantOf_perm
799#print axioms invariant_conjWord
800#print axioms invariant_map_invWord
801#print axioms invariant_substConfig
802#print axioms invariant_reduceConfig
803
804end Loom
805end IndisputableMonolith
806