`lean/SpectreKnot/Reverse.lean`

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

Two facts about gluings used to read the parent's signature off Gluing.Sig: a walk between rim ports can be followed backwards (FReach.reverse), and turning about a vertex is injective on vertices reached along the rim (Rot.inj).

← SpectreKnot/ParentRim.leanSpectreKnot/Bridge.lean →

All 39 files, and the declarations of this one

1/-

2Two facts about gluings used to read the parent's signature off `Gluing.Sig`: a walk between rim ports can be

3followed backwards (`FReach.reverse`), and turning about a vertex is injective on vertices reached along the rim

4(`Rot.inj`).

5-/

6import SpectreKnot.Signature

8namespace SpectreKnot.Gluing

10variable {G : Gluing}

12/-- In a well-formed gluing, `τ` (the children's signature pairing) undoes itself on the ports of actual children. -/

13theorem tau_tau (wf : G.WF) {x : GPort} (valid : G.Valid x) : G.tau (G.tau x) = x := by

14 obtain ⟨c, u, s⟩ := x

15 -- the child's two corners differ

16 have A_ne_B := wf.A_ne_B c valid.1

17 by_cases at_A : u = G.A c

18 · -- at corner `A`: to `B` and back

19 -- `τ` sends `A` to `B`

20 have to_B : G.tau (c, u, s) = (c, G.B c, s) := by simp [tau, at_A]

21 -- and `B` back to `A`

22 have to_A : G.tau (c, G.B c, s) = (c, G.A c, s) := by simp [tau, Ne.symm A_ne_B]

23 rw [to_B, to_A, at_A]

24 · by_cases at_B : u = G.B c

25 · -- at corner `B`: to `A` and back

26 -- `τ` sends `B` to `A`

27 have to_A : G.tau (c, u, s) = (c, G.A c, s) := by simp [tau, at_A, at_B]

28 -- and `A` back to `B`

29 have to_B : G.tau (c, G.A c, s) = (c, G.B c, s) := by simp [tau]

30 rw [to_A, to_B, at_B]

31 · -- at a hook: `R` and `L` swap twice

32 -- the first swap

33 have swap : G.tau (c, u, s) = (c, u, !s) := by simp [tau, at_A, at_B]

34 -- the second swap

35 have swap_back : G.tau (c, u, !s) = (c, u, !!s) := by simp [tau, at_A, at_B]

36 rw [swap, swap_back, Bool.not_not]

38/-- In a well-formed gluing, `σ` (straight across a glued edge) is symmetric: if it takes `x` to `y`, it takes `y`

39back to `x`. -/

40theorem sigma_symm (wf : G.WF) {x y : GPort} (valid : G.Valid x) (across : G.sigma x = some y) :

41 G.sigma y = some x := by

42 obtain ⟨c, u, s⟩ := x

43 obtain ⟨c_lt, u_lt⟩ := valid

44 cases s with

45 | true =>

46 -- port `R(u)`, on edge `u`

47 simp only [sigma] at across

48 cases mate_eq : G.mate c u with

49 | none => rw [mate_eq] at across; contradiction

50 | some p =>

51 obtain ⟨c', k'⟩ := p

52 rw [mate_eq] at across

53 simp only [Option.map_some, Option.some.injEq] at across

54 subst across

55 -- the edge is glued back

56 obtain ⟨_, _, mate_back⟩ := wf.mate_valid c u c' k' c_lt u_lt mate_eq

57 simp only [sigma, mate_back, Option.map_some]

58 | false =>

59 -- port `L(u)`, on edge `u - 1`

60 simp only [sigma] at across

61 cases mate_eq : G.mate c (prv (G.E c) u) with

62 | none => rw [mate_eq] at across; contradiction

63 | some p =>

64 obtain ⟨c', k'⟩ := p

65 rw [mate_eq] at across

66 simp only [Option.map_some, Option.some.injEq] at across

67 subst across

68 -- the edge is glued back

69 obtain ⟨_, k'_lt, mate_back⟩ := wf.mate_valid c _ c' k' c_lt (prv_lt u_lt) mate_eq

70 simp only [sigma, prv_nxt k'_lt, mate_back, Option.map_some, nxt_prv u_lt]

72/-- `Walk n a b`: `n` steps (`τ` then `σ`) lead from `a` to `b`. -/

73inductive Walk (G : Gluing) : Nat → GPort → GPort → Prop

74 | zero {a : GPort} : Walk G 0 a a

75 | succ {n : Nat} {a a' b : GPort} : G.sigma (G.tau a) = some a' → Walk G n a' b → Walk G (n + 1) a b

77/-- A walk extended by one more step at its end. -/

78theorem Walk.snoc {n : Nat} {a b b' : GPort} (walk : G.Walk n a b) (last_step : G.sigma (G.tau b) = some b') :

79 G.Walk (n + 1) a b' := by

80 induction walk with

81 | zero => exact .succ last_step .zero

82 | succ first_step _ ih => exact .succ first_step (ih last_step)

84/-- A walk read backwards, through the other ends of the same pieces and edges. -/

85theorem Walk.reverse (wf : G.WF) {n : Nat} {a b : GPort} (walk : G.Walk n a b) (valid : G.Valid a) :

86 G.Walk n (G.tau b) (G.tau a) := by

87 induction walk with

88 | zero => exact .zero

89 | @succ n a a' b first_step _ ih =>

90 -- the other end of the first piece is a port of an actual child

91 have tau_valid_a := tau_valid wf valid

92 -- and so is the port across from it

93 have valid_a' := sigma_valid wf tau_valid_a first_step

94 -- the rest of the walk, backwards

95 have rest_back := ih valid_a'

96 refine rest_back.snoc ?_

97 rw [tau_tau wf valid_a']

98 exact sigma_symm wf tau_valid_a first_step

100/-- A full walk is a `Walk` to a port whose piece ends on the parent's rim. -/

101theorem FReach.walk {k : Nat} {x r : GPort} (reach : G.FReach k x r) :

102 ∃ y, G.Walk k x y ∧ G.sigma (G.tau y) = none ∧ r = G.tau y := by

103 induction reach with

104 | @stop x on_rim => exact ⟨x, .zero, on_rim, rfl⟩

105 | step first_step _ ih =>

106 obtain ⟨y, walk, on_rim, r_eq⟩ := ih

107 exact ⟨y, .succ first_step walk, on_rim, r_eq⟩

108

109/-- A `Walk` to a port whose piece ends on the parent's rim is a full walk. -/

110theorem Walk.freach {k : Nat} {x y : GPort} (walk : G.Walk k x y) (on_rim : G.sigma (G.tau y) = none) :

111 G.FReach k x (G.tau y) := by

112 induction walk with

113 | zero => exact .stop on_rim

114 | succ first_step _ ih => exact .step first_step (ih on_rim)

115

116/-- **Following backwards**: a walk from a rim port `x` to `r` gives a walk from `r` back to `x`. -/

117theorem FReach.reverse (wf : G.WF) {k : Nat} {x r : GPort} (reach : G.FReach k x r) (valid : G.Valid x)

118 (x_on_rim : G.sigma x = none) : G.FReach k r x := by

119 obtain ⟨y, walk, _, rfl⟩ := reach.walk

120 -- the walk backwards, ending where `x` leaves the parent

121 have back := (walk.reverse wf valid).freach (by rw [tau_tau wf valid]; exact x_on_rim)

122 rwa [tau_tau wf valid] at back

123

124/-- `FReach.reverse` for the full walk with any number of crossings. -/

125theorem FullReach.reverse (wf : G.WF) {x r : GPort} (reach : G.FullReach x r) (valid : G.Valid x)

126 (x_on_rim : G.sigma x = none) : G.FullReach r x := by

127 obtain ⟨k, reach_k⟩ := reach

128 exact ⟨k, reach_k.reverse wf valid x_on_rim⟩

129

130/-! ### Turning about a vertex, backwards -/

131

132/-- Turning backwards about a vertex: across the edge before it, while that edge is glued. -/

133inductive RotB (G : Gluing) : Nat × Nat → Nat × Nat → Prop

134 | stop {c u : Nat} : G.mate c (prv (G.E c) u) = none → RotB G (c, u) (c, u)

135 | step {c u c' k' : Nat} {r : Nat × Nat} : G.mate c (prv (G.E c) u) = some (c', k') → RotB G (c', k') r →

136 RotB G (c, u) r

137

138/-- Turning backwards about a vertex has one result. -/

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

140 induction turn generalizing r' with

141 | stop unglued =>

142 cases turn' with

143 | stop _ => rfl

144 | step glued _ => rw [unglued] at glued; contradiction

145 | step glued _ ih =>

146 cases turn' with

147 | stop unglued => rw [glued] at unglued; contradiction

148 | step glued' rest' =>

149 rw [glued] at glued'

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

151 obtain ⟨rfl, rfl⟩ := glued'

152 exact ih rest'

153

154/-- Turning backwards undoes turning forwards: in a well-formed gluing, if turning about vertex `x` (of an actual

155child) reaches `r`, then turning backwards from `r` reaches whatever turning backwards from `x` reaches. -/

156theorem Rot.rotB (wf : G.WF) {x r : Nat × Nat} (turn : G.Rot x r) :

157 x.1 < G.n → x.2 < G.E x.1 → ∀ y, G.RotB x y → G.RotB r y := by

158 induction turn with

159 | stop _ => intro _ _ y turn_back; exact turn_back

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

161 intro c_lt u_lt y turn_back

162 -- the edge is glued back, and `k'` is an actual edge of `c'`

163 obtain ⟨c'_lt, k'_lt, glued_back⟩ := wf.mate_valid c u c' k' c_lt u_lt glued

164 refine ih c'_lt (nxt_lt k'_lt) y (RotB.step (c' := c) (k' := u) ?_ turn_back)

165 rw [prv_nxt k'_lt]; exact glued_back

166

167/-- Two vertices reached along the parent's rim that turn to the same vertex are the same. -/

168theorem Rot.inj (wf : G.WF) {x x' r : Nat × Nat} (rim_x : G.RimL x.1 x.2) (rim_x' : G.RimL x'.1 x'.2)

169 (turn : G.Rot x r) (turn' : G.Rot x' r) : x = x' := by

170 obtain ⟨c, u⟩ := x

171 obtain ⟨c', u'⟩ := x'

172 -- turning backwards from `r` stops at `x`, since the edge before `x` is on the rim

173 have back := turn.rotB wf rim_x.1 rim_x.2.1 (c, u) (.stop rim_x.2.2)

174 -- and likewise at `x'`

175 have back' := turn'.rotB wf rim_x'.1 rim_x'.2.1 (c', u') (.stop rim_x'.2.2)

176 exact back.unique back'

177

178end SpectreKnot.Gluing

← SpectreKnot/ParentRim.leanSpectreKnot/Bridge.lean →