PD-codes

A PD-code records finite combinatorial crossing data for a link. The halfEdge permutation lists the four half-edges at each crossing, while the perfect matching edgePair joins the two half-edges at the ends of each arc. Opposite slots form the two local strands, one of which is selected by overPair. Crossing-free components are recorded separately.

OrientedPDCode decorates this data with compatible directions on the arcs and crossing-free components. FramedOrientedPDCode further assigns an integer framing to every component. The forgetful maps between these three presentation layers let results use only the data they need.

This is a code-level presentation: PDCode neither imposes planarity nor provides a geometric realization, so these must be supplied separately. Keeping the code finite and explicit avoids choosing a privileged geometric embedding.

The PD-code encoding adapts M. Mastin, Links and Planar Diagram Codes, Definitions 2--3, which develops the Bar-Natan/KnotTheory PD convention. Mastin lists, at each crossing, the labels of the four incident arcs counterclockwise from the incoming under-edge. Here halfEdge labels half-edges rather than arcs, the four slots of a crossing are read counterclockwise from any starting slot, the over-strand is recorded by the separate bit overPair, and crossing-free components are counted separately. The diagram and crossing-sign conventions follow W. B. R. Lickorish, An Introduction to Knot Theory, GTM 175, Chapter 1. The framing convention follows R. Gompf and A. Stipsicz, 4-Manifolds and Kirby Calculus, GSM 20, Section 4.5, especially Proposition 4.5.8.

Main definitions

• TauCeti.PDCode: an unoriented PD-code with n crossings.
• TauCeti.OrientedPDCode: an orientation decoration of a PD-code.
• TauCeti.FramedOrientedPDCode: a framing decoration of an oriented PD-code.
• TauCeti.PDCode.halfEdgeSuccEquiv: the half-edge positions of a code with one crossing more.
• TauCeti.PDCode.mirror and TauCeti.PDCode.relabel: reflection and relabelling along equivalences of the finite index types.
• TauCeti.PDCode.reconnect: reconnect the arcs ending at two half-edges, joining them.
• TauCeti.PDCode.slotSmoothing: the two smoothings of the four slots at a crossing.
• TauCeti.PDCode.kink: the one-crossing kink diagram, and TauCeti.OrientedPDCode.positiveKink, its orientation with a positive crossing.
• TauCeti.OrientedPDCode.reverse: reversal of every component orientation.
• TauCeti.OrientedPDCode.crossingSign: the sign derived from the local oriented crossing data.
• TauCeti.OrientedPDCode.writhe: the sum of the crossing signs.

Main results

• TauCeti.OrientedPDCode.crossingSign_eq_one_iff and crossingSign_eq_neg_one_iff characterize the two possible crossing signs.
• TauCeti.PDCode.mirror_mirror and TauCeti.PDCode.relabel_relabel give the basic operation laws.
• TauCeti.OrientedPDCode.unlinkEquiv classifies zero-crossing oriented PD-codes.

def TauCeti.PDCode.crossingSlotEquiv (n : ℕ) : Fin n × Fin 4 ≃ Fin (4 * n)

The standard equivalence between crossing-slot pairs and the 4 * n half-edge positions.

Equations

• TauCeti.PDCode.crossingSlotEquiv n = finProdFinEquiv.trans (finCongr ⋯)

@[simp]

theorem TauCeti.PDCode.crossingSlotEquiv_apply_val {n : ℕ} (i : Fin n) (slot : Fin 4) : ↑((crossingSlotEquiv n) (i, slot)) = ↑slot + 4 * ↑i

The crossing-slot equivalence numbers slot s at crossing i by s + 4 * i.

def TauCeti.PDCode.halfEdgeSuccEquiv (n : ℕ) : Fin (4 * n) ⊕ Fin 4 ≃ Fin (4 * (n + 1))

The half-edge positions of a code with one crossing more: the 4 * n positions of the first n crossings, followed by the four slots of the new last crossing.

Equations

• TauCeti.PDCode.halfEdgeSuccEquiv n = finSumFinEquiv.trans (finCongr ⋯)

@[simp]

theorem TauCeti.PDCode.crossingSlotEquiv_succ_castSucc {n : ℕ} (i : Fin n) (slot : Fin 4) : (crossingSlotEquiv (n + 1)) (i.castSucc, slot) = (halfEdgeSuccEquiv n) (Sum.inl ((crossingSlotEquiv n) (i, slot)))

A slot of one of the first n crossings keeps its half-edge position when a crossing is added last.

@[simp]

theorem TauCeti.PDCode.crossingSlotEquiv_succ_last {n : ℕ} (slot : Fin 4) : (crossingSlotEquiv (n + 1)) (Fin.last n, slot) = (halfEdgeSuccEquiv n) (Sum.inr slot)

The slots of the last crossing occupy the last four half-edge positions.

theorem TauCeti.PDCode.crossingSlotEquiv_apply_val_mod_four {n : ℕ} (i : Fin n) (slot : Fin 4) : ↑((crossingSlotEquiv n) (i, slot)) % 4 = ↑slot

The slot of a half-edge is recovered from its position modulo four.

@[simp]

theorem TauCeti.PDCode.halfEdgeSuccEquiv_apply_inl_val {n : ℕ} (x : Fin (4 * n)) : ↑((halfEdgeSuccEquiv n) (Sum.inl x)) = ↑x

A half-edge position of the first n crossings keeps its value when a crossing is added.

@[simp]

