lean/SpectreKnot/Strands.lean
189 lines · 14 declarations, each with its own page · on GitHub ·
Strands (paper §3.3, Def 3.3 and Lemma 3.4), in the "two involutions" model.
← SpectreKnot/Basic.leanSpectreKnot/Box.lean →
All 39 files, and the declarations of this one
1/-
2Strands (paper §3.3, Def 3.3 and Lemma 3.4), in the "two involutions" model.
4Instead of the strand multigraph of Def 3.3 we work with ports. Every port is an end of exactly one piece, and the
5piece pairs it with the port at its other end (`inside`); every port is joined by the straight-through rule
6(Def 3.2) to exactly one port of the neighbouring tile (`across`). Both are involutions without fixed points. A strand
7is followed by alternating the two; Lemma 3.4 becomes a statement about the permutation `next = across ∘ inside`.
8-/
9import SpectreKnot.Basic
11namespace SpectreKnot
13/-- Ports with the two pairings of Def 3.1 (`inside`: the two ends of a piece) and Def 3.2 (`across`: the
14straight-through rule). In a tiling of the plane both are defined everywhere and have no fixed points. -/
15structure StrandSystem (P : Type) where
16 inside : P → P
17 across : P → P
18 inside_inside : ∀ p, inside (inside p) = p
19 across_across : ∀ p, across (across p) = p
20 inside_ne : ∀ p, inside p ≠ p
21 across_ne : ∀ p, across p ≠ p
23namespace StrandSystem
25variable {P : Type} (S : StrandSystem P)
27/-- One step along a strand: from a port, through its piece to the other end, then across the edge. -/
30/-- One step back. -/
33/-- A step back undoes a step forwards. -/
37/-- A step forwards undoes a step back. -/
41/-- The port reached after `k` steps. -/
44/-- `k + 1` steps are `k` steps and one more. -/
47/-- Two ports that reach the same port after `n` steps are the same port (each step can be undone). -/
48theorem iter_next_injective (n : Nat) {x y : P} (same_end : iter S.next n x = iter S.next n y) : x = y := by
49 induction n with
50 | zero => simpa using same_end
51 | succ n ih =>
52 apply ih
53 -- one step back from the common end: the two walks already met after `n` steps
54 have one_back := congrArg S.prev same_end
57/-- The strand through `p` is *closed* if following it returns to `p`. -/
60/-- A strand never runs through a piece in both directions: no port reached from `p` is the other end of the piece
61of another port reached from `p`. (In the multigraph language: a strand passes through each piece only once.) -/
62theorem walk_ne_inside_walk (p : P) : ∀ i j, S.walk p j ≠ S.inside (S.walk p i) := by
63 -- the claim for i and j = i + d, by two-step induction on d
64 have key : ∀ d i, S.walk p (i + d) ≠ S.inside (S.walk p i) ∧
65 S.walk p (i + (d + 1)) ≠ S.inside (S.walk p i) := by
66 intro d
67 induction d with
68 | zero =>
69 intro i
70 refine ⟨fun same_piece => S.inside_ne _ same_piece.symm, fun next_is_inside => ?_⟩
71 -- walk (i+1) = across (inside (walk i)) = across (walk (i+1)), but `across` has no fixed point
72 have fixed_by_across : S.walk p (i + 1) = S.across (S.walk p (i + 1)) := by
74 exact S.across_ne _ fixed_by_across.symm
75 | succ d ih =>
76 intro i
77 refine ⟨(ih i).2, fun far_is_inside => ?_⟩
78 -- from walk (i + (d+2)) = inside (walk i) we get walk (i+1 + d) = inside (walk (i+1))
79 apply (ih (i + 1)).1
80 -- the step after `walk i`, written as `across` of the far port
81 have after_start : S.walk p (i + 1) = S.across (S.walk p (i + (d + 1 + 1))) := by
83 -- the far port is one step after `walk (i + 1 + d)`
84 have far_step : S.walk p (i + (d + 1 + 1)) = S.next (S.walk p (i + 1 + d)) := by
86 rw [after_start, far_step, next, S.across_across, S.inside_inside]
87 intro i j is_inside
88 by_cases i_le_j : i ≤ j
89 · obtain ⟨d, rfl⟩ : ∃ d, j = i + d := ⟨j - i, by omega⟩
90 exact (key d i).1 is_inside
91 · -- `j` comes first: swap the two ends of the piece
92 obtain ⟨d, rfl⟩ : ∃ d, i = j + d := ⟨i - j, by omega⟩
93 apply (key d j).1
94 rw [is_inside, S.inside_inside]
96/-- If a strand is not closed, the ports reached by following it are pairwise distinct. -/
97theorem walk_injective_of_not_closed (p : P) (not_closed : ¬ S.Closed p) :
98 ∀ i j, S.walk p i = S.walk p j → i = j := by
99 -- if walk i = walk (i + d) with d > 0 then walk d = p
100 have key : ∀ i d, S.walk p i = S.walk p (i + d) → d = 0 := by
101 intro i d same_port
102 apply Classical.byContradiction
103 intro d_ne_zero
104 apply not_closed
105 refine ⟨d, by omega, ?_⟩
106 apply S.iter_next_injective i
109 exact same_port.symm
110 intro i j same_port
111 by_cases i_le_j : i ≤ j
112 · obtain ⟨d, rfl⟩ : ∃ d, j = i + d := ⟨j - i, by omega⟩
113 -- the gap between the two visits is zero
114 have no_gap := key i d same_port
115 omega
116 · obtain ⟨d, rfl⟩ : ∃ d, i = j + d := ⟨i - j, by omega⟩
117 -- the gap between the two visits is zero
118 have no_gap := key j d same_port.symm
119 omega
121/-- Following a strand that is not closed backwards never meets the ports reached forwards, except at `p`. -/
122theorem back_ne_forward_of_not_closed (p : P) (not_closed : ¬ S.Closed p) :
124 -- `a` steps back, then `a` steps forwards, return to the start
126 intro a
127 induction a with
128 | zero => intro x; rfl
129 | succ a ih => intro x; rw [iter_succ', iter_succ, next_prev, ih]
130 intro a b meet
131 -- going `a` steps forwards from the meeting point: `a + b` steps from `p` return to `p`
132 have returns : p = S.walk p (a + b) := by
133 -- the meeting point, moved `a` steps forwards on both sides
135 rw [back_then_forward] at moved
138 -- an open strand never returns to `p`, so `a + b = 0`
139 have no_steps := S.walk_injective_of_not_closed p not_closed 0 (a + b) returns
140 omega
142/-- If a strand is not closed, the ports reached by following it backwards are pairwise distinct. -/
143theorem prev_injective_of_not_closed (p : P) (not_closed : ¬ S.Closed p) :
145 -- `a` steps back, then `a` steps forwards, return to the start
147 intro a
148 induction a with
149 | zero => intro x; rfl
150 | succ a ih => intro x; rw [iter_succ', iter_succ, next_prev, ih]
151 -- going back `d` steps never returns to the start, unless `d = 0`
153 (S.back_ne_forward_of_not_closed p not_closed d 0 back_at_start).1
154 -- if `a` and `a + d` steps back meet, then `d` steps back return to the start
156 intro a d same
158 -- go `a` steps forwards from both
160 rw [back_then_forward, back_then_forward] at undone
161 exact back_ne d undone.symm
162 intro a a' same
163 rcases Nat.le_total a a' with le | le
164 · obtain ⟨d, rfl⟩ : ∃ d, a' = a + d := ⟨a' - a, by omega⟩
165 -- the gap between the two visits is zero
166 have no_gap := key a d same
167 omega
168 · obtain ⟨d, rfl⟩ : ∃ d, a = a' + d := ⟨a - a', by omega⟩
169 -- the gap between the two visits is zero
170 have no_gap := key a' d same.symm
171 omega
173/-- **Lemma 3.4** (in the port model). Every strand is either closed, or a two-way infinite path: following it
174forwards from a port `p`, the ports met are distinct; so are those met backwards; the two walks meet only at `p`; and
175no piece is passed twice (in either direction). -/
176theorem closed_or_path (p : P) :
177 S.Closed p ∨
178 ((∀ i j, S.walk p i = S.walk p j → i = j) ∧
181 (∀ i j, S.walk p j ≠ S.inside (S.walk p i))) := by
182 by_cases closed : S.Closed p
183 · exact Or.inl closed
184 · exact Or.inr ⟨S.walk_injective_of_not_closed p closed, S.prev_injective_of_not_closed p closed,
185 S.back_ne_forward_of_not_closed p closed, S.walk_ne_inside_walk p⟩
187end StrandSystem
189end SpectreKnot