The third Reidemeister move on PD-codes

The braid form of the third Reidemeister move replaces the three-crossing tangle σ₁ σ₂ σ₁ by σ₂ σ₁ σ₂, inside an arbitrary surrounding PD-code. The crossing slots are read counterclockwise as northwest, southwest, southeast, northeast. Its six boundary attachments are transported to the corresponding ports of the replacement tangle; every half-edge outside the three selected crossings stays fixed. The three over-pair indicators give an acyclic height order on the three strands for a valid Reidemeister move. All six orders are allowed. The raw rewire and its component identities are defined without this condition. The over-pair indicators at the first and third crossing exchange places, so each pair of physical strands keeps its over-strand.

The construction uses a permutation of the twelve local half-edges. This permutation mixes crossings, so the operation is not a relabelling of a PD-code. It commutes with opposite-slot traversal, however, which proves preservation of the link components. The triangular arcs and the boundary attachments are specified explicitly below.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1 (Reidemeister moves) and Chapter 3 (the Kauffman bracket).

def TauCeti.PDCode.reidemeisterThreeSlots : Equiv.Perm (Fin 3 × Fin 4)

The twelve local half-edge positions are transported from σ₁ σ₂ σ₁ to σ₂ σ₁ σ₂. The first coordinate is the crossing and the second its cyclic slot.

Equations

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

theorem TauCeti.PDCode.reidemeisterThreeSlots_apply (i : Fin 3) (s : Fin 4) : reidemeisterThreeSlots (i, s) = ![![(1, 0), (0, 2), (1, 2), (0, 0)], ![(2, 0), (0, 1), (2, 2), (0, 3)], ![(2, 3), (1, 1), (2, 1), (1, 3)]] i s

The twelve-slot table defining the local rewire.

theorem TauCeti.PDCode.reidemeisterThreeSlots_symm_apply (i : Fin 3) (s : Fin 4) : (Equiv.symm reidemeisterThreeSlots) (i, s) = ![![(0, 3), (1, 1), (0, 1), (1, 3)], ![(0, 0), (2, 1), (0, 2), (2, 3)], ![(1, 0), (2, 2), (1, 2), (2, 0)]] i s

The inverse twelve-slot table reconstructs the original tangle positions.