theorem TauCeti.PDCode.halfEdgeSuccEquiv_apply_inr_val {n : ℕ} (slot : Fin 4) : ↑((halfEdgeSuccEquiv n) (Sum.inr slot)) = ↑slot + 4 * n

The slots of the added crossing follow the 4 * n positions of the first n crossings.

def TauCeti.PDCode.oppositeCrossingSlot : Equiv.Perm (Fin 4)

The slot opposite a given slot in the cyclic order at a crossing.

Equations

• TauCeti.PDCode.oppositeCrossingSlot = finCycle 2

theorem TauCeti.PDCode.oppositeCrossingSlot_apply (slot : Fin 4) : oppositeCrossingSlot slot = slot + 2

The opposite crossing slot is obtained by adding two cyclically.

@[simp]

theorem TauCeti.PDCode.oppositeCrossingSlot_apply_val (slot : Fin 4) : ↑(oppositeCrossingSlot slot) = ↑(slot + 2)

The value of the opposite crossing slot.

theorem TauCeti.PDCode.oppositeCrossingSlot_eq_swap_mul_swap : oppositeCrossingSlot = Equiv.swap 0 2 * Equiv.swap 1 3

The opposite-slot permutation swaps slots 0, 2 and slots 1, 3.

theorem TauCeti.PDCode.two_le_oppositeCrossingSlot_val_iff (slot : Fin 4) : 2 ≤ ↑(oppositeCrossingSlot slot) ↔ ¬2 ≤ ↑slot

Exactly one of a slot and its opposite slot is one of the last two slots 2, 3.

@[simp]

theorem TauCeti.PDCode.oppositeCrossingSlot_apply_oppositeCrossingSlot (slot : Fin 4) : oppositeCrossingSlot (oppositeCrossingSlot slot) = slot

Taking the opposite crossing slot twice returns to the original slot.

def TauCeti.PDCode.slotSmoothing (b : Bool) : Equiv.Perm (Fin 4)

The two smoothings of the four slots at a crossing, indexed by an over-pair indicator. slotSmoothing false pairs slot 0 with slot 3 and slot 1 with slot 2, and slotSmoothing true pairs slot 0 with slot 1 and slot 2 with slot 3: in both cases each slot of the pair indicated is joined to the slot preceding it in the counterclockwise order. Applied to D.overPair i it is therefore the A-smoothing at crossing i, the one turning left off the over-strand, and applied to !D.overPair i the B-smoothing.

Equations

• TauCeti.PDCode.slotSmoothing b = if b = true then Equiv.swap 0 1 * Equiv.swap 2 3 else Equiv.swap 0 3 * Equiv.swap 1 2

@[simp]

theorem TauCeti.PDCode.slotSmoothing_true : slotSmoothing true = Equiv.swap 0 1 * Equiv.swap 2 3

The true smoothing pairs slots 0-1 and 2-3.

@[simp]

theorem TauCeti.PDCode.slotSmoothing_false : slotSmoothing false = Equiv.swap 0 3 * Equiv.swap 1 2

The false smoothing pairs slots 0-3 and 1-2.

@[simp]

theorem TauCeti.PDCode.slotSmoothing_apply_apply (b : Bool) (slot : Fin 4) : (slotSmoothing b) ((slotSmoothing b) slot) = slot

A local smoothing is an involution of the four slots.

theorem TauCeti.PDCode.slotSmoothing_ne (b : Bool) (slot : Fin 4) : (slotSmoothing b) slot ≠ slot

A local smoothing moves every slot: it pairs the four slots off into two arcs.

theorem Fin.oppositeCrossingSlot_ne (slot : Fin 4) : TauCeti.PDCode.oppositeCrossingSlot slot ≠ slot

The opposite crossing slot is different from the original slot.

structure TauCeti.PDCode (n : ℕ) : Type

A finite unoriented PD-code with n crossings.

The 4 * n half-edges are grouped into four slots for each crossing by halfEdge, listed counterclockwise around the crossing. The perfect matching edgePair joins the two half-edges at the ends of each arc. Slots 0 and 2 form one local strand, while slots 1 and 3 form the other. crossinglessComponentCount counts circle components which meet no crossing. overPair i = false selects the 0-2 strand as over, while true selects the 1-3 strand.

• halfEdge : Equiv.Perm (Fin (4 * n))

  The half-edge labels occupying the four slots of each crossing.

• edgePair : PerfectMatching (Fin (4 * n))

  The perfect matching pairing the two half-edges at the ends of each arc.

• crossinglessComponentCount : ℕ

  The number of circle components which meet no crossing.

• overPair : Fin n → Bool

  Which of the two opposite-slot strands is over at each crossing.

theorem TauCeti.PDCode.ext_iff {n : ℕ} {x y : PDCode n} : x = y ↔ x.halfEdge = y.halfEdge ∧ x.edgePair = y.edgePair ∧ x.crossinglessComponentCount = y.crossinglessComponentCount ∧ x.overPair = y.overPair

theorem TauCeti.PDCode.ext {n : ℕ} {x y : PDCode n} (halfEdge : x.halfEdge = y.halfEdge) (edgePair : x.edgePair = y.edgePair) (crossinglessComponentCount : x.crossinglessComponentCount = y.crossinglessComponentCount) (overPair : x.overPair = y.overPair) : x = y

structure TauCeti.OrientedPDCode (n : ℕ) extends TauCeti.PDCode n : Type

An oriented PD-code, consisting of an unoriented code and compatible component directions.

• halfEdge : Equiv.Perm (Fin (4 * n))
• edgePair : PerfectMatching (Fin (4 * n))
• crossinglessComponentCount : ℕ
• overPair : Fin n → Bool
• orientation : Fin (4 * n) → Bool

  Whether an arc points away from its incident crossing (true) or toward it (false).

