A Reidemeister kink on a crossing-free circle

PDCode.adjoinKink D b adjoins an isolated one-crossing component to D. Its two arcs join slots 0–1 and 2–3, as in PDCode.kink, and b chooses the over-strand. It is the result of applying the first Reidemeister move to the new circle in PDCode.adjoinCircle D. This complements arc-based kink insertion, whose half-edge argument cannot select a crossing-free component.

The state-circle formula includes the empty surrounding diagram. Consequently the bracket formula compares the kink with D.adjoinCircle, with no nonemptiness assumption on D. The kink contributes one graph component and three faces, so adjoining it preserves planarity. The Kauffman bracket of D.adjoinKink b is the bracket of D.adjoinCircle multiplied by -a³ when b = true and by -a⁻³ when b = false.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapters 1 and 3 (Reidemeister moves and the Kauffman bracket).
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395–407.
• Formalization sources: PDCode.kauffmanBracket_reidemeisterOne and PDCode.stateLoopCount_adjoinCircle.

def TauCeti.PDCode.adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) : PDCode (n + 1)

Adjoin an isolated kink with over-pair indicator b. Compared with D.adjoinCircle, the new circle has acquired one crossing by a first Reidemeister move.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.PDCode.adjoinKink_halfEdge {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).halfEdge = (halfEdgeSuccEquiv n).permCongr (D.halfEdge.sumCongr 1)

The old crossings and the new crossing occupy separate blocks of half-edges.

theorem TauCeti.PDCode.adjoinKink_edgePair_val {n : ℕ} (D : PDCode n) (b : Bool) : ↑(D.adjoinKink b).edgePair = (halfEdgeSuccEquiv n).permCongr ((↑D.edgePair).sumCongr (slotSmoothing true))

The old arcs and the two arcs of the kink form separate matchings.

@[simp]

theorem TauCeti.PDCode.adjoinKink_crossinglessComponentCount {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).crossinglessComponentCount = D.crossinglessComponentCount

Adjoining a kink retains the crossing-free components of the surrounding diagram.

@[simp]

theorem TauCeti.PDCode.adjoinKink_overPair {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).overPair = Fin.snoc D.overPair b

The new crossing has over-pair indicator b; the old indicators are unchanged.

@[simp]

theorem TauCeti.PDCode.adjoinKink_crossing_castSucc {n : ℕ} (D : PDCode n) (b : Bool) (i : Fin n) (s : Fin 4) : (D.adjoinKink b).crossing i.castSucc s = (halfEdgeSuccEquiv n) (Sum.inl (D.crossing i s))

The old crossings keep their slots.

@[simp]

theorem TauCeti.PDCode.adjoinKink_crossing_last {n : ℕ} (D : PDCode n) (b : Bool) (s : Fin 4) : (D.adjoinKink b).crossing (Fin.last n) s = (halfEdgeSuccEquiv n) (Sum.inr s)

The slots of the new crossing are the new half-edges.

@[simp]

theorem TauCeti.PDCode.adjoinKink_edgePair_inl {n : ℕ} (D : PDCode n) (b : Bool) (x : Fin (4 * n)) : ↑(D.adjoinKink b).edgePair ((halfEdgeSuccEquiv n) (Sum.inl x)) = (halfEdgeSuccEquiv n) (Sum.inl (↑D.edgePair x))

The old arcs are unchanged by adjoining a kink.

@[simp]

theorem TauCeti.PDCode.adjoinKink_edgePair_inr {n : ℕ} (D : PDCode n) (b : Bool) (s : Fin 4) : ↑(D.adjoinKink b).edgePair ((halfEdgeSuccEquiv n) (Sum.inr s)) = (halfEdgeSuccEquiv n) (Sum.inr ((slotSmoothing true) s))

The new arcs pair slots 0–1 and 2–3, independently of the old diagram.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).crossingComponentCount = D.crossingComponentCount + 1

Adjoining an isolated kink adds one crossing-bearing component.

@[simp]

theorem TauCeti.PDCode.componentCount_adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).componentCount = D.adjoinCircle.componentCount

A kink and a crossing-free circle contribute the same number of components.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) (s : Fin (n + 1) → Bool) : (D.adjoinKink b).stateLoopCount s = D.stateLoopCount (Fin.init s) + 1 + if s (Fin.last n) = b then 1 else 0

A state of the isolated kink contributes two circles when it separates its arcs, and one circle otherwise.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_adjoinKink {n : ℕ} {R : Type u_1} [CommRing R] (D : PDCode n) (b : Bool) (a : Rˣ) : (D.adjoinKink b).kauffmanBracket a = -↑(bif b then a else a⁻¹) ^ 3 * D.adjoinCircle.kauffmanBracket a

The first Reidemeister factor for a kink on a crossing-free circle. The surrounding diagram may be empty.

@[simp]

theorem TauCeti.PDCode.mirror_adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).mirror = D.mirror.adjoinKink !b

Reflection switches the over-strand of the new kink.

@[simp]

theorem TauCeti.PDCode.card_monodromyOrbit_adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) : Nat.card (D.adjoinKink b).toPermutationTriple.MonodromyOrbit = Nat.card D.toPermutationTriple.MonodromyOrbit + 1

The new kink is one connected component of the underlying graph, separate from all components of the surrounding diagram.

@[simp]

theorem TauCeti.PDCode.faceCount_adjoinKink {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).faceCount = D.faceCount + 3

The isolated kink adds its three faces to the surrounding diagram.

@[simp]

theorem TauCeti.PDCode.isPlanar_adjoinKink_iff {n : ℕ} (D : PDCode n) (b : Bool) : (D.adjoinKink b).IsPlanar ↔ D.IsPlanar

The first Reidemeister move on a crossing-free circle preserves planarity.