def TauCeti.PDCode.ReidemeisterThree.triangleEmbedding {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : Fin 3 × Fin 4 ↪ Fin (4 * n)

Include the twelve selected crossing slots in the ambient half-edge type.

Equations

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

theorem TauCeti.PDCode.ReidemeisterThree.triangleEmbedding_apply {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (i : Fin 3) (s : Fin 4) : (triangleEmbedding D c) (i, s) = D.crossing (c i) s

The selected-slot inclusion agrees with the named crossing half-edges.

def TauCeti.PDCode.reidemeisterThreePerm {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : Equiv.Perm (Fin (4 * n))

The local half-edge permutation transporting the boundary ports and triangular arcs from σ₁ σ₂ σ₁ to σ₂ σ₁ σ₂, fixing half-edges at every other crossing.

Equations

• D.reidemeisterThreePerm c = TauCeti.PDCode.reidemeisterThreeSlots.viaFintypeEmbedding (TauCeti.PDCode.ReidemeisterThree.triangleEmbedding D c)

theorem TauCeti.PDCode.reidemeisterThreePerm_apply_crossing {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (i : Fin 3) (s : Fin 4) : (D.reidemeisterThreePerm c) (D.crossing (c i) s) = D.crossing (c (reidemeisterThreeSlots (i, s)).1) (reidemeisterThreeSlots (i, s)).2

On a selected crossing, the half-edge permutation follows the twelve-slot table.

theorem TauCeti.PDCode.reidemeisterThreePerm_crossing_of_notMem {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) {i : Fin n} (hi : i ∉ Set.range ⇑c) (s : Fin 4) : (D.reidemeisterThreePerm c) (D.crossing i s) = D.crossing i s

Half-edges at unselected crossings are fixed by the local permutation.

theorem TauCeti.PDCode.reidemeisterThreePerm_crossingTurn {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (Equiv.permCongr (D.reidemeisterThreePerm c)) D.crossingTurn = D.crossingTurn

The local rewire commutes with the crossing turn: it carries each pair of opposite slots of a crossing to a pair of opposite slots of a crossing.

def TauCeti.PDCode.HasReidemeisterThreeTriangleArcs {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : Prop

The three internal arcs of the triangular tangle σ₁ σ₂ σ₁. Crossing slots are northwest, southwest, southeast, northeast. This condition is independent of strand heights; no condition is imposed on the surrounding arcs.

Equations

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

theorem TauCeti.PDCode.hasReidemeisterThreeTriangleArcs_iff {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : D.HasReidemeisterThreeTriangleArcs c ↔ ↑D.edgePair (D.crossing (c 0) 2) = D.crossing (c 1) 0 ∧ ↑D.edgePair (D.crossing (c 1) 1) = D.crossing (c 2) 3 ∧ ↑D.edgePair (D.crossing (c 0) 1) = D.crossing (c 2) 0

The triangle arc condition specifies exactly its three internal arcs.

def TauCeti.PDCode.HasReidemeisterThreeTriangle {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : Prop

The three crossings form the triangular tangle of σ₁ σ₂ σ₁, with a consistent height order on its three strands. No condition is imposed on the surrounding arcs.

Equations

• D.HasReidemeisterThreeTriangle c = (D.HasReidemeisterThreeTriangleArcs c ∧ (D.overPair (c 0) = D.overPair (c 2) → D.overPair (c 1) = D.overPair (c 0)))

theorem TauCeti.PDCode.HasReidemeisterThreeTriangle.arcs {n : ℕ} {D : PDCode n} {c : Fin 3 ↪ Fin n} (h : D.HasReidemeisterThreeTriangle c) : D.HasReidemeisterThreeTriangleArcs c

A Reidemeister triangle has the prescribed internal arcs, independently of its heights.

theorem TauCeti.PDCode.hasReidemeisterThreeTriangle_iff {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : D.HasReidemeisterThreeTriangle c ↔ ↑D.edgePair (D.crossing (c 0) 2) = D.crossing (c 1) 0 ∧ ↑D.edgePair (D.crossing (c 1) 1) = D.crossing (c 2) 3 ∧ ↑D.edgePair (D.crossing (c 0) 1) = D.crossing (c 2) 0 ∧ (D.overPair (c 0) = D.overPair (c 2) → D.overPair (c 1) = D.overPair (c 0))

A triangle consists of the three internal arcs and an acyclic strand height order.

def TauCeti.PDCode.reidemeisterThree {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : PDCode n

The third Reidemeister rewire in braid form at three distinct crossings. The rewire is defined for every PD-code. It is a Reidemeister move when the selected crossings satisfy HasReidemeisterThreeTriangle.

Equations

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

@[simp]

theorem TauCeti.PDCode.reidemeisterThree_halfEdge {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (D.reidemeisterThree c).halfEdge = D.halfEdge

The move keeps the names of its half-edges.

theorem TauCeti.PDCode.reidemeisterThree_crossing {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (i : Fin n) (s : Fin 4) : (D.reidemeisterThree c).crossing i s = D.crossing i s

The move keeps the slots at each named crossing.

@[simp]

theorem TauCeti.PDCode.reidemeisterThree_overPair {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (i : Fin n) : (D.reidemeisterThree c).overPair i = D.overPair ((Equiv.swap (c 0) (c 2)) i)

The first and third crossing exchange their over-pair indicators; all other crossing indicators stay at their old names.

@[simp]

theorem TauCeti.PDCode.reidemeisterThree_crossinglessComponentCount {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (D.reidemeisterThree c).crossinglessComponentCount = D.crossinglessComponentCount

The move keeps crossing-free circles.

theorem TauCeti.PDCode.reidemeisterThree_edgePair {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : ↑(D.reidemeisterThree c).edgePair = (Equiv.permCongr (D.reidemeisterThreePerm c)) ↑D.edgePair

The arc matching after the move is the transport of the original matching by the local half-edge permutation.

theorem TauCeti.PDCode.reidemeisterThree_edgePair_transport {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (x : Fin (4 * n)) : ↑(D.reidemeisterThree c).edgePair ((D.reidemeisterThreePerm c) x) = (D.reidemeisterThreePerm c) (↑D.edgePair x)

Transport an arc across the replacement of the local twelve half-edges.

theorem TauCeti.PDCode.reidemeisterThree_triangleArcs {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangleArcs c) : ↑(D.reidemeisterThree c).edgePair (D.crossing (c 0) 1) = D.crossing (c 1) 3 ∧ ↑(D.reidemeisterThree c).edgePair (D.crossing (c 1) 2) = D.crossing (c 2) 0 ∧ ↑(D.reidemeisterThree c).edgePair (D.crossing (c 0) 2) = D.crossing (c 2) 3

The replacement has the three internal arcs of σ₂ σ₁ σ₂.

theorem TauCeti.PDCode.componentPerm_reidemeisterThree {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (D.reidemeisterThree c).componentPerm = (Equiv.permCongr (D.reidemeisterThreePerm c)) D.componentPerm

Component traversal is conjugated by the local rewire.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_reidemeisterThree {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (D.reidemeisterThree c).crossingComponentCount = D.crossingComponentCount

The third Reidemeister move preserves crossing-bearing link components.

@[simp]

theorem TauCeti.PDCode.componentCount_reidemeisterThree {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (D.reidemeisterThree c).componentCount = D.componentCount

The third Reidemeister move preserves the total number of link components.

@[simp]

theorem TauCeti.PDCode.hasReidemeisterThreeTriangleArcs_mirror_iff {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : D.mirror.HasReidemeisterThreeTriangleArcs c ↔ D.HasReidemeisterThreeTriangleArcs c

Reversing every strand height preserves the three internal triangle arcs.

@[simp]

theorem TauCeti.PDCode.hasReidemeisterThreeTriangle_mirror_iff {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : D.mirror.HasReidemeisterThreeTriangle c ↔ D.HasReidemeisterThreeTriangle c

Reversing every strand height preserves the triangle condition.

@[simp]

theorem TauCeti.PDCode.reidemeisterThreePerm_mirror {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : D.mirror.reidemeisterThreePerm c = D.reidemeisterThreePerm c

The local half-edge rewire is independent of the strand heights.

@[simp]

theorem TauCeti.PDCode.mirror_reidemeisterThree {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (D.reidemeisterThree c).mirror = D.mirror.reidemeisterThree c

Mirroring commutes with the third Reidemeister move.