Local permutation calculus for the third Reidemeister move

The Kauffman bracket and planarity proofs use the same twelve-slot inclusion and the same remainder after removing the three internal triangle arcs. This module supplies their common permutation calculus, exterior crossing-slot permutations, and lifted swap-forest orbit counts; smoothing and face traversal specialize these constructions in the two consumers.

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

The three internal arcs of the original Reidemeister triangle, extended by identity.

Equations

• TauCeti.PDCode.ReidemeisterThree.localInternalMatching = Equiv.swap (0, 2) (1, 0) * Equiv.swap (1, 1) (2, 3) * Equiv.swap (0, 1) (2, 0)

theorem TauCeti.PDCode.ReidemeisterThree.localInternalMatching_def : localInternalMatching = Equiv.swap (0, 2) (1, 0) * Equiv.swap (1, 1) (2, 3) * Equiv.swap (0, 1) (2, 0)

The internal matching is the product of the three disjoint triangle-arc swaps.

theorem TauCeti.PDCode.ReidemeisterThree.localInternalMatching_apply_apply (p : Fin 3 × Fin 4) : localInternalMatching (localInternalMatching p) = p

Traversing an internal arc twice returns to the original slot.

theorem TauCeti.PDCode.ReidemeisterThree.localInternalMatching_mul_self : localInternalMatching * localInternalMatching = 1

The internal matching is an involutive permutation.

def TauCeti.PDCode.ReidemeisterThree.localInternal (p : Fin 3 × Fin 4) : Prop

The six slots incident to the internal arcs of the original triangle.

Equations

• TauCeti.PDCode.ReidemeisterThree.localInternal p = (p = (0, 1) ∨ p = (0, 2) ∨ p = (1, 0) ∨ p = (1, 1) ∨ p = (2, 0) ∨ p = (2, 3))

theorem TauCeti.PDCode.ReidemeisterThree.localInternal_iff (p : Fin 3 × Fin 4) : localInternal p ↔ p = (0, 1) ∨ p = (0, 2) ∨ p = (1, 0) ∨ p = (1, 1) ∨ p = (2, 0) ∨ p = (2, 3)

The internal slots are exactly the six endpoints of the three triangle arcs.

@[instance_reducible]

instance TauCeti.PDCode.ReidemeisterThree.instDecidableLocalInternal (p : Fin 3 × Fin 4) : Decidable (localInternal p)

Membership in the six internal slots is decidable.

Equations

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

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

Extend a permutation of the twelve selected slots by identity on other crossings.

Equations

• TauCeti.PDCode.ReidemeisterThree.localLift D c = Equiv.Perm.extendDomainHom (TauCeti.PDCode.ReidemeisterThree.triangleEmbedding D c).toEquivRange