• orientation_edgePair (h : Fin (4 * n)) : self.orientation (↑self.edgePair h) = !self.orientation h

  The direction on an arc reverses at its paired half-edge.

• orientation_oppositeCrossingSlot (i : Fin n) (slot : Fin 4) : self.orientation (self.halfEdge ((PDCode.crossingSlotEquiv n) (i, PDCode.oppositeCrossingSlot slot))) = !self.orientation (self.halfEdge ((PDCode.crossingSlotEquiv n) (i, slot)))

  The orientation reverses between the opposite slots belonging to each local strand.

• crossinglessComponents : Multiset Bool

  The orientations of the circle components which meet no crossing, one entry per component. For such a circle, true and false simply label its two orientations, which TauCeti.OrientedPDCode.reverse exchanges.

• card_crossinglessComponents : self.crossinglessComponents.card = self.crossinglessComponentCount

  The orientation multiset has one entry per crossing-free component of the underlying code.

theorem TauCeti.OrientedPDCode.ext_iff {n : ℕ} {x y : OrientedPDCode n} : x = y ↔ x.toPDCode = y.toPDCode ∧ x.orientation = y.orientation ∧ x.crossinglessComponents = y.crossinglessComponents

theorem TauCeti.OrientedPDCode.ext {n : ℕ} {x y : OrientedPDCode n} (toPDCode : x.toPDCode = y.toPDCode) (orientation : x.orientation = y.orientation) (crossinglessComponents : x.crossinglessComponents = y.crossinglessComponents) : x = y

structure TauCeti.FramedOrientedPDCode (n : ℕ) extends TauCeti.OrientedPDCode n : Type

A framed oriented PD-code.

On a component meeting a crossing, framing is an integer constant along arc pairings and local strands. For crossing-free components, crossinglessFramings keeps each orientation paired with its framing integer. These integers measure the chosen framing relative to the Seifert (0-) framing. The diagram's blackboard framing instead has coefficient equal to the component writhe.

• halfEdge : Equiv.Perm (Fin (4 * n))
• edgePair : PerfectMatching (Fin (4 * n))
• crossinglessComponentCount : ℕ
• overPair : Fin n → Bool
• orientation : Fin (4 * n) → Bool
• orientation_edgePair (h : Fin (4 * n)) : self.orientation (↑self.edgePair h) = !self.orientation h
• orientation_oppositeCrossingSlot (i : Fin n) (slot : Fin 4) : self.orientation (self.halfEdge ((PDCode.crossingSlotEquiv n) (i, PDCode.oppositeCrossingSlot slot))) = !self.orientation (self.halfEdge ((PDCode.crossingSlotEquiv n) (i, slot)))
• crossinglessComponents : Multiset Bool
• card_crossinglessComponents : self.crossinglessComponents.card = self.crossinglessComponentCount
• framing : Fin (4 * n) → ℤ

  The Seifert-relative framing coefficient of the component through each half-edge.

• framing_edgePair (h : Fin (4 * n)) : self.framing (↑self.edgePair h) = self.framing h

  Framing is constant along an arc.

• framing_oppositeCrossingSlot (i : Fin n) (slot : Fin 4) : self.framing (self.halfEdge ((PDCode.crossingSlotEquiv n) (i, PDCode.oppositeCrossingSlot slot))) = self.framing (self.halfEdge ((PDCode.crossingSlotEquiv n) (i, slot)))

  Framing is constant along a local strand through a crossing.

• crossinglessFramings : Multiset (Bool × ℤ)

  The orientation and Seifert-relative framing coefficient of each crossing-free component.

• map_fst_crossinglessFramings : Multiset.map Prod.fst self.crossinglessFramings = self.crossinglessComponents

  Forgetting framings recovers the oriented crossing-free components.

theorem TauCeti.FramedOrientedPDCode.ext_iff {n : ℕ} {x y : FramedOrientedPDCode n} : x = y ↔ x.toOrientedPDCode = y.toOrientedPDCode ∧ x.framing = y.framing ∧ x.crossinglessFramings = y.crossinglessFramings

theorem TauCeti.FramedOrientedPDCode.ext {n : ℕ} {x y : FramedOrientedPDCode n} (toOrientedPDCode : x.toOrientedPDCode = y.toOrientedPDCode) (framing : x.framing = y.framing) (crossinglessFramings : x.crossinglessFramings = y.crossinglessFramings) : x = y

