lean/SpectreKnot/Lengths.lean
286 lines · 22 declarations, each with its own page · on GitHub ·
Side lengths (paper §6): Prop 6.1 (lengths by letter), Prop 6.2 (Fibonacci side lengths), Cor 6.3 (parities are constant), Lemma 6.4 (position of A on the Σ side), Lemma 6.5 (lower bounds).
← SpectreKnot/Zigzag.leanSpectreKnot/Compose.lean →
All 39 files, and the declarations of this one
1/-
2Side lengths (paper §6): Prop 6.1 (lengths by letter), Prop 6.2 (Fibonacci side lengths), Cor 6.3 (parities are
3constant), Lemma 6.4 (position of A on the Σ side), Lemma 6.5 (lower bounds).
5The side lengths are *defined* here from the level-1 counts and Prop 2.4(c) (a parent side is the concatenation of
6the children's sides of Table 3). Prop 2.4 itself rests on the cited spectre theorems and is not formalised. That the
7supertiles `super m K` of the statement file have these side lengths, the paper's definition of `ℓ_m`, is
8`Statement.super_side_length` (`ProofA.lean`).
9-/
10import SpectreKnot.Basic
11import SpectreKnot.Data.Pattern
13namespace SpectreKnot
15open Pattern Kind Letter
17/-- Child `c` of a `T`-supertile (Table 1). -/
20/-- The letter of side `j` of a `K`-supertile (Table 4). -/
23/-- The children's sides `(c, j)` that make up side `J` of a `T`-supertile (Table 3). -/
26/-- `sideLen m K j` = ℓ_m(K, j), the number of edges of side `j` of a level-`m` `K`-supertile (`m ≥ 1`): the level-1
27counts, and then Prop 2.4(c). (Level 0 is not a hexagon level; the value 0 there is a placeholder.) -/
29 | 0, _, _ => 0
33/-- The letters on the right-hand side of the recurrence (6.1), with multiplicity. -/
34def recLetters : Letter → List Letter
35 | .alpha => [.beta, .epsilon, .eta]
36 | .beta => [.alpha, .epsilon]
37 | .gamma => [.beta, .epsilon, .epsilon, .eta, .theta]
38 | .delta => [.alpha, .beta, .epsilon, .theta, .theta]
39 | .epsilon => [.epsilon, .epsilon, .epsilon, .eta]
40 | .zeta => [.alpha, .epsilon, .theta]
41 | .eta => [.epsilon, .epsilon, .epsilon, .epsilon, .eta]
42 | .theta => [.epsilon, .epsilon, .epsilon, .epsilon, .eta, .theta]
44/-- The level-1 letter lengths (α₁, …, θ₁) = (7, 5, 10, 10, 8, 6, 10, 11). -/
45def letterLen1 : Letter → Nat
46 | .alpha => 7 | .beta => 5 | .gamma => 10 | .delta => 10
47 | .epsilon => 8 | .zeta => 6 | .eta => 10 | .theta => 11
49/-- `letterLen m x` = x_m, the common length of the sides with letter `x` at level `m ≥ 1`, by the recurrence (6.1). -/
51 | 0, _ => 0
52 | 1, x => letterLen1 x
53 | m + 2, x => ((recLetters x).map (letterLen (m + 1))).sum
55/-! ### Prop 6.1: lengths by letter -/
57/-- The level-1 counts depend only on the letter. -/
58theorem len1_by_letter : ∀ K : Kind, ∀ j, j < 6 → (len1 K).getD j 0 = letterLen1 (letterOf K j) := by
59 intro K; cases K <;> decide
61/-- Every piece listed in Table 3 is a side `0..5` of a child. -/
62theorem pieces_valid : ∀ T : Kind, ∀ J, J < 6 → ∀ p ∈ pieces T J, p.2 < 6 := by
63 intro T; cases T <;> decide
65/-- "Inspection of Tables 1, 3, 4" in the proof of Prop 6.1: the letters of the pieces of side `J` of `T` are, up to
66order, the letters of the recurrence for the letter of side `J`. -/
67theorem pieces_perm : ∀ T : Kind, ∀ J, J < 6 →
69 intro T; cases T <;> decide
71/-- **Prop 6.1.** For every `m ≥ 1`, ℓ_m(K, j) depends only on the letter of side `j` of `K`, and the letter lengths
72satisfy (6.1). -/
73theorem sideLen_eq_letterLen (m : Nat) (level_pos : 1 ≤ m) (K : Kind) (j : Nat) (side_lt : j < 6) :
75 obtain ⟨m, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
76 clear level_pos
77 induction m generalizing K j with
78 | zero => exact len1_by_letter K j side_lt
79 | succ m ih =>
81 = ((recLetters (letterOf K j)).map (letterLen (m + 1))).sum
82 -- each piece's length is the length of its letter one level down (by induction)
85 rw [List.map_map]
86 apply List.map_congr_left
87 intro p piece_mem
88 exact ih _ _ (pieces_valid K j side_lt p piece_mem)
89 rw [by_letter]
90 exact ((pieces_perm K j side_lt).map _).sum_nat
92/-- The recurrence (6.1) written out. -/
93theorem letterLen_succ (m : Nat) :
94 letterLen (m + 2) .alpha = letterLen (m + 1) .beta + letterLen (m + 1) .epsilon + letterLen (m + 1) .eta ∧
101 letterLen (m + 2) .zeta = letterLen (m + 1) .alpha + letterLen (m + 1) .epsilon + letterLen (m + 1) .theta ∧
105 simp only [letterLen, recLetters, List.map, List.sum_cons, List.sum_nil]
106 omega
108/-! ### Prop 6.2: Fibonacci side lengths -/
110-- The Fibonacci numbers `fib`, with `fib 1 = fib 2 = 1`, are in `Basic.lean`.
112/-- The Fibonacci recurrence. -/
113theorem fib_add_two (n : Nat) : fib (n + 2) = fib n + fib (n + 1) := rfl
115/-- Prop 6.2 at level `k + 1`, with the Fibonacci indices written out (3(k+1)+1 = 3k+4, …). -/
116theorem letterLen_fib_aux (k : Nat) :
125 induction k with
126 | zero => decide
127 | succ k ih =>
128 rw [show k + 1 + 1 = k + 2 from rfl]
129 -- the closed forms at level `k + 1`, and the recurrence (6.1) from level `k + 1` to `k + 2`
130 obtain ⟨alpha_k, beta_k, gamma_k, delta_k, epsilon_k, zeta_k, eta_k, theta_k⟩ := ih
131 obtain ⟨alpha_rec, beta_rec, gamma_rec, delta_rec, epsilon_rec, zeta_rec, eta_rec, theta_rec⟩ := letterLen_succ k
132 -- the Fibonacci recurrence up to F_{3k+10}, so that `omega` can write everything in F_{3k+4} and F_{3k+5}
133 have fib6 : fib (3 * k + 6) = fib (3 * k + 4) + fib (3 * k + 5) := fib_add_two _
134 have fib7 : fib (3 * k + 7) = fib (3 * k + 5) + fib (3 * k + 6) := fib_add_two _ -- likewise for F_{3k+7}
135 have fib8 : fib (3 * k + 8) = fib (3 * k + 6) + fib (3 * k + 7) := fib_add_two _ -- likewise for F_{3k+8}
136 have fib9 : fib (3 * k + 9) = fib (3 * k + 7) + fib (3 * k + 8) := fib_add_two _ -- likewise for F_{3k+9}
137 have fib10 : fib (3 * k + 10) = fib (3 * k + 8) + fib (3 * k + 9) := fib_add_two _ -- likewise for F_{3k+10}
138 -- the indices at level `k + 2` in the form of those above: 3k + 7 for β and ζ
139 have idx4 : 3 * (k + 1) + 4 = 3 * k + 7 := by omega
140 have idx5 : 3 * (k + 1) + 5 = 3 * k + 8 := by omega -- for α, γ, δ and η
141 have idx6 : 3 * (k + 1) + 6 = 3 * k + 9 := by omega -- for ε
142 have idx7 : 3 * (k + 1) + 7 = 3 * k + 10 := by omega -- for θ
143 rw [idx4, idx5, idx6, idx7]
144 omega
146/-- **Prop 6.2.** For every `m ≥ 1`: α_m = F_{3m+2} + 2, β_m = F_{3m+1} + 2, γ_m = δ_m = η_m = 2F_{3m+2},
147ε_m = F_{3m+3}, ζ_m = 2F_{3m+1}, θ_m = F_{3m+4} − 2. -/
148theorem letterLen_fib (m : Nat) (level_pos : 1 ≤ m) :
157 obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
158 -- the indices at level `k + 1` in the form of `letterLen_fib_aux`: 3k + 4 for β and ζ
159 have idx1 : 3 * (k + 1) + 1 = 3 * k + 4 := by omega
160 have idx2 : 3 * (k + 1) + 2 = 3 * k + 5 := by omega -- for α, γ, δ and η
161 have idx3 : 3 * (k + 1) + 3 = 3 * k + 6 := by omega -- for ε
162 have idx4 : 3 * (k + 1) + 4 = 3 * k + 7 := by omega -- for θ
163 rw [idx1, idx2, idx3, idx4]
164 -- the closed forms, with the indices written out
165 have closed_forms := letterLen_fib_aux k
166 omega
168/-! ### Cor 6.3: parities are constant -/
170/-- **Cor 6.3.** For every `m ≥ 1`, α_m, β_m, θ_m are odd and γ_m, δ_m, ε_m, ζ_m, η_m are even. (Proved from the
171recurrence: the parity vector is a fixed point of (6.1) mod 2.) -/
172theorem letterLen_parity (m : Nat) (level_pos : 1 ≤ m) :
176 obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
177 induction k with
178 | zero => decide
179 | succ k ih =>
180 rw [show k + 1 + 1 = k + 2 from rfl]
181 -- the recurrence (6.1) keeps the parities
182 have recurrence := letterLen_succ k
183 omega
185/-- Cor 6.3 for sides: the parity of ℓ_m(K, j) does not depend on `m ≥ 1`. -/
186theorem sideLen_parity (m m' : Nat) (level_pos : 1 ≤ m) (level_pos' : 1 ≤ m') (K : Kind) (j : Nat) (side_lt : j < 6) :
188 rw [sideLen_eq_letterLen m level_pos K j side_lt, sideLen_eq_letterLen m' level_pos' K j side_lt]
189 -- the parities of the letter lengths at level `m`
190 have parity := letterLen_parity m level_pos
191 -- and the same parities at level `m'`
192 have parity' := letterLen_parity m' level_pos'
195/-! ### Lemma 6.4: the position of A on the Σ side -/
197/-- In a Σ-supertile of level ≥ 2, side 5 begins with the pieces 0.2, 0.1, 7.0, and child 7 is the Γ child, whose
198vertex 0 (the end of piece 7.0) is the crossover corner (Prop 2.4(d)). -/
199theorem sigma_side5_start :
200 (pieces .Sigma 5).take 3 = [(0, 2), (0, 1), (7, 0)] ∧ kidAt .Sigma 0 = .Xi ∧ kidAt .Sigma 7 = .Gamma := by
201 decide
203/-- `dOff m` = d_m, the distance along side 5 of a level-`m` Σ-supertile from its vertex 5 to its crossover corner:
204measured on the level-1 supertile for `m = 1`, and the length of the pieces before the Γ child's vertex 0 above. -/
206 | 0 => 0
208 | m + 2 => (((pieces .Sigma 5).take 3).map (fun p => sideLen (m + 1) (kidAt .Sigma p.1) p.2)).sum
210/-- d_{m+2} is the sum of the lengths of the pieces 0.2, 0.1 and 7.0 at level `m + 1`: θ + ε + α. -/
212 dOff (m + 2) = letterLen (m + 1) .theta + letterLen (m + 1) .epsilon + letterLen (m + 1) .alpha := by
213 -- the length of piece 0.2, side 2 of the Ξ child 0, by its letter
214 have piece_0_2 := sideLen_eq_letterLen (m + 1) (by omega) .Xi 2 (by omega)
215 -- the length of piece 0.1, side 1 of the Ξ child 0, by its letter
216 have piece_0_1 := sideLen_eq_letterLen (m + 1) (by omega) .Xi 1 (by omega)
217 -- the length of piece 7.0, side 0 of the Γ child 7, by its letter
218 have piece_7_0 := sideLen_eq_letterLen (m + 1) (by omega) .Gamma 0 (by omega)
219 simp only [dOff, sigma_side5_start.1, List.map, List.sum_cons, List.sum_nil, sigma_side5_start.2.1,
220 sigma_side5_start.2.2, piece_0_2, piece_0_1, piece_7_0]
223 omega
225/-- **Lemma 6.4.** d_m = 2F_{3m+1}, and the crossover corner is at distance δ_m − d_m = 2F_{3m} from vertex 0. -/
228 obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
229 cases k with
230 | zero => decide
231 | succ k =>
232 rw [show k + 1 + 1 = k + 2 from rfl, dOff_succ, (letterLen_succ k).2.2.2.1]
233 rw [show 3 * (k + 2) + 1 = 3 * k + 7 by omega, show 3 * (k + 2) = 3 * k + 6 by omega]
234 -- the closed forms of Prop 6.2 at level `k + 1`
235 have closed_forms := letterLen_fib_aux k
236 -- the Fibonacci recurrence at F_{3k+6} and F_{3k+7}, for `omega`
237 have fib6 : fib (3 * k + 6) = fib (3 * k + 4) + fib (3 * k + 5) := fib_add_two _
238 have fib7 : fib (3 * k + 7) = fib (3 * k + 5) + fib (3 * k + 6) := fib_add_two _ -- likewise for F_{3k+7}
239 omega
241/-! ### Lemma 6.5: lower bounds -/
243/-- **Lemma 6.5.** For every `m ≥ 1`: every side has length at least 5; d_m ≥ 6; and δ_m − d_m ≥ 4. -/
246 obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := ⟨m - 1, by omega⟩
247 -- every side has length at least 5, at every level
249 intro k
250 induction k with
251 | zero => intro x; cases x <;> decide
252 | succ k ih =>
253 rw [show k + 1 + 1 = k + 2 from rfl]
254 -- the recurrence (6.1): each letter at level `k + 2` is a sum of letters at level `k + 1`
255 have recurrence := letterLen_succ k
256 -- the bound one level down, letter by letter
257 have alpha5 := ih .alpha
258 have beta5 := ih .beta -- likewise for β
259 have gamma5 := ih .gamma -- likewise for γ
260 have delta5 := ih .delta -- likewise for δ
261 have epsilon5 := ih .epsilon -- likewise for ε
262 have zeta5 := ih .zeta -- likewise for ζ
263 have eta5 := ih .eta -- likewise for η
264 have theta5 := ih .theta -- likewise for θ
265 intro x; cases x <;> omega
266 refine ⟨five k, ?_, ?_⟩
267 · cases k with
268 | zero => decide
269 | succ k =>
271 -- d_{k+2} = θ + ε + α, each at least 5
272 have theta5 := five k .theta
273 have epsilon5 := five k .epsilon -- likewise for ε
274 have alpha5 := five k .alpha -- likewise for α
275 omega
276 · cases k with
277 | zero => decide
278 | succ k =>
280 -- δ_{k+2} = α + β + ε + 2θ, so δ − d = β + θ
281 have delta_rec := (letterLen_succ k).2.2.2.1
282 have beta5 := five k .beta -- β is at least 5
283 have theta5 := five k .theta -- θ is at least 5
284 omega
286end SpectreKnot