theorem TauCeti.PDCode.ReidemeisterThree.localLift_apply {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (p : Equiv.Perm (Fin 3 × Fin 4)) (x : Fin 3 × Fin 4) : ((localLift D c) p) ((triangleEmbedding D c) x) = (triangleEmbedding D c) (p x)

A lifted permutation acts according to its local slot permutation.

theorem TauCeti.PDCode.ReidemeisterThree.localLift_fixed {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (p : Equiv.Perm (Fin 3 × Fin 4)) {i : Fin n} (hi : i ∉ Set.range ⇑c) (s : Fin 4) : ((localLift D c) p) (D.crossing i s) = D.crossing i s

Lifting fixes every half-edge at an unselected crossing.

theorem TauCeti.PDCode.ReidemeisterThree.localLift_swap {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (a b : Fin 3 × Fin 4) : (localLift D c) (Equiv.swap a b) = Equiv.swap ((triangleEmbedding D c) a) ((triangleEmbedding D c) b)

Lifting a transposition gives the transposition of its two ambient half-edges.

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

Act by the specified slot permutation at each unselected crossing and fix all twelve slots of the selected triangle.

Equations

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

theorem TauCeti.PDCode.ReidemeisterThree.exteriorSlots_def {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (slots : Fin n → Equiv.Perm (Fin 4)) : exteriorSlots D c slots = (Equiv.permCongr D.halfEdge) ((crossingSlotEquiv n).permCongr (Equiv.prodCongrRight fun (i : Fin n) => if i ∈ Set.range ⇑c then 1 else slots i))

Exterior slot permutations transport the crossingwise action through the diagram's half-edge labeling.

theorem TauCeti.PDCode.ReidemeisterThree.exteriorSlots_crossing {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (slots : Fin n → Equiv.Perm (Fin 4)) (i : Fin n) (s : Fin 4) : (exteriorSlots D c slots) (D.crossing i s) = D.crossing i ((if i ∈ Set.range ⇑c then 1 else slots i) s)

Exterior slot permutations act crossing by crossing, with identity on selected crossings.

theorem TauCeti.PDCode.ReidemeisterThree.exteriorSlots_local {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (slots : Fin n → Equiv.Perm (Fin 4)) (p : Fin 3 × Fin 4) : (exteriorSlots D c slots) ((triangleEmbedding D c) p) = (triangleEmbedding D c) p

Exterior slot permutations fix every slot of the selected triangle.

theorem TauCeti.PDCode.ReidemeisterThree.localLift_commute_exteriorSlots {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (p : Equiv.Perm (Fin 3 × Fin 4)) (slots : Fin n → Equiv.Perm (Fin 4)) : Commute ((localLift D c) p) (exteriorSlots D c slots)

Permutations supported on the selected triangle commute with exterior slot permutations.

theorem TauCeti.PDCode.ReidemeisterThree.localLift_swapForest_orbitCount {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (factor base : Equiv.Perm (Fin 3 × Fin 4)) (factors : List ((Fin 3 × Fin 4) × Fin 3 × Fin 4)) (outside : Equiv.Perm (Fin (4 * n))) (hforest : factors.IsSwapForest) (hfactor : factor = (List.map (Function.uncurry Equiv.swap) factors).prod * base) (hfixed : ∀ p ∈ factors, ((localLift D c) base * outside) ((triangleEmbedding D c) p.2) = (triangleEmbedding D c) p.2) : orbitCount ((localLift D c) factor * outside) + factors.length = orbitCount ((localLift D c) base * outside)

Lift a swap-forest factorization into the diagram. If the remaining traversal fixes all second endpoints, inserting the forest removes one orbit per factor.

theorem TauCeti.PDCode.ReidemeisterThree.internalMatching_edgePair {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangleArcs c) (p : Fin 3 × Fin 4) (hp : localInternal p) : ↑D.edgePair ((triangleEmbedding D c) p) = (triangleEmbedding D c) (localInternalMatching p)

The prescribed triangle arcs agree with the local internal matching.

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

Remove the three internal arcs, leaving their six slots fixed by the remainder.

Equations

• TauCeti.PDCode.ReidemeisterThree.outsideEdges D c = (TauCeti.PDCode.ReidemeisterThree.localLift D c) TauCeti.PDCode.ReidemeisterThree.localInternalMatching * ↑D.edgePair

theorem TauCeti.PDCode.ReidemeisterThree.outsideEdges_def {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : outsideEdges D c = (localLift D c) localInternalMatching * ↑D.edgePair

Removing the internal arcs composes the original matching with their three swaps.

theorem TauCeti.PDCode.ReidemeisterThree.localLift_remove_internal {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (p : Equiv.Perm (Fin 3 × Fin 4)) (outside : Equiv.Perm (Fin (4 * n))) (hcomm : Commute ((localLift D c) localInternalMatching) outside) : (localLift D c) (p * localInternalMatching) * outside * outsideEdges D c = (localLift D c) p * outside * ↑D.edgePair

Cancel the internal matching against the removed triangle arcs when the intervening outside permutation commutes with that matching.

theorem TauCeti.PDCode.ReidemeisterThree.outsideEdges_internal {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangleArcs c) (p : Fin 3 × Fin 4) (hp : localInternal p) : (outsideEdges D c) ((triangleEmbedding D c) p) = (triangleEmbedding D c) p

Removing the triangle arcs fixes each of their six incident slots.

theorem TauCeti.PDCode.ReidemeisterThree.localLift_slots {n : ℕ} (D : PDCode n) (c : Fin 3 ↪ Fin n) : (localLift D c) reidemeisterThreeSlots = D.reidemeisterThreePerm c

The lifted twelve-slot rewire is the half-edge permutation of the move.