The Spectre Knot the proofPictures and ideas →
Draft proof, not peer reviewed. What has been checked

lean/SpectreKnot/Parity.lean

632 lines · 38 declarations, each with its own page · on GitHub ·

The parity lemma (the paper's Prop 7.4, by Lemmas 7.1 and 7.2). For every level m ≥ 1, every kind and both signs, the composition with the level-m lengths (ℓ_m, d_m), its children carrying the signature, has the signature itself (parity_lemma; prop_7_4 reads it at Table 3's rim positions).

← SpectreKnot/CompSig.leanSpectreKnot/PatchSig.lean →

All 39 files, and the declarations of this one
1/-
2**The parity lemma** (the paper's Prop 7.4, by Lemmas 7.1 and 7.2). For every level `m ≥ 1`, every kind and both
3signs, the composition with the level-`m` lengths `(ℓ_m, d_m)`, its children carrying the signature, has the signature
4itself (`parity_lemma`; `prop_7_4` reads it at Table 3's rim positions).
5
6Proof, as in the paper. The pairs `(L, d)` reached from `(ℓ₁, d₁)` by moves are the admissible ones (`Adm`): a move adds
7two edges to a pair of glued sides (or to one side on the parent's rim), and two to `d` if it adds them before the Σ
8corner. The level-`m` lengths are admissible (`adm_level`, Lemma 7.2(a)), and a property that holds at `(ℓ₁, d₁)` and is
9kept by the moves holds at every admissible pair (`adm_induct`, Lemma 7.2(b)). The signature holds at `(ℓ₁, d₁)` by
10Computation 7.3 (`sig_base`), and a move keeps it (Lemma 7.1, `Move.OK.keep`): a move is the same as cutting one edge
11into three (`Move.OK.equiv`), and cutting keeps the signature (`Cut.OK.sig`). So every admissible pair has it
12(`adm_sig`). The junction map (`StepMap.lean`, Lemma 9.3) is carried to every level by `adm_induct` too.
13-/
17namespace SpectreKnot.Compose
19open Gluing Pattern
21/-! ### Facts from the tables -/
23/-- The Σ child of each kind. -/
24def sigIdx : Kind → Nat
25 | .Gamma => 3
26 | _ => 4
28/-- `sigIdx T` is a child of kind `T`, and it is the Σ child (checked by `decide`). -/
29theorem sigIdx_spec : ∀ T : Kind, sigIdx T < nk T ∧ kidAt T (sigIdx T) = .Sigma := by
30 intro T; cases T <;> decide
32/-- Each kind has only one Σ child. -/
33theorem sigma_unique : ∀ T : Kind, ∀ c, c < nk T → ∀ c', c' < nk T → kidAt T c = .Sigma → kidAt T c' = .Sigma →
34 c = c' := by
35 intro T; cases T <;> decide
37/-- Table 2 glues sides with the same letter. -/
38def pairOk (T : Kind) (c j : Nat) : Bool :=
39 match adjAt T c j with
40 | none => true
41 | some (c', j') => letterOf (kidAt T c') j' == letterOf (kidAt T c) j
43/-- Table 2 glues sides with the same letter, at every side of every child of every kind (checked by `decide`). -/
44theorem pair_ok : ∀ T : Kind, ∀ c, c < nk T → ∀ j, j < 6 → pairOk T c j = true := by
45 intro T; cases T <;> decide
47/-- Sides glued by Table 2 carry the same letter. -/
48theorem pair_letter {T : Kind} {c j c' j' : Nat} (c_lt : c < nk T) (j_lt : j < 6)
49 (glued : adjAt T c j = some (c', j')) : letterOf (kidAt T c') j' = letterOf (kidAt T c) j := by
50 -- the table check at `(c, j)`
51 have table := pair_ok T c c_lt j j_lt
52 simp only [pairOk, glued, beq_iff_eq] at table
53 exact table
55/-! ### Sums -/
57/-- `tot n f = f 0 + … + f (n-1)`. -/
58def tot : Nat → (Nat → Nat) → Nat
59 | 0, _ => 0
60 | n + 1, f => tot n f + f n
62/-- Sums are monotone: if `f ≤ g` term by term, then `tot n f ≤ tot n g`. -/
63theorem tot_le {n : Nat} {f g : Nat → Nat} (le_termwise : ∀ i, i < n → f i ≤ g i) : tot n f ≤ tot n g := by
64 induction n with
65 | zero => exact Nat.le_refl _
66 | succ n ih =>
67 simp only [tot]
68 -- the first `n` terms
69 have := ih (fun i i_lt => le_termwise i (by omega))
70 -- the last term
71 have := le_termwise n (by omega)
72 omega
74/-- If `f ≤ g` term by term, and strictly at one term, then `tot n f < tot n g`. -/
75theorem tot_lt {n : Nat} {f g : Nat → Nat} (le_termwise : ∀ i, i < n → f i ≤ g i) {i : Nat} (i_lt : i < n)
76 (lt_at_i : f i < g i) : tot n f < tot n g := by
77 induction n with
78 | zero => omega
79 | succ n ih =>
80 simp only [tot]
81 by_cases is_last : i = n
82 · subst is_last
83 -- the terms before the strict one
84 have := tot_le (n := i) (fun k k_lt => le_termwise k (by omega))
85 omega
86 -- the strict term is among the first `n`
87 · have := ih (fun k k_lt => le_termwise k (by omega)) (by omega)
88 -- the last term
89 have := le_termwise n (by omega)
90 omega
92/-- A sum that is not zero has a term that is not zero. -/
93theorem tot_ne_zero {n : Nat} {f : Nat → Nat} (ne_zero : tot n f ≠ 0) : ∃ i, i < n ∧ f i ≠ 0 := by
94 induction n with
95 | zero => exact absurd rfl ne_zero
96 | succ n ih =>
97 simp only [tot] at ne_zero
98 by_cases last_zero : f n = 0
99 · obtain ⟨i, i_lt, term_ne⟩ := ih (by omega)
100 exact ⟨i, by omega, term_ne⟩
101 · exact ⟨n, by omega, last_zero⟩
103/-- A sum that is zero has only zero terms. -/
104theorem tot_eq_zero {n : Nat} {f : Nat → Nat} (eq_zero : tot n f = 0) : ∀ i, i < n → f i = 0 := by
105 induction n with
106 | zero => intro i i_lt; omega
107 | succ n ih =>
108 simp only [tot] at eq_zero
109 intro i i_lt
110 by_cases is_last : i = n
111 · subst is_last; omega
112 · exact ih (by omega) i (by omega)
114/-! ### Admissible lengths -/
116/-- The level-1 side lengths ℓ₁. -/
117abbrev L₁ (T : Kind) (c j : Nat) : Nat := letterLen 1 (letterOf (kidAt T c) j)
In the paper Lemma 7.2 Reachability
119/-- Side lengths `L` and Σ offset `d` reachable from `(ℓ₁, d₁)` by moves: every side at least as long as at level 1
120and of the same parity, glued sides equally long, `d ≥ d₁` of the same parity, and the rest of the Σ child's side 5
121past its corner at least as long as at level 1. -/
122structure Adm (T : Kind) (L : Nat → Nat → Nat) (d : Nat) : Prop where
123 len : ∀ c, c < nk T → ∀ j, j < 6 → L₁ T c j ≤ L c j ∧ (L c j - L₁ T c j) % 2 = 0
124 pair : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j
125 d_ge : dOff 1 ≤ d
126 d_par : (d - dOff 1) % 2 = 0
127 sig : ∀ c, c < nk T → kidAt T c = .Sigma → d + L₁ T c 5 ≤ L c 5 + dOff 1
129/-- How far `L` is from `ℓ₁`. -/
130def excess (T : Kind) (L : Nat → Nat → Nat) : Nat := tot (nk T) fun c => tot 6 fun j => L c j - L₁ T c j
132/-- Every level-1 side has at least 5 edges (Lemma 6.5). -/
133theorem L₁_ge (T : Kind) (c j : Nat) : 5 ≤ L₁ T c j := (bounds 1 (by omega)).1 _
135/-- At level 1, side 5 of the Σ child has 10 edges. -/
136theorem L₁_sig {T : Kind} {c : Nat} (is_sigma : kidAt T c = .Sigma) : L₁ T c 5 = 10 := by
137 show letterLen 1 (letterOf (kidAt T c) 5) = 10; rw [is_sigma]; rfl
139/-- The level-1 Σ offset is `d₁ = 6`. -/
140theorem dOff_one : dOff 1 = 6 := rfl
142/-- A composition depends only on the lengths of actual sides (and on `d` only through its Σ child). -/
143theorem ofLens_congr {T : Kind} {L L' : Nat → Nat → Nat} {d d' : Nat} {ω : Bool}
144 (same_len : ∀ c, c < nk T → ∀ j, j < 6 → L c j = L' c j)
145 (same_d : ∀ c, c < nk T → kidAt T c = .Sigma → d = d') :
146 Comp.ofLens T L d ω = Comp.ofLens T L' d' ω := by
148 congr 1
149 apply List.map_congr_left
150 intro c c_lt
151 rw [List.mem_range] at c_lt
152 -- the six side lengths of child `c` agree
153 have same_sides : (List.range 6).map (L c) = (List.range 6).map (L' c) :=
154 List.map_congr_left (fun j j_mem => same_len c c_lt j (List.mem_range.mp j_mem))
155 rw [same_sides]
156 by_cases is_sigma : kidAt T c = .Sigma
157 · rw [same_d c c_lt is_sigma]
158 · simp only [mkKidL, is_sigma, ite_false]
160/-! ### Undoing a move -/
162namespace Move
164variable {T : Kind} {μ : Move}
166/-- The side lengths before the move. -/
167def shorten (T : Kind) (μ : Move) (L : Nat → Nat → Nat) (c j : Nat) : Nat := L c j - if μ.Hit T c j then 2 else 0
169/-- If a side is lengthened, so is the side glued to it. -/
170theorem hit_partner_mp (c₀_lt : μ.c₀ < nk T) (j₀_lt : μ.j₀ < 6) {c j c' j' : Nat}
171 (glued : adjAt T c j = some (c', j')) (hit : μ.Hit T c j) : μ.Hit T c' j' := by
172 rcases hit with ⟨rfl, rfl⟩ | ⟨side_glued, rfl, rfl⟩
173 -- (c, j) = (c₀, j₀): Table 2 glues it to the sibling's side, which is hit
174 · have partner := adj₀ (T := T) (μ := μ)
175 rw [glued] at partner
176 by_cases side_glued : μ.two T = true
177 · rw [ite_eq_left side_glued] at partner
178 simp only [Option.some.injEq, Prod.mk.injEq] at partner
179 exact Or.inr ⟨side_glued, partner.1, partner.2⟩
180 · rw [ite_eq_right side_glued] at partner; contradiction
181 -- (c, j) = (c₁, j₁): Table 2 glues side `j₀` of `c₀` to it
182 · have sib_glued := adj₀ (T := T) (μ := μ)
183 rw [ite_eq_left side_glued] at sib_glued
184 -- so the sibling's side is glued back to side `j₀` of `c₀`
185 have glued_back := (adj_valid c₀_lt j₀_lt sib_glued).2.2.2
186 rw [glued] at glued_back
187 simp only [Option.some.injEq, Prod.mk.injEq] at glued_back
188 exact Or.inl ⟨glued_back.1, glued_back.2⟩
190/-- Glued sides are both lengthened or both not. -/
191theorem hit_partner (c₀_lt : μ.c₀ < nk T) (j₀_lt : μ.j₀ < 6) {c j c' j' : Nat} (c_lt : c < nk T) (j_lt : j < 6)
192 (glued : adjAt T c j = some (c', j')) : μ.Hit T c j ↔ μ.Hit T c' j' :=
193 ⟨hit_partner_mp c₀_lt j₀_lt glued, hit_partner_mp c₀_lt j₀_lt (adj_valid c_lt j_lt glued).2.2.2⟩
195variable {L : Nat → Nat → Nat} {d : Nat}
197/-- The sides lengthened are at least two edges longer than at level 1. -/
198theorem hit_big (adm : Adm T L d) (c₀_lt : μ.c₀ < nk T) (j₀_lt : μ.j₀ < 6) (long₀ : L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀)
199 {c j : Nat} (hit : μ.Hit T c j) : L₁ T c j + 2 ≤ L c j := by
200 rcases hit with ⟨rfl, rfl⟩ | ⟨side_glued, rfl, rfl⟩
201 · exact long₀
202 -- the sibling's side: Table 2 glues side `j₀` of `c₀` to it
203 · have glued := adj₀ (T := T) (μ := μ)
204 rw [ite_eq_left side_glued] at glued
205 rw [adm.pair _ c₀_lt _ j₀_lt _ _ glued]
206 show letterLen 1 (letterOf (kidAt T (μ.c₁ T)) (μ.j₁ T)) + 2 ≤ _
207 rw [pair_letter c₀_lt j₀_lt glued]
208 exact long₀
210/-- Undoing a move and then making it gives back `L`. -/
211theorem lens_shorten (adm : Adm T L d) (c₀_lt : μ.c₀ < nk T) (j₀_lt : μ.j₀ < 6)
212 (long₀ : L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀) : μ.lens T (μ.shorten T L) = L := by
213 funext c j
214 simp only [lens, shorten]
215 by_cases hit : μ.Hit T c j
216 -- a side lengthened has at least two edges to spare
217 · have := hit_big adm c₀_lt j₀_lt long₀ hit
218 rw [ite_eq_left hit]; omega
219 · rw [ite_eq_right hit]; omega
221/-- Undoing a move from admissible lengths gives admissible lengths, with any Σ offset `d₀` that suits them. -/
222theorem adm_shorten (adm : Adm T L d) (c₀_lt : μ.c₀ < nk T) (j₀_lt : μ.j₀ < 6)
223 (long₀ : L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀) {d₀ : Nat} (d₀_ge : dOff 1 ≤ d₀) (d₀_par : (d₀ - dOff 1) % 2 = 0)
224 (sig_room : ∀ c, c < nk T → kidAt T c = .Sigma → d₀ + L₁ T c 5 ≤ μ.shorten T L c 5 + dOff 1) :
225 Adm T (μ.shorten T L) d₀ where
226 len c c_lt j j_lt := by
227 -- the side is as long as at level 1 or longer, by an even number of edges
228 have := adm.len c c_lt j j_lt
229 simp only [shorten]
230 by_cases hit : μ.Hit T c j
231 -- a side lengthened is at least two edges longer than at level 1
232 · have := hit_big adm c₀_lt j₀_lt long₀ hit
233 rw [ite_eq_left hit]; omega
234 · rw [ite_eq_right hit]; omega
235 pair c c_lt j j_lt c' j' glued := by
236 simp only [shorten]
237 rw [adm.pair c c_lt j j_lt c' j' glued]
238 by_cases hit : μ.Hit T c j
239 · rw [ite_eq_left hit, ite_eq_left ((hit_partner c₀_lt j₀_lt c_lt j_lt glued).mp hit)]
240 · rw [ite_eq_right hit,
241 ite_eq_right (fun partner_hit => hit ((hit_partner c₀_lt j₀_lt c_lt j_lt glued).mpr partner_hit))]
242 d_ge := d₀_ge
243 d_par := d₀_par
244 sig := sig_room
246/-- Undoing a move lowers the excess over the level-1 lengths. -/
247theorem excess_shorten (adm : Adm T L d) (c₀_lt : μ.c₀ < nk T) (j₀_lt : μ.j₀ < 6)
248 (long₀ : L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀) : excess T (μ.shorten T L) < excess T L := by
249 unfold excess
250 -- no side's excess grows
251 have no_growth : ∀ c j, μ.shorten T L c j - L₁ T c j ≤ L c j - L₁ T c j := fun c j => by
252 simp only [shorten]; omega
253 refine tot_lt (fun c _ => tot_le (fun j _ => no_growth c j)) c₀_lt (tot_lt (fun j _ => no_growth _ j) j₀_lt ?_)
254 simp only [shorten]
255 rw [ite_eq_left (show μ.Hit T μ.c₀ μ.j₀ from Or.inl ⟨rfl, rfl⟩)]
256 omega
In the paper Lemma 7.1 Lengthening
258/-- **Lemma 7.1**: a move keeps the signature. -/
259theorem OK.keep {ω : Bool} (move_ok : μ.OK T L d ω) (has_sig : Sig (Comp.ofLens T L d ω).toGluing (nk T - 1)) :
260 Sig (Comp.ofLens T (μ.lens T L) (μ.d' T L d) ω).toGluing (nk T - 1) :=
261 move_ok.equiv.symm.sig (move_ok.cutOK.sig has_sig)
263/-- The conditions of a move from the shortened lengths: a move cutting side `j₀` of child `c₀` at offset `r₀`, at
264least one edge from its start and three from its end (with the lengths after the move), can be made at admissible
265shortened lengths whose composition is well formed, if it is clear of the Σ corner. -/
266theorem mkOK {ω : Bool} (hc₀ : μ.c₀ < nk T) (hj₀ : μ.j₀ < 6)
267 (r₀_pos : 1 ≤ μ.r₀) (r₀_room : μ.r₀ + 4 ≤ L μ.c₀ μ.j₀) {d₀ : Nat} (adm₀ : Adm T (μ.shorten T L) d₀)
268 (cut₀ : kidAt T μ.c₀ = .Sigma → μ.j₀ = 5 → d₀ + 1 ≤ μ.r₀ ∨ μ.r₀ + 2 ≤ d₀)
269 (cut₁ : μ.two T = true → kidAt T (μ.c₁ T) ≠ .Sigma ∨ μ.j₁ T ≠ 5)
270 (wf₀ : (Comp.ofLens T (μ.shorten T L) d₀ ω).toGluing.WF) : μ.OK T (μ.shorten T L) d₀ ω :=
271 { wf := wf₀
272 pos_len := fun c hc j hj => by
273 -- each side is at least as long as at level 1
274 have := (adm₀.len c hc j hj).1
275 -- where it has at least 5 edges
276 have := L₁_ge T c j
277 omega
278 pair := adm₀.pair
279 c₀ := hc₀
280 j₀ := hj₀
281 r₀ := r₀_pos
282 r₀' := by simp only [shorten]; rw [ite_eq_left (show μ.Hit T μ.c₀ μ.j₀ from Or.inl ⟨rfl, rfl⟩)]; omega
283 sig := fun c hc is_sigma => by
284 -- room for the Σ corner on side 5, as at level 1
285 have := adm₀.sig c hc is_sigma
286 -- and `d₀ ≥ d₁`
287 have := adm₀.d_ge
288 rw [L₁_sig is_sigma, dOff_one] at *
289 omega
290 sig1 := fun c c' hc hc' is_sigma is_sigma' => sigma_unique T c hc c' hc' is_sigma is_sigma'
291 cut₀ := cut₀
292 cut₁ := fun shared is_sigma side_five => by
293 rcases cut₁ shared with not_sigma | not_five <;> contradiction }
295end Move
297/-! ### The induction (Lemma 7.2) -/
In the paper Lemma 7.2 Reachability
299/-- **Lemma 7.2(b), as an induction principle** (with `adm_level`, Lemma 7.2(a), below). A property of `(L, d)` that
300holds at `(ℓ₁, d₁)`, depends only on the lengths of actual sides (and on `d` only through the Σ child), and is kept by
301every move whose cut is two edges clear of both ends of its side or lies on the Σ child's side 5, holds at every
302admissible `(L, d)`.
304By induction on the excess over `ℓ₁` (the paper's induction on `∑ L`): from an admissible `(L, d) ≠ (ℓ₁, d₁)`, undo a
305move, chosen as in the paper: the third edge of a long side; on the Σ child's side 5, the second edge before the corner
306if `d ≥ d₁ + 2`, the second after it if `d = d₁`. The induction also carries that the composition is well formed
307(`Gluing.WF`), which a move needs (`Move.OK`): at `(ℓ₁, d₁)` by Computation 7.3 (`sig_base`), and after a move because
308the composition is then the old one with an edge cut (`Move.OK.equiv`). -/
309theorem adm_induct (T : Kind) (ω : Bool) (P : (Nat → Nat → Nat) → Nat → Prop)
310 (congr : ∀ L L' d d', (∀ c, c < nk T → ∀ j, j < 6 → L c j = L' c j) →
311 (∀ c, c < nk T → kidAt T c = .Sigma → d = d') → P L' d' → P L d)
312 (base : P (L₁ T) (dOff 1))
313 (step : ∀ (μ : Move) (L : Nat → Nat → Nat) (d : Nat), μ.OK T L d ω →
314 ((2 ≤ μ.r₀ ∧ μ.r₀ + 3 ≤ L μ.c₀ μ.j₀) ∨ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5)) → P L d →
315 P (μ.lens T L) (μ.d' T L d)) :
316 ∀ L d, Adm T L d → P L d := by
317 -- by induction on the excess, carrying along that the composition is well formed
318 suffices carried : ∀ N L d, excess T L < N → Adm T L d → P L d ∧ (Comp.ofLens T L d ω).toGluing.WF from
319 fun L d adm => (carried _ L d (Nat.lt_succ_self _) adm).1
320 intro N
321 induction N with
322 | zero => intro L d below_zero; omega
323 | succ N ih =>
324 intro L d excess_lt adm
325 -- the Σ child is an actual child, of kind Σ
326 obtain ⟨sig_lt, sig_kind⟩ := sigIdx_spec T
327 -- `d₁ = 6`
328 have d₁_eq := dOff_one
329 by_cases at_base : excess T L = 0
330 · -- the base case: `(L, d) = (ℓ₁, d₁)`
331 -- every side is as long as at level 1
332 have is_L₁ : ∀ c, c < nk T → ∀ j, j < 6 → L c j = L₁ T c j := fun c hc j hj => by
333 -- no excess on side `j` of child `c`
334 have := tot_eq_zero (tot_eq_zero at_base c hc) j hj
335 -- and the side is at least as long as at level 1
336 have := (adm.len c hc j hj).1
337 omega
338 -- and the Σ offset is `d₁`
339 have is_d₁ : d = dOff 1 := by
340 -- room for the Σ corner on side 5
341 have := adm.sig _ sig_lt sig_kind
342 -- which is as long as at level 1
343 have := is_L₁ _ sig_lt 5 (by omega)
344 -- and `d ≥ d₁`
345 have := adm.d_ge
346 omega
347 -- so the property holds, and the composition is that of Computation 7.3, which is well formed
348 refine ⟨congr L (L₁ T) d (dOff 1) is_L₁ (fun _ _ _ => is_d₁) base, ?_⟩
349 rw [ofLens_congr is_L₁ (fun _ _ _ => is_d₁)]
350 exact (sig_base T ω).wf
351 · -- a side longer than at level 1
352 obtain ⟨c, hc, child_excess⟩ := tot_ne_zero at_base
353 obtain ⟨j, hj, side_excess⟩ := tot_ne_zero child_excess
354 -- side `j` of child `c` is at least two edges longer than at level 1
355 have longer : L₁ T c j + 2 ≤ L c j := by
356 -- it is at least as long, with the same parity
357 have := adm.len c hc j hj
358 omega
359 -- one step back
360 have back : ∀ μ : Move, μ.c₀ < nk T → μ.j₀ < 6 → L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀ → 1 ≤ μ.r₀ →
361 μ.r₀ + 4 ≤ L μ.c₀ μ.j₀ → ∀ d₀, Adm T (μ.shorten T L) d₀ →
362 (kidAt T μ.c₀ = .Sigma → μ.j₀ = 5 → d₀ + 1 ≤ μ.r₀ ∨ μ.r₀ + 2 ≤ d₀) →
363 (μ.two T = true → kidAt T (μ.c₁ T) ≠ .Sigma ∨ μ.j₁ T ≠ 5) → μ.d' T (μ.shorten T L) d₀ = d →
364 ((2 ≤ μ.r₀ ∧ μ.r₀ + 5 ≤ L μ.c₀ μ.j₀) ∨ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5)) →
365 P L d ∧ (Comp.ofLens T L d ω).toGluing.WF := by
366 intro μ hc₀ hj₀ big r₀_pos r₀_room d₀ adm₀ cut₀ cut₁ d_after clear
367 -- the induction hypothesis: at the shortened lengths, which have less excess, the property holds and the
368 -- composition is well formed
369 obtain ⟨holds₀, wf₀⟩ := ih _ _ (by
370 -- shortening lowers the excess
371 have := Move.excess_shorten adm hc₀ hj₀ big
372 omega) adm₀
373 -- so the move can be made from the shortened lengths
374 have move_ok : μ.OK T (μ.shorten T L) d₀ ω := Move.mkOK hc₀ hj₀ r₀_pos r₀_room adm₀ cut₀ cut₁ wf₀
375 -- side `j₀` of `c₀` is two edges shorter before the move
376 have shortened : μ.shorten T L μ.c₀ μ.j₀ = L μ.c₀ μ.j₀ - 2 := by
377 simp only [Move.shorten]; rw [ite_eq_left (show μ.Hit T μ.c₀ μ.j₀ from Or.inl ⟨rfl, rfl⟩)]
378 -- the property survives the move
379 have after := step μ _ _ move_ok (by
380 rw [shortened]
381 rcases clear with clear_ends | on_sigma_five
382 · exact Or.inl ⟨clear_ends.1, by omega⟩
383 · exact Or.inr on_sigma_five) holds₀
384 -- and the composition after it is the old one with an edge cut, so it is well formed
385 have wf_after := move_ok.equiv.symm.wf move_ok.cutOK.wf_subdiv
386 rw [Move.lens_shorten adm hc₀ hj₀ big, d_after] at after wf_after
387 exact ⟨after, wf_after⟩
388 -- the sibling glued to side 5 of the Σ child is not the Σ child
389 have sib_not_sig : ∀ μ : Move, μ.c₀ = sigIdx T → μ.j₀ = 5 → μ.two T = true → kidAt T (μ.c₁ T) ≠ .Sigma := by
390 intro μ on_sigma side_five shared sib_sigma
391 -- Table 2 glues side `j₀` of `c₀` to side `j₁` of `c₁`
392 have sib := Move.adj₀ (T := T) (μ := μ)
393 rw [ite_eq_left shared] at sib
394 -- the sibling is an actual child, other than `c₀`
395 have sib_valid := adj_valid (on_sigma ▸ sig_lt) (by omega) sib
396 exact sib_valid.2.2.1 (sigma_unique T _ sib_valid.1 _ (on_sigma ▸ sig_lt) sib_sigma (on_sigma ▸ sig_kind))
397 by_cases on_sig_five : (c = sigIdx T ∧ j = 5) ∨ adjAt T c j = some (sigIdx T, 5)
398 · -- a move on the Σ child's side 5
399 -- that side is at least two edges longer than at level 1
400 have big : L₁ T (sigIdx T) 5 + 2 ≤ L (sigIdx T) 5 := by
401 rcases on_sig_five with ⟨rfl, rfl⟩ | glued_to
402 · exact longer
403 · rw [adm.pair c hc j hj _ _ glued_to]
404 show letterLen 1 (letterOf (kidAt T (sigIdx T)) 5) + 2 ≤ _
405 rw [pair_letter hc hj glued_to]; exact longer
406 -- side 5 of the Σ child has 10 edges at level 1
407 have sig_five := L₁_sig sig_kind
408 -- room for the Σ corner on side 5
409 have corner_room := adm.sig _ sig_lt sig_kind
410 -- `d ≥ d₁`
411 have d_ge := adm.d_ge
412 -- and `d` has the parity of `d₁`
413 have d_par := adm.d_par
414 by_cases d_big : dOff 1 + 2 ≤ d
415 · -- cut the edge at offset 1, before the Σ corner, which moves back by 2
416 obtain ⟨μ, μ_c₀, μ_j₀, μ_r₀⟩ : ∃ μ : Move, μ.c₀ = sigIdx T ∧ μ.j₀ = 5 ∧ μ.r₀ = 1 :=
417 ⟨⟨_, 5, 1⟩, rfl, rfl, rfl⟩
418 have hc₀ : μ.c₀ < nk T := μ_c₀ ▸ sig_lt -- the Σ child is an actual child
419 have hj₀ : μ.j₀ < 6 := by omega -- and side 5 is a side
420 -- the side cut is at least two edges longer than at level 1
421 have big' : L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀ := by rw [μ_c₀, μ_j₀]; exact big
422 -- before the move it is two edges shorter
423 have shortened : μ.shorten T L (sigIdx T) 5 = L (sigIdx T) 5 - 2 := by
424 simp only [Move.shorten]; rw [ite_eq_left (show μ.Hit T (sigIdx T) 5 from Or.inl ⟨μ_c₀.symm, μ_j₀.symm⟩)]
425 -- the shortened lengths, with `d - 2`, are admissible
426 have adm₀ : Adm T (μ.shorten T L) (d - 2) :=
427 Move.adm_shorten adm hc₀ hj₀ big' (by omega) (by omega) (fun c' hc' is_sigma => by
428 rw [sigma_unique T _ hc' _ sig_lt is_sigma sig_kind, shortened, sig_five]; omega)
429 refine back μ hc₀ hj₀ big' (by omega) (by rw [μ_c₀, μ_j₀, μ_r₀]; omega) _ adm₀
430 (fun _ _ => Or.inr (by omega)) (fun shared => Or.inl (sib_not_sig μ μ_c₀ μ_j₀ shared)) ?_
431 (Or.inr ⟨by rw [μ_c₀]; exact sig_kind, μ_j₀⟩)
432 -- the move puts the Σ corner back at `d`
433 have new_d := Move.d'_c₀ (L := μ.shorten T L) (d := d - 2) (by rw [μ_c₀]; exact sig_kind) μ_j₀
434 (fun ⟨shared, is_sigma, _⟩ => sib_not_sig μ μ_c₀ μ_j₀ shared is_sigma)
435 rw [ite_eq_left (by omega)] at new_d; omega
436 · -- `d = d₁`: cut the edge just after the Σ corner, which stays put
437 have is_d₁ : d = dOff 1 := by omega -- `d` has the parity of `d₁`
438 obtain ⟨μ, μ_c₀, μ_j₀, μ_r₀⟩ : ∃ μ : Move, μ.c₀ = sigIdx T ∧ μ.j₀ = 5 ∧ μ.r₀ = d + 1 :=
439 ⟨⟨_, 5, d + 1⟩, rfl, rfl, rfl⟩
440 have hc₀ : μ.c₀ < nk T := μ_c₀ ▸ sig_lt -- the Σ child is an actual child
441 have hj₀ : μ.j₀ < 6 := by omega -- and side 5 is a side
442 -- the side cut is at least two edges longer than at level 1
443 have big' : L₁ T μ.c₀ μ.j₀ + 2 ≤ L μ.c₀ μ.j₀ := by rw [μ_c₀, μ_j₀]; exact big
444 -- before the move it is two edges shorter
445 have shortened : μ.shorten T L (sigIdx T) 5 = L (sigIdx T) 5 - 2 := by
446 simp only [Move.shorten]; rw [ite_eq_left (show μ.Hit T (sigIdx T) 5 from Or.inl ⟨μ_c₀.symm, μ_j₀.symm⟩)]
447 -- the shortened lengths, with the same `d`, are admissible
448 have adm₀ : Adm T (μ.shorten T L) d :=
449 Move.adm_shorten adm hc₀ hj₀ big' d_ge d_par (fun c' hc' is_sigma => by
450 rw [sigma_unique T _ hc' _ sig_lt is_sigma sig_kind, shortened, sig_five]; omega)
451 refine back μ hc₀ hj₀ big' (by omega) (by rw [μ_c₀, μ_j₀, μ_r₀]; omega) _ adm₀
452 (fun _ _ => Or.inl (by omega)) (fun shared => Or.inl (sib_not_sig μ μ_c₀ μ_j₀ shared)) ?_
453 (Or.inr ⟨by rw [μ_c₀]; exact sig_kind, μ_j₀⟩)
454 -- the move leaves the Σ corner at `d`
455 have new_d := Move.d'_c₀ (L := μ.shorten T L) (d := d) (by rw [μ_c₀]; exact sig_kind) μ_j₀
456 (fun ⟨shared, is_sigma, _⟩ => sib_not_sig μ μ_c₀ μ_j₀ shared is_sigma)
457 rw [ite_eq_right (by omega)] at new_d; omega
458 · -- a move elsewhere, cutting the third edge of the side
459 obtain ⟨μ, μ_c₀, μ_j₀, μ_r₀⟩ : ∃ μ : Move, μ.c₀ = c ∧ μ.j₀ = j ∧ μ.r₀ = 2 := ⟨⟨c, j, 2⟩, rfl, rfl, rfl⟩
460 subst μ_c₀ μ_j₀
461 -- every side has at least 5 edges at level 1
462 have L₁_five := L₁_ge T μ.c₀ μ.j₀
463 -- the side cut is not the Σ child's side 5
464 have not_sig_five₀ : ¬ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5) := fun ⟨is_sigma, side_five⟩ =>
465 on_sig_five (Or.inl ⟨sigma_unique T _ hc _ sig_lt is_sigma sig_kind, side_five⟩)
466 -- nor is the sibling's side glued to it
467 have not_sig_five₁ : ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma ∧ μ.j₁ T = 5) := by
468 rintro ⟨shared, is_sigma, side_five⟩
469 -- Table 2 glues side `j₀` of `c₀` to side `j₁` of `c₁`
470 have sib := Move.adj₀ (T := T) (μ := μ)
471 rw [ite_eq_left shared] at sib
472 -- the sibling is an actual child
473 have sib_valid := adj_valid hc hj sib
474 rw [sigma_unique T _ sib_valid.1 _ sig_lt is_sigma sig_kind, side_five] at sib
475 exact on_sig_five (Or.inr sib)
476 -- so the move leaves the Σ child's side 5 alone
477 have sig_not_hit : ¬ μ.Hit T (sigIdx T) 5 := by
478 rintro (⟨is_c₀, is_j₀⟩ | ⟨shared, is_c₁, is_j₁⟩)
479 · exact not_sig_five₀ ⟨is_c₀ ▸ sig_kind, is_j₀.symm⟩
480 · exact not_sig_five₁ ⟨shared, is_c₁ ▸ sig_kind, is_j₁.symm⟩
481 -- the Σ child's side 5 is as long before the move as after
482 have unchanged : μ.shorten T L (sigIdx T) 5 = L (sigIdx T) 5 := by
483 simp only [Move.shorten]; rw [ite_eq_right sig_not_hit]; omega
484 -- the shortened lengths, with the same `d`, are admissible
485 have adm₀ : Adm T (μ.shorten T L) d :=
486 Move.adm_shorten adm hc hj longer adm.d_ge adm.d_par (fun c' hc' is_sigma => by
487 rw [sigma_unique T _ hc' _ sig_lt is_sigma sig_kind, unchanged]; exact adm.sig _ sig_lt sig_kind)
488 refine back μ hc hj longer (by omega) (by omega) _ adm₀
489 (fun is_sigma side_five => absurd ⟨is_sigma, side_five⟩ not_sig_five₀) (fun shared => ?_)
490 (Move.d'_eq not_sig_five₀ not_sig_five₁) (Or.inl ⟨by omega, by omega⟩)
491 by_cases is_sigma : kidAt T (μ.c₁ T) = .Sigma
492 · exact Or.inr (fun side_five => not_sig_five₁ ⟨shared, is_sigma, side_five⟩)
493 · exact Or.inl is_sigma
In the paper Proposition 7.4 Compositions at every level
495/-- **Every admissible `(L, d)` has the signature**: it holds at `(ℓ₁, d₁)` by Computation 7.3 (`sig_base`), and a
496move keeps it by Lemma 7.1 (`Move.OK.keep`). -/
497theorem adm_sig (T : Kind) (ω : Bool) : ∀ L d, Adm T L d → Sig (Comp.ofLens T L d ω).toGluing (nk T - 1) :=
498 adm_induct T ω (fun L d => Sig (Comp.ofLens T L d ω).toGluing (nk T - 1))
499 (fun _ _ _ _ same_len same_d has_sig => by rw [ofLens_congr same_len same_d]; exact has_sig)
500 (sig_base T ω) (fun _ _ _ move_ok _ has_sig => move_ok.keep has_sig)
502/-! ### The level-`m` lengths are admissible -/
504/-- Each Fibonacci number is at most the next. -/
505theorem fib_le_succ (n : Nat) : fib n ≤ fib (n + 1) := by
506 cases n with
507 | zero => decide
508 | succ n => rw [fib_add_two]; omega
510/-- The Fibonacci numbers are monotone. -/
511theorem fib_mono {a b : Nat} (a_le_b : a ≤ b) : fib a ≤ fib b := by
512 induction b with
513 | zero =>
514 -- only `a = 0` is at most 0
515 have a_zero : a = 0 := by omega
516 subst a_zero; exact Nat.le_refl _
517 | succ b ih =>
518 by_cases a_eq : a = b + 1
519 · subst a_eq; exact Nat.le_refl _
520 · exact Nat.le_trans (ih (by omega)) (fib_le_succ b)
522/-- Letter lengths only grow, and keep their parities. -/
523theorem letterLen_ge (m : Nat) (m_pos : 1 ≤ m) (x : Letter) :
524 letterLen 1 x ≤ letterLen m x ∧ (letterLen m x - letterLen 1 x) % 2 = 0 := by
525 -- the closed forms of the eight letter lengths (Prop 6.2)
526 obtain ⟨len_a, len_b, len_g, len_d, len_e, len_z, len_h, len_t⟩ := letterLen_fib m m_pos
527 -- and their parities (Cor 6.3)
528 obtain ⟨par_a, par_b, par_g, par_d, par_e, par_z, par_h, par_t⟩ := letterLen_parity m m_pos
529 -- `F(3m+1) ≥ F(4)`
530 have fib_3m1 := fib_mono (show 4 ≤ 3 * m + 1 by omega)
531 -- `F(3m+2) ≥ F(5)`
532 have fib_3m2 := fib_mono (show 5 ≤ 3 * m + 2 by omega)
533 -- `F(3m+3) ≥ F(6)`
534 have fib_3m3 := fib_mono (show 6 ≤ 3 * m + 3 by omega)
535 -- `F(3m+4) ≥ F(7)`
536 have fib_3m4 := fib_mono (show 7 ≤ 3 * m + 4 by omega)
537 -- `F(4) = 3`
538 have fib4_eq : fib 4 = 3 := rfl
539 -- `F(5) = 5`
540 have fib5_eq : fib 5 = 5 := rfl
541 -- `F(6) = 8`
542 have fib6_eq : fib 6 = 8 := rfl
543 -- `F(7) = 13`
544 have fib7_eq : fib 7 = 13 := rfl
545 cases x <;> simp only [letterLen, letterLen1] <;> omega
In the paper Lemma 7.2 Reachability
547/-- The level-`m` lengths `(ℓ_m, d_m)` are admissible. -/
548theorem adm_level (T : Kind) (m : Nat) (m_pos : 1 ≤ m) :
549 Adm T (fun c j => letterLen m (letterOf (kidAt T c) j)) (dOff m) where
550 len c _ j _ := letterLen_ge m m_pos _
551 pair c c_lt j j_lt c' j' glued := by simp only [pair_letter c_lt j_lt glued]
552 d_ge := by
553 rw [(dOff_fib m m_pos).1, dOff_one]
554 -- `F(3m+1) ≥ F(4)`
555 have := fib_mono (show 4 ≤ 3 * m + 1 by omega)
556 -- `F(4) = 3`
557 have fib4_eq : fib 4 = 3 := rfl
558 omega
559 d_par := by rw [(dOff_fib m m_pos).1, dOff_one]; omega
560 sig c _ is_sigma := by
561 show dOff m + L₁ T c 5 ≤ letterLen m (letterOf (kidAt T c) 5) + dOff 1
562 rw [L₁_sig is_sigma, is_sigma, dOff_one, show letterOf .Sigma 5 = .delta from rfl, (dOff_fib m m_pos).2]
563 -- `F(3m) ≥ F(3)`
564 have := fib_mono (show 3 ≤ 3 * m by omega)
565 -- `F(3) = 2`
566 have fib3_eq : fib 3 = 2 := rfl
567 omega
569/-! ### The parity lemma -/
In the paper Proposition 7.4 Compositions at every level
571/-- **The parity lemma** (the paper's Prop 7.4: Computation 7.3 at every level). For every level `m ≥ 1`, every kind
572`T` and both signs `ω`: the composition of §7.1 with the level-`m` lengths `(ℓ_m, d_m)`, its children carrying the
573signature, has the signature (`Sig`): it is well formed, no strand closes up, every parent rim vertex is a hook except
574the Γ child's corners `A` and `B`, which lie on the parent's rim and carry the crossover. -/
575theorem parity_lemma (m : Nat) (m_pos : 1 ≤ m) (T : Kind) (ω : Bool) :
576 Sig (Comp.ofPattern T (letterLen m) (dOff m) ω).toGluing (nk T - 1) :=
577 adm_sig T ω _ _ (adm_level T m m_pos)
In the paper Proposition 7.4 Compositions at every level
579/-- **Prop 7.4, as the paper words it**: for every level `m ≥ 1`, every kind `T` and both signs `ω`, the composition
580`C_T(ℓ_m, d_m, ω)` has the signature (`CompSig`): the parity lemma's `Sig`, read at Table 3's rim positions. -/
581theorem prop_7_4 (m : Nat) (m_pos : 1 ≤ m) (T : Kind) (ω : Bool) :
582 Statement.CompSig T (fun c j => letterLen m (letterOf (kidAt T c) j)) (dOff m) ω :=
584 (fun c j => by
585 -- every side has at least 5 edges (Lemma 6.5)
586 have := (bounds m m_pos).1 (letterOf (kidAt T c) j)
587 omega)
588 (by
589 -- so does side 0 of the Γ child
590 have := (bounds m m_pos).1 (letterOf (kidAt T (nk T - 1)) 0)
591 omega)
592 (parity_lemma m m_pos T ω)
594/-- The corner `B` of child `c`, in terms of the composition's own rim length and corner `A`: the vertex after `A` if
595`ω`, the vertex before it otherwise. -/
596theorem ofLens_B' {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool} {c : Nat} (c_lt : c < nk T) :
597 (Comp.ofLens T L d ω).toGluing.B c =
598 if ω then nxt ((Comp.ofLens T L d ω).toGluing.E c) ((Comp.ofLens T L d ω).toGluing.A c)
599 else prv ((Comp.ofLens T L d ω).toGluing.E c) ((Comp.ofLens T L d ω).toGluing.A c) := by
600 rw [ofLens_B c_lt, ofLens_E c_lt]
602/-- In a composition with the signature, `A` and `B` are adjacent parent rim vertices: `B` comes right after `A`
603along the parent's rim (in the children's sense) if `ω`, right before it otherwise. -/
604theorem sig_adj {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool} {G : Gluing}
605 (G_eq : G = (Comp.ofLens T L d ω).toGluing) (has_sig : Sig G (nk T - 1)) :
606 if ω then G.Rot (nk T - 1, nxt (G.E (nk T - 1)) (G.A (nk T - 1))) (nk T - 1, G.B (nk T - 1))
607 else G.Rot (nk T - 1, nxt (G.E (nk T - 1)) (G.B (nk T - 1))) (nk T - 1, G.A (nk T - 1)) := by
608 -- the crossover child is a child of the composition
609 have g_lt : nk T - 1 < nk T := by
610 -- the signature says it is a child of `G`
611 have g_lt_G := has_sig.g_lt
612 rw [G_eq, ofLens_n] at g_lt_G; exact g_lt_G
613 -- `B` is the vertex after `A` if `ω`, the vertex before it otherwise
614 have B_eq : G.B (nk T - 1) = if ω then nxt (G.E (nk T - 1)) (G.A (nk T - 1))
615 else prv (G.E (nk T - 1)) (G.A (nk T - 1)) := by subst G_eq; exact ofLens_B' g_lt
616 cases ω with
617 | true =>
618 rw [ite_eq_left rfl] at B_eq ⊢
619 rw [← B_eq]; exact .stop has_sig.rimB
620 | false =>
621 rw [ite_eq_right (by decide)] at B_eq ⊢
622 rw [B_eq, nxt_prv (has_sig.wf.A_lt _ has_sig.g_lt)]; exact .stop has_sig.rimA
In the paper Proposition 7.4 Compositions at every level
624/-- **The parity lemma, adjacency**: `A` and `B` are adjacent parent rim vertices, `B` right after `A` along the
625parent's rim (in the children's sense) if `ω`, right before it otherwise. -/
626theorem parity_lemma_adj (m : Nat) (m_pos : 1 ≤ m) (T : Kind) (ω : Bool) :
627 let G := (Comp.ofPattern T (letterLen m) (dOff m) ω).toGluing
628 let g := nk T - 1
629 if ω then G.Rot (g, nxt (G.E g) (G.A g)) (g, G.B g) else G.Rot (g, nxt (G.E g) (G.B g)) (g, G.A g) :=
630 sig_adj rfl (parity_lemma m m_pos T ω)
632end SpectreKnot.Compose

← SpectreKnot/CompSig.leanSpectreKnot/PatchSig.lean →