def TauCeti.PDCode.crossing {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : Fin (4 * n)

The four half-edge labels at a crossing, in counterclockwise cyclic order.

Equations

• D.crossing i slot = D.halfEdge ((TauCeti.PDCode.crossingSlotEquiv n) (i, slot))

@[simp]

theorem TauCeti.PDCode.crossing_apply {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : D.crossing i slot = D.halfEdge ((crossingSlotEquiv n) (i, slot))

The explicit formula for the half-edge in a specified crossing slot.

theorem TauCeti.PDCode.eq_permCongr_sumCongr_of_halfEdge_eq {n : ℕ} {D : PDCode n} {D' : PDCode (n + 1)} (hD : D'.halfEdge = (halfEdgeSuccEquiv n).permCongr (D.halfEdge.sumCongr 1)) {σ : Equiv.Perm (Fin (4 * n))} {τ : Equiv.Perm (Fin (4 * (n + 1)))} (f : Fin (n + 1) → Equiv.Perm (Fin 4)) (hσ : ∀ (i : Fin n) (slot : Fin 4), σ (D.halfEdge ((crossingSlotEquiv n) (i, slot))) = D.crossing i ((f i.castSucc) slot)) (hτ : ∀ (i : Fin (n + 1)) (slot : Fin 4), τ (D'.halfEdge ((crossingSlotEquiv (n + 1)) (i, slot))) = D'.crossing i ((f i) slot)) : τ = (halfEdgeSuccEquiv n).permCongr (σ.sumCongr (f (Fin.last n)))

Let D' be a code with one crossing more than D, whose first n crossings keep the half-edges of D and whose last crossing takes the four new half-edge positions. A permutation of the half-edges of D' that acts at each crossing i by the local permutation f i of its slots is the permutation of the half-edges of D acting at each crossing i by f i.castSucc, together with f (Fin.last n) on the four new slots.

def TauCeti.PDCode.isOver {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : Bool

Whether a slot belongs to the over-strand at its crossing.

Equations

• D.isOver i slot = (D.overPair i == decide (slot = 1 ∨ slot = 3))

theorem TauCeti.PDCode.isOver_def {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : D.isOver i slot = (D.overPair i == decide (slot = 1 ∨ slot = 3))

The defining equation for the over-strand indicator of a slot: it compares the over-pair indicator with the parity of the slot.

@[simp]

theorem TauCeti.PDCode.isOver_zero {n : ℕ} (D : PDCode n) (i : Fin n) : D.isOver i 0 = !D.overPair i

Slot zero is over exactly when the second opposite-slot pair was not selected.

@[simp]

theorem TauCeti.PDCode.isOver_one {n : ℕ} (D : PDCode n) (i : Fin n) : D.isOver i 1 = D.overPair i

Slot one is over exactly when the second opposite-slot pair was selected.

@[simp]

theorem TauCeti.PDCode.isOver_two {n : ℕ} (D : PDCode n) (i : Fin n) : D.isOver i 2 = !D.overPair i

Slot two is over exactly when the second opposite-slot pair was not selected.

@[simp]

theorem TauCeti.PDCode.isOver_three {n : ℕ} (D : PDCode n) (i : Fin n) : D.isOver i 3 = D.overPair i

Slot three is over exactly when the second opposite-slot pair was selected.

@[simp]

theorem TauCeti.PDCode.isOver_oppositeCrossingSlot {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : D.isOver i (oppositeCrossingSlot slot) = D.isOver i slot

Opposite slots belong to the same over- or under-strand.

def TauCeti.PDCode.mirror {n : ℕ} (D : PDCode n) : PDCode n

Reflect a diagram by swapping the over- and under-strands.

Equations

• D.mirror = { halfEdge := D.halfEdge, edgePair := D.edgePair, crossinglessComponentCount := D.crossinglessComponentCount, overPair := fun (i : Fin n) => !D.overPair i }

@[simp]

theorem TauCeti.PDCode.mirror_halfEdge {n : ℕ} (D : PDCode n) : D.mirror.halfEdge = D.halfEdge

Reflection leaves the half-edge order unchanged.

@[simp]

theorem TauCeti.PDCode.mirror_edgePair {n : ℕ} (D : PDCode n) : D.mirror.edgePair = D.edgePair

Reflection leaves the arc matching unchanged.

@[simp]

theorem TauCeti.PDCode.mirror_crossinglessComponentCount {n : ℕ} (D : PDCode n) : D.mirror.crossinglessComponentCount = D.crossinglessComponentCount

Reflection preserves the number of crossing-free components.

@[simp]

theorem TauCeti.PDCode.mirror_overPair {n : ℕ} (D : PDCode n) (i : Fin n) : D.mirror.overPair i = !D.overPair i

Reflection complements each over-strand choice.

theorem TauCeti.PDCode.crossing_mirror {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : D.mirror.crossing i slot = D.crossing i slot

Reflection leaves every labelled crossing slot unchanged.

@[simp]

theorem TauCeti.PDCode.isOver_mirror {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : D.mirror.isOver i slot = !D.isOver i slot

Reflection interchanges over- and under-slots.

@[simp]

theorem TauCeti.PDCode.mirror_mirror {n : ℕ} (D : PDCode n) : D.mirror.mirror = D

Reflecting a PD-code twice gives the original code.

@[simp]

theorem TauCeti.PDCode.mirror_eq_self_of_zero_crossings (D : PDCode 0) : D.mirror = D

Reflection fixes every PD-code without crossings.

def TauCeti.PDCode.reconnect {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : PDCode n

Reconnecting two arcs. Cut the arc of D ending at the half-edge p and the arc ending at q, and join p to q and the other end D.edgePair.val p of the first arc to the other end D.edgePair.val q of the second (TauCeti.PerfectMatching.reconnect). The crossings, their over-strands and the crossing-free circles are unchanged. This is how a smoothing of a crossing added by TauCeti.PDCode.insertCrossing reconnects the cut arcs. The two arcs are distinct when q ≠ p and q ≠ D.edgePair.val p; when q = D.edgePair.val p both choices name the same arc and the code is left unchanged.

Equations

• D.reconnect p q = { halfEdge := D.halfEdge, edgePair := D.edgePair.reconnect p q, crossinglessComponentCount := D.crossinglessComponentCount, overPair := D.overPair }

@[simp]

theorem TauCeti.PDCode.reconnect_halfEdge {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : (D.reconnect p q).halfEdge = D.halfEdge

Reconnecting arcs keeps the half-edges at the crossings.

@[simp]

theorem TauCeti.PDCode.reconnect_overPair {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : (D.reconnect p q).overPair = D.overPair

Reconnecting arcs keeps the over-strands.

@[simp]

theorem TauCeti.PDCode.reconnect_crossinglessComponentCount {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : (D.reconnect p q).crossinglessComponentCount = D.crossinglessComponentCount

Reconnecting arcs keeps the crossing-free circles.

@[simp]

theorem TauCeti.PDCode.reconnect_edgePair {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : (D.reconnect p q).edgePair = D.edgePair.reconnect p q

Reconnecting arcs of the code reconnects its perfect matching of half-edges.

@[simp]

theorem TauCeti.PDCode.reconnect_partner {n : ℕ} (D : PDCode n) (p : Fin (4 * n)) : D.reconnect p (↑D.edgePair p) = D

Reconnecting the two ends of one arc leaves the code unchanged.

@[simp]

theorem TauCeti.PDCode.reconnect_self {n : ℕ} (D : PDCode n) (p : Fin (4 * n)) : D.reconnect p p = D

Reconnecting a half-edge with itself leaves the code unchanged.

theorem TauCeti.PDCode.reconnect_edgePair_val {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : ↑(D.reconnect p q).edgePair = (Equiv.permCongr (Equiv.swap (↑D.edgePair p) q)) ↑D.edgePair

The arcs of the reconnected code are the old arcs conjugated by the transposition of D.edgePair.val p with q.

@[simp]

theorem TauCeti.PDCode.mirror_reconnect {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) : (D.reconnect p q).mirror = D.mirror.reconnect p q

Mirroring commutes with reconnecting arcs.

def TauCeti.PDCode.crossingBlockEquiv {n m : ℕ} (cross : Fin n ≃ Fin m) : Fin (4 * n) ≃ Fin (4 * m)

The equivalence of half-edge positions induced by an equivalence of crossing names. It changes the crossing coordinate and preserves the slot coordinate.

Equations

• TauCeti.PDCode.crossingBlockEquiv cross = (TauCeti.PDCode.crossingSlotEquiv n).symm.trans ((cross.prodCongr (Equiv.refl (Fin 4))).trans (TauCeti.PDCode.crossingSlotEquiv m))

@[simp]

theorem TauCeti.PDCode.crossingBlockEquiv_apply_crossingSlotEquiv {n m : ℕ} (cross : Fin n ≃ Fin m) (i : Fin n) (slot : Fin 4) : (crossingBlockEquiv cross) ((crossingSlotEquiv n) (i, slot)) = (crossingSlotEquiv m) (cross i, slot)

A crossing-block equivalence changes the crossing coordinate and preserves its slot.

@[simp]

theorem TauCeti.PDCode.crossingBlockEquiv_symm {n m : ℕ} (cross : Fin n ≃ Fin m) : (crossingBlockEquiv cross).symm = crossingBlockEquiv cross.symm

The inverse of a crossing-block equivalence is induced by the inverse crossing equivalence.

@[simp]

theorem TauCeti.PDCode.crossingBlockEquiv_refl {n : ℕ} : crossingBlockEquiv (Equiv.refl (Fin n)) = Equiv.refl (Fin (4 * n))

The identity equivalence of crossing names induces the identity equivalence of half-edges.

@[simp]

theorem TauCeti.PDCode.crossingBlockEquiv_trans {n m r : ℕ} (cross₁ : Fin n ≃ Fin m) (cross₂ : Fin m ≃ Fin r) : crossingBlockEquiv (cross₁.trans cross₂) = (crossingBlockEquiv cross₁).trans (crossingBlockEquiv cross₂)

Crossing-block equivalences preserve composition.

def TauCeti.PDCode.relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : PDCode m

Relabel the half-edges and crossings of a code along equivalences of their index types: the half-edge h becomes half h and the crossing j becomes cross j. Slots are kept, so the half-edge in slot s of crossing cross j is half of the half-edge in slot s of crossing j; arcs join the images of the half-edges they joined, the over-strand choice at cross j is the one at j, and the number of crossing-free components is unchanged. The half-edge equivalence need not be the one induced by the crossing equivalence.

Equations

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

@[simp]

theorem TauCeti.PDCode.relabel_halfEdge {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).halfEdge = ((crossingBlockEquiv cross).equivCongr half) D.halfEdge

The half-edge permutation of a relabelled code is half ∘ D.halfEdge ∘ (crossingBlockEquiv cross).symm: the half-edge in slot s of crossing cross j is half of the half-edge of D in slot s of crossing j.

@[simp]

theorem TauCeti.PDCode.relabel_edgePair {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).edgePair = (PerfectMatching.congr half) D.edgePair

Relabelling transports the perfect matching along the half-edge equivalence.

@[simp]

theorem TauCeti.PDCode.relabel_crossinglessComponentCount {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).crossinglessComponentCount = D.crossinglessComponentCount

Relabelling preserves the number of crossing-free components.

@[simp]

theorem TauCeti.PDCode.relabel_overPair {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (i : Fin m) : (D.relabel half cross).overPair i = D.overPair (cross.symm i)

Relabelling reads the over-strand choice at the old crossing name.

theorem TauCeti.PDCode.crossing_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (i : Fin m) (slot : Fin 4) : (D.relabel half cross).crossing i slot = half (D.crossing (cross.symm i) slot)

Relabelling transports every crossing block together with its slot order.

@[simp]

theorem TauCeti.PDCode.isOver_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (i : Fin m) (slot : Fin 4) : (D.relabel half cross).isOver i slot = D.isOver (cross.symm i) slot

The over/under status after relabelling is read at the old crossing name.

@[simp]

theorem TauCeti.PDCode.relabel_refl {n : ℕ} (D : PDCode n) : D.relabel (Equiv.refl (Fin (4 * n))) (Equiv.refl (Fin n)) = D

Relabelling by identity equivalences does nothing.

@[simp]

theorem TauCeti.PDCode.relabel_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) {r : ℕ} (half₂ : Fin (4 * m) ≃ Fin (4 * r)) (cross₂ : Fin m ≃ Fin r) : (D.relabel half cross).relabel half₂ cross₂ = D.relabel (half.trans half₂) (cross.trans cross₂)

Consecutive relabellings compose their half-edge and crossing equivalences.

@[simp]

theorem TauCeti.PDCode.mirror_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).mirror = D.mirror.relabel half cross

Reflection commutes with relabelling.

def TauCeti.PDCode.kink : PDCode 1

The one-crossing knot diagram: a single kink. Its single crossing has the slot pair 1-3 as its over-strand, and its two arcs join slot 0 to slot 1 and slot 2 to slot 3, so the strand doubles back on itself, as in the first Reidemeister move.

Equations

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

@[simp]

theorem TauCeti.PDCode.kink_halfEdge : kink.halfEdge = 1

The kink numbers its half-edges by their crossing slots.

@[simp]

theorem TauCeti.PDCode.kink_crossinglessComponentCount : kink.crossinglessComponentCount = 0

The kink has no crossing-free component.

@[simp]

theorem TauCeti.PDCode.kink_overPair (i : Fin 1) : kink.overPair i = true

The over-strand of the kink is the slot pair 1-3.

theorem TauCeti.PDCode.kink_crossing (i : Fin 1) (t : Fin 4) : kink.crossing i t = (crossingSlotEquiv 1) (i, t)

The half-edge of the kink in a given crossing slot is that slot.

@[simp]

theorem TauCeti.PDCode.kink_edgePair_apply (i : Fin 1) (t : Fin 4) : ↑kink.edgePair ((crossingSlotEquiv 1) (i, t)) = (crossingSlotEquiv 1) (i, (slotSmoothing true) t)

The two arcs of the kink join each slot of the over-pair to the slot preceding it.

theorem TauCeti.OrientedPDCode.orientation_crossing_of_add_two_eq {n : ℕ} (D : OrientedPDCode n) (i : Fin n) {s t : Fin 4} (hst : s + 2 = t) : D.orientation (D.crossing i t) = !D.orientation (D.crossing i s)

The orientation reverses between two opposite slots s and t = s + 2 of a crossing.

def TauCeti.OrientedPDCode.crossingSign {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : ℤ

The sign of crossing i:1 if the crossing is right-handed and -1 if it is left-handed, as in Lickorish, Chapter 1. The slots are read counterclockwise in the oriented plane and orientation is true at the half-edges where the strands leave the crossing. The crossing is right-handed when a counterclockwise quarter turn takes the direction of the over-strand to that of the under-strand; in terms of the code, the sign is 1 exactly when overPair i records whether the orientations at slots 0 and 1 differ.

Equations

• D.crossingSign i = if (D.orientation (D.crossing i 0) ^^ D.orientation (D.crossing i 1)) = D.overPair i then 1 else -1

theorem TauCeti.OrientedPDCode.crossingSign_def {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.crossingSign i = if (D.orientation (D.crossing i 0) ^^ D.orientation (D.crossing i 1)) = D.overPair i then 1 else -1

The defining equation for an oriented crossing sign.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_eq_one_iff {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.crossingSign i = 1 ↔ (D.orientation (D.crossing i 0) ^^ D.orientation (D.crossing i 1)) = D.overPair i

A crossing is positive exactly when its orientation parity agrees with its over-strand.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_eq_neg_one_iff {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.crossingSign i = -1 ↔ (D.orientation (D.crossing i 0) ^^ D.orientation (D.crossing i 1)) ≠ D.overPair i

A crossing is negative exactly when its orientation parity disagrees with its over-strand.

theorem TauCeti.OrientedPDCode.crossingSign_eq_one_or_neg_one {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.crossingSign i = 1 ∨ D.crossingSign i = -1

Every crossing sign is either positive or negative.

def TauCeti.OrientedPDCode.writhe {n : ℕ} (D : OrientedPDCode n) : ℤ

The writhe of an oriented code is the sum of its crossing signs.

Equations

• D.writhe = ∑ i : Fin n, D.crossingSign i

theorem TauCeti.OrientedPDCode.writhe_def {n : ℕ} (D : OrientedPDCode n) : D.writhe = ∑ i : Fin n, D.crossingSign i

Expand the writhe as the sum of the crossing signs.

def TauCeti.OrientedPDCode.reverse {n : ℕ} (D : OrientedPDCode n) : OrientedPDCode n

Reverse every component orientation while preserving the underlying unoriented code.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.reverse_toPDCode {n : ℕ} (D : OrientedPDCode n) : D.reverse.toPDCode = D.toPDCode

Forgetting orientation after reversal leaves the underlying code unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_orientation {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) : D.reverse.orientation h = !D.orientation h

Reversal complements the direction at every half-edge.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_crossinglessComponents {n : ℕ} (D : OrientedPDCode n) : D.reverse.crossinglessComponents = Multiset.map (fun (x : Bool) => !x) D.crossinglessComponents

Reversal complements the orientations of all crossing-free components.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_reverse {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.reverse.crossingSign i = D.crossingSign i

Reversing every component orientation preserves each crossing sign.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_reverse {n : ℕ} (D : OrientedPDCode n) : D.reverse.reverse = D

Reversing every component orientation twice gives the original code.

def TauCeti.OrientedPDCode.mirror {n : ℕ} (D : OrientedPDCode n) : OrientedPDCode n

Reflect an oriented diagram, preserving all component orientations.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.mirror_toPDCode {n : ℕ} (D : OrientedPDCode n) : D.mirror.toPDCode = D.mirror

Forgetting orientation after reflection gives reflection of the underlying code.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_orientation {n : ℕ} (D : OrientedPDCode n) : D.mirror.orientation = D.orientation

Reflection preserves the orientation of every arc.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_crossinglessComponents {n : ℕ} (D : OrientedPDCode n) : D.mirror.crossinglessComponents = D.crossinglessComponents

Reflection preserves the oriented crossing-free components.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_mirror {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.mirror.crossingSign i = -D.crossingSign i

Reflection reverses the sign of every crossing.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_mirror {n : ℕ} (D : OrientedPDCode n) : D.mirror.mirror = D

Reflecting an oriented PD-code twice gives the original code.

def TauCeti.OrientedPDCode.relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : OrientedPDCode m

Relabel half-edges and crossings along equivalences of their finite index types.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.relabel_toPDCode {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).toPDCode = D.relabel half cross

Forgetting orientation after relabelling gives relabelling of the underlying code.

@[simp]

theorem TauCeti.OrientedPDCode.relabel_orientation {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (h : Fin (4 * m)) : (D.relabel half cross).orientation h = D.orientation (half.symm h)

Relabelling transports arc orientations along the half-edge equivalence.

@[simp]

theorem TauCeti.OrientedPDCode.relabel_crossinglessComponents {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).crossinglessComponents = D.crossinglessComponents

Relabelling leaves crossing-free oriented components unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (i : Fin m) : (D.relabel half cross).crossingSign i = D.crossingSign (cross.symm i)

The crossing sign after relabelling is read at the old crossing name.

@[simp]

theorem TauCeti.OrientedPDCode.relabel_refl {n : ℕ} (D : OrientedPDCode n) : D.relabel (Equiv.refl (Fin (4 * n))) (Equiv.refl (Fin n)) = D

Relabelling by identity equivalences does nothing.

@[simp]

theorem TauCeti.OrientedPDCode.relabel_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) {r : ℕ} (half₂ : Fin (4 * m) ≃ Fin (4 * r)) (cross₂ : Fin m ≃ Fin r) : (D.relabel half cross).relabel half₂ cross₂ = D.relabel (half.trans half₂) (cross.trans cross₂)

Consecutive relabellings compose their half-edge and crossing equivalences.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).writhe = D.writhe

Relabelling matches the crossings bijectively, so it preserves the writhe.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_mirror {n : ℕ} (D : OrientedPDCode n) : D.mirror.writhe = -D.writhe

Reflection negates the writhe.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_reverse {n : ℕ} (D : OrientedPDCode n) : D.reverse.writhe = D.writhe

Reversing every component orientation preserves the writhe.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_reverse {n : ℕ} (D : OrientedPDCode n) : D.reverse.mirror = D.mirror.reverse

Reflection and orientation reversal commute.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).mirror = D.mirror.relabel half cross

Reflection commutes with relabelling.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).reverse = D.reverse.relabel half cross

Orientation reversal commutes with relabelling.

def TauCeti.FramedOrientedPDCode.mirror {n : ℕ} (D : FramedOrientedPDCode n) : FramedOrientedPDCode n

Reflect a framed oriented diagram, negating its Seifert-relative framing coefficients.

Equations

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

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_toOrientedPDCode {n : ℕ} (D : FramedOrientedPDCode n) : D.mirror.toOrientedPDCode = D.mirror

Forgetting framing after reflection gives reflection of the underlying oriented code.

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_framing {n : ℕ} (D : FramedOrientedPDCode n) : D.mirror.framing = -D.framing

Reflection negates the Seifert-relative framing coefficient at every half-edge.

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_crossinglessFramings {n : ℕ} (D : FramedOrientedPDCode n) : D.mirror.crossinglessFramings = Multiset.map (fun (component : Bool × ℤ) => (component.1, -component.2)) D.crossinglessFramings

Reflection preserves orientation and negates framing on every crossing-free component.

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_mirror {n : ℕ} (D : FramedOrientedPDCode n) : D.mirror.mirror = D

Reflecting a framed oriented PD-code twice gives the original code.

def TauCeti.FramedOrientedPDCode.relabel {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : FramedOrientedPDCode m

Relabel half-edges and crossings along equivalences of their finite index types while transporting the framing function.

Equations

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

@[simp]

theorem TauCeti.FramedOrientedPDCode.relabel_toOrientedPDCode {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).toOrientedPDCode = D.relabel half cross

Forgetting framing after relabelling gives relabelling of the underlying oriented code.

@[simp]

theorem TauCeti.FramedOrientedPDCode.relabel_framing {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (h : Fin (4 * m)) : (D.relabel half cross).framing h = D.framing (half.symm h)

Relabelling transports framing values along the half-edge equivalence.

@[simp]

theorem TauCeti.FramedOrientedPDCode.relabel_crossinglessFramings {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).crossinglessFramings = D.crossinglessFramings

Relabelling preserves all crossing-free orientation-framing pairs.

@[simp]

theorem TauCeti.FramedOrientedPDCode.relabel_refl {n : ℕ} (D : FramedOrientedPDCode n) : D.relabel (Equiv.refl (Fin (4 * n))) (Equiv.refl (Fin n)) = D

Relabelling by identity equivalences does nothing to a framed oriented code.

@[simp]

theorem TauCeti.FramedOrientedPDCode.relabel_relabel {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) {r : ℕ} (half₂ : Fin (4 * m) ≃ Fin (4 * r)) (cross₂ : Fin m ≃ Fin r) : (D.relabel half cross).relabel half₂ cross₂ = D.relabel (half.trans half₂) (cross.trans cross₂)

Consecutive framed relabellings compose their half-edge and crossing equivalences.

def TauCeti.FramedOrientedPDCode.reverse {n : ℕ} (D : FramedOrientedPDCode n) : FramedOrientedPDCode n

Reverse every component orientation of a framed code, preserving all framing integers.

Equations

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

@[simp]

theorem TauCeti.FramedOrientedPDCode.reverse_toOrientedPDCode {n : ℕ} (D : FramedOrientedPDCode n) : D.reverse.toOrientedPDCode = D.reverse

Forgetting framing after reversal gives reversal of the underlying oriented code.

@[simp]

theorem TauCeti.FramedOrientedPDCode.reverse_framing {n : ℕ} (D : FramedOrientedPDCode n) : D.reverse.framing = D.framing

Reversal preserves the framing at every half-edge.

@[simp]

theorem TauCeti.FramedOrientedPDCode.reverse_crossinglessFramings {n : ℕ} (D : FramedOrientedPDCode n) : D.reverse.crossinglessFramings = Multiset.map (fun (component : Bool × ℤ) => (!component.1, component.2)) D.crossinglessFramings

Reversal complements only the orientation in each crossing-free framing pair.

@[simp]

theorem TauCeti.FramedOrientedPDCode.reverse_reverse {n : ℕ} (D : FramedOrientedPDCode n) : D.reverse.reverse = D

Reversing every component orientation twice gives the original framed code.

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_reverse {n : ℕ} (D : FramedOrientedPDCode n) : D.reverse.mirror = D.mirror.reverse

Reflection and orientation reversal commute.

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_relabel {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).mirror = D.mirror.relabel half cross

Reflection commutes with relabelling.

@[simp]

theorem TauCeti.FramedOrientedPDCode.reverse_relabel {n m : ℕ} (D : FramedOrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).reverse = D.reverse.relabel half cross

Orientation reversal commutes with relabelling.

def TauCeti.OrientedPDCode.unlink (orientations : Multiset Bool) : OrientedPDCode 0

A zero-crossing oriented PD-code consisting of crossing-free circles with the specified orientations. Multiplicity records distinct components without imposing an ordering on them.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_unlink (orientations : Multiset Bool) : (unlink orientations).crossinglessComponents = orientations

The unlink constructor retains exactly its component-orientation multiset.

theorem TauCeti.OrientedPDCode.eq_unlink (D : OrientedPDCode 0) : D = unlink D.crossinglessComponents

Every zero-crossing oriented PD-code is its canonical crossing-free unlink code.

def TauCeti.OrientedPDCode.unlinkEquiv : Multiset Bool ≃ OrientedPDCode 0

Multisets of orientations are equivalent to zero-crossing oriented PD-codes.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.unlinkEquiv_symm_apply (D : OrientedPDCode 0) : unlinkEquiv.symm D = D.crossinglessComponents

The inverse of unlinkEquiv reads off the orientations of the crossing-free components.

def TauCeti.OrientedPDCode.empty : OrientedPDCode 0

The empty oriented PD-code.

Equations

• TauCeti.OrientedPDCode.empty = TauCeti.OrientedPDCode.unlink 0

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_empty : empty.crossinglessComponents = 0

The empty diagram has no crossing-free components.

def TauCeti.OrientedPDCode.unknot (orientation : Bool) : OrientedPDCode 0

A crossing-free oriented unknot with the specified choice of orientation.

Equations

• TauCeti.OrientedPDCode.unknot orientation = TauCeti.OrientedPDCode.unlink {orientation}

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_unknot (orientation : Bool) : (unknot orientation).crossinglessComponents = {orientation}

The oriented unknot retains its specified component orientation.

theorem TauCeti.OrientedPDCode.unknot_ne_empty (orientation : Bool) : unknot orientation ≠ empty

A crossing-free oriented circle is distinct from the empty diagram.

theorem TauCeti.OrientedPDCode.unknot_injective : Function.Injective unknot

Distinct orientation choices give distinct crossing-free circle presentations.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_eq_self_of_zero_crossings (D : OrientedPDCode 0) : D.mirror = D

Reflection fixes every zero-crossing oriented PD-code.

def TauCeti.OrientedPDCode.positiveKink : OrientedPDCode 1

The kink TauCeti.PDCode.kink, oriented so that its crossing is positive.

This concrete code is a semantic witness that the presentation permits a genuine positive crossing, not only crossing-free links.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.toPDCode_positiveKink : positiveKink.toPDCode = PDCode.kink

The underlying PD-code of positiveKink is the kink.

@[simp]

theorem TauCeti.OrientedPDCode.orientation_positiveKink (h : Fin (4 * 1)) : positiveKink.orientation h = decide (h = 1 ∨ h = 2)

The arcs of positiveKink point away from the crossing exactly at slots 1 and 2.

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_positiveKink : positiveKink.crossinglessComponents = 0

The positive kink has no crossing-free components.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_positiveKink (i : Fin 1) : positiveKink.crossingSign i = 1

The crossing of positiveKink has positive sign.