`lean/SpectreKnot/Signature.lean`

298 lines · 13 declarations, each with its own page · on GitHub · hide comments

The signature of a composition (the conclusion of the induction step), stated without lists: a parent rim vertex is found by turning about a vertex of a child (Rot). The signature survives cutting an edge (Cut.OK.sig) and passing to an equivalent gluing (Sig.congr); that is what the parity lemma needs.

← SpectreKnot/Move.leanSpectreKnot/CompSig.lean →

All 39 files, and the declarations of this one

1/-

2The signature of a composition (the conclusion of the induction step), stated without lists: a parent rim vertex is

3found by turning about a vertex of a child (`Rot`). The signature survives cutting an edge (`Cut.OK.sig`) and passing

4to an equivalent gluing (`Sig.congr`); that is what the parity lemma needs.

5-/

6import SpectreKnot.NewWalk

8namespace SpectreKnot.Gluing

10variable {G G' : Gluing}

12/-! ### Turning about a vertex -/

14/-- Turning about a vertex inside the parent. Vertex `u` of child `c` is where its edge `u` starts. If that edge is

15glued to edge `k'` of child `c'`, the same point is where edge `k'` ends, so the next edge about it is edge `k' + 1` of

16`c'`. `Rot G (c, u) r`: turning from vertex `u` of `c` reaches the vertex `r`, whose edge is on the parent's rim. -/

17inductive Rot (G : Gluing) : Nat × Nat → Nat × Nat → Prop

18 | stop {c u : Nat} : G.mate c u = none → Rot G (c, u) (c, u)

19 | step {c u c' k' : Nat} {r : Nat × Nat} :

20 G.mate c u = some (c', k') → Rot G (c', nxt (G.E c') k') r → Rot G (c, u) r

22/-- Turning about a vertex has one result. -/

23theorem Rot.unique {x r r' : Nat × Nat} (turn : G.Rot x r) (turn' : G.Rot x r') : r = r' := by

24 induction turn generalizing r' with

25 | stop on_rim =>

26 cases turn' with

27 | stop _ => rfl

28 | step glued _ => rw [on_rim] at glued; contradiction

29 | step glued _ ih =>

30 cases turn' with

31 | stop on_rim => rw [glued] at on_rim; contradiction

32 | step glued' rest' =>

33 rw [glued] at glued'

34 simp only [Option.some.injEq, Prod.mk.injEq] at glued'

35 obtain ⟨rfl, rfl⟩ := glued'

36 exact ih rest'

38/-- Vertex `u` of child `c` is a parent rim vertex, reached along the parent's rim: the edge before it, `u - 1`, is on

39the parent's rim. (Its port `L` is then a port of the parent.) -/

40def RimL (G : Gluing) (c u : Nat) : Prop := c < G.n ∧ u < G.E c ∧ G.mate c (prv (G.E c) u) = none

42/-! ### The signature -/

44/-- **The signature** of the parent, for a gluing whose crossover child is `g` (Def 4.3 at the parent's level):

45* the gluing is well formed, and the walk from every port ends on the parent's rim (no closed strand);

46* at every parent rim vertex, reached along the rim at vertex `u` of child `c` and left along the rim at vertex `u₂`

47 of child `c₂` (`Rot`), the strand from the port `L` there leaves at the port `R` there (a hook), except at the

48 crossover child's corners `A` and `B`;

49* those corners are parent rim vertices (their edges lie on the parent's rim), and carry the crossover:

50 `R(A) ↔ R(B)` and `L(A) ↔ L(B)`. -/

51structure Sig (G : Gluing) (g : Nat) : Prop where

52 wf : G.WF

53 noLoops : ∀ x, G.Valid x → ∃ r, G.FullReach x r

54 hooks : ∀ c u, G.RimL c u → ∃ c₂ u₂, G.Rot (c, u) (c₂, u₂) ∧

55 ((c₂ = g ∧ (u₂ = G.A g ∨ u₂ = G.B g)) ∨ G.FullReach (c, u, false) (c₂, u₂, true))

56 g_lt : g < G.n

57 rimA : G.mate g (G.A g) = none

58 rimB : G.mate g (G.B g) = none

59 crossR : G.FullReach (g, G.A g, true) (g, G.B g, true)

60 crossL : ∃ cA uA cB uB, G.RimL cA uA ∧ G.Rot (cA, uA) (g, G.A g) ∧ G.RimL cB uB ∧ G.Rot (cB, uB) (g, G.B g) ∧

61 G.FullReach (cA, uA, false) (cB, uB, false)

63/-! ### Equivalent gluings -/

65namespace Equiv

67variable (equiv : Equiv G G')

69include equiv

71/-- Turning about a vertex of a child gives the same result in an equivalent gluing. -/

72theorem rot (G_wf : G.WF) {x r : Nat × Nat} (turn : G.Rot x r) : x.1 < G.n → x.2 < G.E x.1 → G'.Rot x r := by

73 induction turn with

74 | @stop c u on_rim => intro c_lt u_lt; exact .stop (by rw [← equiv.mate c u c_lt u_lt]; exact on_rim)

75 | @step c u c' k' r glued _ ih =>

76 intro c_lt u_lt

77 obtain ⟨c'_lt, k'_lt, _⟩ := G_wf.mate_valid _ _ _ _ c_lt u_lt glued

78 exact .step (by rw [← equiv.mate c u c_lt u_lt]; exact glued)

79 (by rw [← equiv.E c' c'_lt]; exact ih c'_lt (nxt_lt k'_lt))

81/-- A parent rim vertex of `G` is one of an equivalent gluing `G'`. -/

82theorem rimL {c u : Nat} (rim_vertex : G.RimL c u) : G'.RimL c u := by

83 obtain ⟨c_lt, u_lt, prev_on_rim⟩ := rim_vertex

84 refine ⟨equiv.n ▸ c_lt, (equiv.E c c_lt) ▸ u_lt, ?_⟩

85 rw [← equiv.E c c_lt, ← equiv.mate c _ c_lt (prv_lt u_lt)]; exact prev_on_rim

87/-- A gluing equivalent to one with the signature has the signature, with the same crossover child. -/

88theorem sig {g : Nat} (has_sig : Sig G g) : Sig G' g where

89 wf := equiv.wf has_sig.wf

90 noLoops x x_valid := by

91 obtain ⟨r, reach⟩ := has_sig.noLoops x (equiv.valid' x_valid)

92 exact ⟨r, equiv.fullReach has_sig.wf (equiv.valid' x_valid) reach⟩

93 hooks c u rim_vertex := by

94 -- the vertex is a parent rim vertex of `G`

95 have rim_vertex_G : G.RimL c u := equiv.symm.rimL rim_vertex

96 obtain ⟨c₂, u₂, turn, hook⟩ := has_sig.hooks c u rim_vertex_G

97 refine ⟨c₂, u₂, equiv.rot has_sig.wf turn rim_vertex_G.1 rim_vertex_G.2.1, ?_⟩

98 rw [← equiv.A g has_sig.g_lt, ← equiv.B g has_sig.g_lt]

99 rcases hook with at_corner | joins

100 · exact Or.inl at_corner

101 · exact Or.inr (equiv.fullReach has_sig.wf ⟨rim_vertex_G.1, rim_vertex_G.2.1⟩ joins)

102 g_lt := equiv.n ▸ has_sig.g_lt

103 rimA := by

104 rw [← equiv.A g has_sig.g_lt, ← equiv.mate g _ has_sig.g_lt (has_sig.wf.A_lt g has_sig.g_lt)]

105 exact has_sig.rimA

106 rimB := by

107 rw [← equiv.B g has_sig.g_lt, ← equiv.mate g _ has_sig.g_lt (has_sig.wf.B_lt g has_sig.g_lt)]

108 exact has_sig.rimB

109 crossR := by

110 rw [← equiv.A g has_sig.g_lt, ← equiv.B g has_sig.g_lt]

111 exact equiv.fullReach has_sig.wf ⟨has_sig.g_lt, has_sig.wf.A_lt g has_sig.g_lt⟩ has_sig.crossR

112 crossL := by

113 obtain ⟨cA, uA, cB, uB, rim_A, turn_A, rim_B, turn_B, joins⟩ := has_sig.crossL

114 rw [← equiv.A g has_sig.g_lt, ← equiv.B g has_sig.g_lt]

115 exact ⟨cA, uA, cB, uB, equiv.rimL rim_A, equiv.rot has_sig.wf turn_A rim_A.1 rim_A.2.1, equiv.rimL rim_B,

116 equiv.rot has_sig.wf turn_B rim_B.1 rim_B.2.1, equiv.fullReach has_sig.wf ⟨rim_A.1, rim_A.2.1⟩ joins⟩

117

118end Equiv

119

120/-! ### Cutting an edge -/

121

122namespace Cut.OK

123

124set_option linter.unusedSectionVars false

125

126variable {κ : Cut} (cut_ok : κ.OK G)

127

128include cut_ok

129

130/-- A rim edge stays a rim edge. -/

131theorem mate_none {c k : Nat} (on_rim : G.mate c k = none) : (subdiv G κ).mate c (κ.sh c k) = none := by

132 by_cases is_cut₀ : c = κ.c₀ ∧ k = κ.e₀

133 · obtain ⟨rfl, rfl⟩ := is_cut₀

134 rw [cut_ok.sh_c₀_le (Nat.le_refl _), cut_ok.mate_cut₀, cut_ok.two_false on_rim]; rfl

135 · by_cases is_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ k = κ.e₁

136 · obtain ⟨cut_glued, rfl, rfl⟩ := is_cut₁

137 rw [(cut_ok.two_mate cut_glued).2.2] at on_rim; contradiction

138 · rw [cut_ok.mate_old is_cut₀ is_cut₁, on_rim]; rfl

139

140/-- The vertex after a rim edge stays the vertex after a rim edge. -/

141theorem rimL_port {c u : Nat} (rim_vertex : G.RimL c u) : (subdiv G κ).RimL c (κ.sh c u) := by

142 obtain ⟨c_lt, u_lt, prev_on_rim⟩ := rim_vertex

143 refine ⟨c_lt, cut_ok.sh_lt u_lt, ?_⟩

144 -- the cut edge is not the last edge of `c₀`

145 have e₀_lt := cut_ok.e₀

146 by_cases after_cut₀ : c = κ.c₀ ∧ u = κ.e₀ + 1

147 · obtain ⟨rfl, rfl⟩ := after_cut₀

148 rw [prv_succ'] at prev_on_rim

149 -- the cut edge is on the rim, so only it is cut

150 have cut_on_rim := cut_ok.two_false prev_on_rim

151 rw [cut_ok.sh_c₀_gt (by omega), cut_ok.E_c₀, show κ.e₀ + 1 + 2 = (κ.e₀ + 2) + 1 by omega, prv_succ',

152 cut_ok.mate_new₀ (by omega), cut_on_rim]; rfl

153 · by_cases after_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ u = κ.e₁ + 1

154 · obtain ⟨cut_glued, rfl, rfl⟩ := after_cut₁

155 rw [prv_succ', (cut_ok.two_mate cut_glued).2.2] at prev_on_rim; contradiction

156 · rw [cut_ok.prv_sh u_lt after_cut₀ after_cut₁]

157 exact cut_ok.mate_none prev_on_rim

158

159/-- Every vertex after a rim edge of the subdivided gluing is an old one, or one of the two new vertices of a cut rim

160edge. -/

161theorem rimL_pre {c u' : Nat} (rim_vertex : (subdiv G κ).RimL c u') :

162 (∃ u, G.RimL c u ∧ κ.sh c u = u') ∨ (κ.two = false ∧ c = κ.c₀ ∧ (u' = κ.e₀ + 1 ∨ u' = κ.e₀ + 2)) := by

163 obtain ⟨c_lt, u'_lt, prev_on_rim⟩ := rim_vertex

164 -- the cut edge is not the last edge of `c₀`

165 have e₀_lt := cut_ok.e₀

166 by_cases new₀ : c = κ.c₀ ∧ κ.e₀ < u' ∧ u' ≤ κ.e₀ + 2

167 · obtain ⟨rfl, u'_gt, u'_le⟩ := new₀

168 right

169 -- the edge before a new vertex is a new edge

170 have prev_edge : prv ((subdiv G κ).E κ.c₀) u' = κ.e₀ + (u' - 1 - κ.e₀) := by unfold prv; split <;> omega

171 rw [prev_edge, cut_ok.mate_new₀ (by omega)] at prev_on_rim

172 cases cut_glued : κ.two

173 · exact ⟨rfl, rfl, by omega⟩

174 · rw [cut_glued] at prev_on_rim; simp at prev_on_rim

175 · by_cases new₁ : κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ < u' ∧ u' ≤ κ.e₁ + 2

176 · exfalso

177 obtain ⟨cut_glued, rfl, u'_gt, u'_le⟩ := new₁

178 -- the edge before a new vertex is a new edge, which is glued

179 have prev_edge : prv ((subdiv G κ).E κ.c₁) u' = κ.e₁ + (u' - 1 - κ.e₁) := by unfold prv; split <;> omega

180 rw [prev_edge, cut_ok.mate_new₁ cut_glued (by omega)] at prev_on_rim; contradiction

181 · left

182 obtain ⟨u, u_lt, rfl⟩ := cut_ok.preimage u'_lt new₀ new₁

183 refine ⟨u, ⟨c_lt, u_lt, ?_⟩, rfl⟩

184 by_cases after_cut₀ : c = κ.c₀ ∧ u = κ.e₀ + 1

185 · obtain ⟨rfl, rfl⟩ := after_cut₀

186 rw [cut_ok.sh_c₀_gt (by omega), cut_ok.E_c₀, show κ.e₀ + 1 + 2 = (κ.e₀ + 2) + 1 by omega, prv_succ',

187 cut_ok.mate_new₀ (by omega)] at prev_on_rim

188 rw [prv_succ']

189 cases cut_glued : κ.two

190 · have cut_mate := cut_ok.mate -- the cut edge lies on the rim

191 rw [cut_glued] at cut_mate; rw [cut_mate]; rfl

192 · rw [cut_glued] at prev_on_rim; simp at prev_on_rim

193 · by_cases after_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ u = κ.e₁ + 1

194 · exfalso

195 obtain ⟨cut_glued, rfl, rfl⟩ := after_cut₁

196 -- the partner edge is not the last edge of `c₁`

197 have e₁_lt := cut_ok.e₁ cut_glued

198 rw [cut_ok.sh_c₁_gt cut_glued (by omega), cut_ok.E_c₁ cut_glued,

199 show κ.e₁ + 1 + 2 = (κ.e₁ + 2) + 1 by omega, prv_succ',

200 cut_ok.mate_new₁ cut_glued (by omega)] at prev_on_rim

201 contradiction

202 · rw [cut_ok.prv_sh u_lt after_cut₀ after_cut₁] at prev_on_rim

203 -- the edge before `u` is not the cut edge

204 have not_cut₀ : ¬ (c = κ.c₀ ∧ prv (G.E c) u = κ.e₀) :=

205 fun prev_cut => after_cut₀ ⟨prev_cut.1, cut_ok.prv_cut u_lt prev_cut⟩

206 -- nor the partner edge

207 have not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ prv (G.E c) u = κ.e₁) := fun ⟨cut_glued, is_c₁, prev_eq⟩ =>

208 after_cut₁ ⟨cut_glued, is_c₁, cut_ok.prv_cut₁ cut_glued u_lt ⟨is_c₁, prev_eq⟩⟩

209 rw [cut_ok.mate_old not_cut₀ not_cut₁, Option.map_eq_none_iff] at prev_on_rim

210 exact prev_on_rim

211

212/-- Turning about an old vertex gives the same result, renumbered. -/

213theorem rot_port {x r : Nat × Nat} (turn : G.Rot x r) :

214 x.1 < G.n → x.2 < G.E x.1 → (subdiv G κ).Rot (x.1, κ.sh x.1 x.2) (r.1, κ.sh r.1 r.2) := by

215 induction turn with

216 | @stop c u on_rim => intro _ _; exact .stop (cut_ok.mate_none on_rim)

217 | @step c u c' k' r glued _ ih =>

218 intro c_lt u_lt

219 obtain ⟨c'_lt, k'_lt, _⟩ := cut_ok.wf.mate_valid _ _ _ _ c_lt u_lt glued

220 -- the rest of the turn, renumbered

221 have rest := ih c'_lt (nxt_lt k'_lt)

222 dsimp only at rest ⊢

223 by_cases is_cut₀ : c = κ.c₀ ∧ u = κ.e₀

224 · obtain ⟨rfl, rfl⟩ := is_cut₀

225 obtain ⟨cut_glued, partner⟩ := cut_ok.two_true glued

226 simp only [Prod.mk.injEq] at partner

227 obtain ⟨rfl, rfl⟩ := partner

228 -- the partner edge is not the last edge of `c₁`

229 have e₁_lt := cut_ok.e₁ cut_glued

230 refine .step (c' := κ.c₁) (k' := κ.e₁ + 2) ?_ ?_

231 · rw [cut_ok.sh_c₀_le (Nat.le_refl _), cut_ok.mate_cut₀, ite_eq_left cut_glued]

232 · rw [cut_ok.E_c₁ cut_glued, nxt_of_lt' (by omega)]

233 rw [nxt_of_lt' e₁_lt, cut_ok.sh_c₁_gt cut_glued (by omega)] at rest

234 exact rest

235 · by_cases is_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ u = κ.e₁

236 · obtain ⟨cut_glued, rfl, rfl⟩ := is_cut₁

237 rw [(cut_ok.two_mate cut_glued).2.2] at glued

238 simp only [Option.some.injEq, Prod.mk.injEq] at glued

239 obtain ⟨rfl, rfl⟩ := glued

240 -- the cut edge is not the last edge of `c₀`

241 have e₀_lt := cut_ok.e₀

242 refine .step (c' := κ.c₀) (k' := κ.e₀ + 2) ?_ ?_

243 · rw [cut_ok.sh_c₁_le cut_glued (Nat.le_refl _), cut_ok.mate_cut₁ cut_glued]

244 · rw [cut_ok.E_c₀, nxt_of_lt' (by omega)]

245 rw [nxt_of_lt' e₀_lt, cut_ok.sh_c₀_gt (by omega)] at rest

246 exact rest

247 · refine .step (c' := c') (k' := κ.sh c' k') ?_ ?_

248 · rw [cut_ok.mate_old is_cut₀ is_cut₁, glued]; rfl

249 · obtain ⟨mate_not_cut₀, mate_not_cut₁⟩ := cut_ok.target_not_cut c_lt u_lt glued is_cut₀ is_cut₁

250 rw [cut_ok.nxt_sh k'_lt mate_not_cut₀ mate_not_cut₁]; exact rest

251

252/-- The two new vertices of a cut rim edge are parent rim vertices with a hook. -/

253theorem new_hook (cut_on_rim : κ.two = false) {i : Nat} (i_ge : 1 ≤ i) (i_le : i ≤ 2) :

254 (subdiv G κ).Rot (κ.c₀, κ.e₀ + i) (κ.c₀, κ.e₀ + i) ∧

255 (subdiv G κ).FullReach (κ.c₀, κ.e₀ + i, false) (κ.c₀, κ.e₀ + i, true) := by

256 -- the new edge starting at the vertex lies on the rim

257 have on_rim : (subdiv G κ).mate κ.c₀ (κ.e₀ + i) = none := by rw [cut_ok.mate_new₀ (by omega), cut_on_rim]; rfl

258 refine ⟨.stop on_rim, 0, ?_⟩

259 -- the piece at the vertex joins its two ports, and the walk stops at port `R` there

260 have stops := FReach.stop (G := subdiv G κ) (x := (κ.c₀, κ.e₀ + i, false))

261 (by rw [cut_ok.tau_new₀ i_ge i_le, Bool.not_false, sigmaR, on_rim]; rfl)

262 rw [cut_ok.tau_new₀ i_ge i_le, Bool.not_false] at stops

263 exact stops

264

In the paper Lemma 7.1 Lengthening

265/-- **The signature survives cutting an edge.** -/

266theorem sig {g : Nat} (has_sig : Sig G g) : Sig (subdiv G κ) g where

267 wf := cut_ok.wf_subdiv

268 noLoops := cut_ok.noLoops has_sig.noLoops

269 hooks c u' rim_vertex := by

270 rcases cut_ok.rimL_pre rim_vertex with ⟨u, old_rim_vertex, rfl⟩ | ⟨cut_on_rim, rfl, new_vertex⟩

271 · obtain ⟨c₂, u₂, turn, hook⟩ := has_sig.hooks c u old_rim_vertex

272 refine ⟨c₂, κ.sh c₂ u₂, cut_ok.rot_port turn old_rim_vertex.1 old_rim_vertex.2.1, ?_⟩

273 rcases hook with ⟨rfl, at_A | at_B⟩ | joins

274 · exact Or.inl ⟨rfl, Or.inl (by rw [at_A]; rfl)⟩

275 · exact Or.inl ⟨rfl, Or.inr (by rw [at_B]; rfl)⟩

276 · obtain ⟨k, walk⟩ := joins

277 exact Or.inr (Sim.reach cut_ok.wf cut_ok.sim k _ _ ⟨old_rim_vertex.1, old_rim_vertex.2.1⟩ walk)

278 · obtain ⟨i, i_ge, i_le, rfl⟩ : ∃ i, 1 ≤ i ∧ i ≤ 2 ∧ u' = κ.e₀ + i := by

279 rcases new_vertex with rfl | rfl

280 · exact ⟨1, by omega, by omega, rfl⟩

281 · exact ⟨2, by omega, by omega, rfl⟩

282 obtain ⟨turn, joins⟩ := cut_ok.new_hook cut_on_rim i_ge i_le

283 exact ⟨κ.c₀, κ.e₀ + i, turn, Or.inr joins⟩

284 g_lt := has_sig.g_lt

285 rimA := cut_ok.mate_none has_sig.rimA

286 rimB := cut_ok.mate_none has_sig.rimB

287 crossR := by

288 obtain ⟨k, walk⟩ := has_sig.crossR

289 exact Sim.reach cut_ok.wf cut_ok.sim k _ _ ⟨has_sig.g_lt, has_sig.wf.A_lt g has_sig.g_lt⟩ walk

290 crossL := by

291 obtain ⟨cA, uA, cB, uB, rim_A, turn_A, rim_B, turn_B, ⟨k, walk⟩⟩ := has_sig.crossL

292 exact ⟨cA, κ.sh cA uA, cB, κ.sh cB uB, cut_ok.rimL_port rim_A, cut_ok.rot_port turn_A rim_A.1 rim_A.2.1,

293 cut_ok.rimL_port rim_B, cut_ok.rot_port turn_B rim_B.1 rim_B.2.1,

294 Sim.reach cut_ok.wf cut_ok.sim k _ _ ⟨rim_A.1, rim_A.2.1⟩ walk⟩

295

296end Cut.OK

297

298end SpectreKnot.Gluing

← SpectreKnot/Move.leanSpectreKnot/CompSig.lean →