A trefoil PD-code and its Kauffman bracket

This file gives the standard oriented PD-code of the right-handed trefoil. All three crossings are positive, and traversing the arc matching reads the alternating Gauss word

O0, U1, O2, U0, O1, U2.

The writhe-normalized Kauffman bracket of this diagram is then evaluated directly from its eight states. The result fixes the Jones-polynomial convention: after the substitution t = A⁻⁴, the value is t + t³ - t⁴.

Main definitions

• TauCeti.rightHandedTrefoilArcPair: the six arcs in crossing-slot coordinates.
• TauCeti.rightHandedTrefoilPDCode: the standard three-crossing oriented PD-code.

Main results

• TauCeti.rightHandedTrefoilPDCode_writhe: the diagram has writhe three.
• TauCeti.rightHandedTrefoilPDCode_componentCount: the diagram is a knot.
• TauCeti.normalizedKauffmanBracket_rightHandedTrefoilPDCode: its normalized bracket is A⁻⁴ + A⁻¹² - A⁻¹⁶.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3.
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395–407.

def TauCeti.rightHandedTrefoilArcPair : PerfectMatching (Fin 3 × Fin 4)

The six arcs of the standard trefoil diagram, expressed directly on crossing-slot pairs.

Equations

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

@[simp]

theorem TauCeti.rightHandedTrefoilArcPair_pairs : ↑rightHandedTrefoilArcPair (0, 2) = (1, 1) ∧ ↑rightHandedTrefoilArcPair (1, 1) = (0, 2) ∧ ↑rightHandedTrefoilArcPair (1, 3) = (2, 0) ∧ ↑rightHandedTrefoilArcPair (2, 0) = (1, 3) ∧ ↑rightHandedTrefoilArcPair (2, 2) = (0, 1) ∧ ↑rightHandedTrefoilArcPair (0, 1) = (2, 2) ∧ ↑rightHandedTrefoilArcPair (0, 3) = (1, 0) ∧ ↑rightHandedTrefoilArcPair (1, 0) = (0, 3) ∧ ↑rightHandedTrefoilArcPair (1, 2) = (2, 1) ∧ ↑rightHandedTrefoilArcPair (2, 1) = (1, 2) ∧ ↑rightHandedTrefoilArcPair (2, 3) = (0, 0) ∧ ↑rightHandedTrefoilArcPair (0, 0) = (2, 3)

The six arcs paired by rightHandedTrefoilArcPair, stated in both directions so that the partner of each of the twelve crossing slots is available to simp.

def TauCeti.rightHandedTrefoilPDCode : OrientedPDCode 3

The standard three-crossing oriented PD-code of the right-handed trefoil. Crossing slots are numbered consecutively, slots zero and two form the over-strand, and slots two and three point out of each crossing. The arc matching gives the alternating Gauss word O0, U1, O2, U0, O1, U2.

Equations

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

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_halfEdge : rightHandedTrefoilPDCode.halfEdge = 1

The trefoil code numbers half-edges consecutively by their crossing slots.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_crossinglessComponentCount : rightHandedTrefoilPDCode.crossinglessComponentCount = 0

The trefoil code has no crossing-free component.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_overPair (i : Fin 3) : rightHandedTrefoilPDCode.overPair i = false

Slots zero and two form the over-strand at each crossing of the trefoil code.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_edgePair_apply (i : Fin 3) (slot : Fin 4) : ↑rightHandedTrefoilPDCode.edgePair ((PDCode.crossingSlotEquiv 3) (i, slot)) = (PDCode.crossingSlotEquiv 3) (↑rightHandedTrefoilArcPair (i, slot))

The arc partner of a crossing slot is the partner prescribed by rightHandedTrefoilArcPair.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_orientation_crossing (i : Fin 3) (slot : Fin 4) : rightHandedTrefoilPDCode.orientation ((PDCode.crossingSlotEquiv 3) (i, slot)) = decide (2 ≤ ↑slot)

At every crossing, slots zero and one point into the crossing while slots two and three point out of it.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_crossingSign (i : Fin 3) : rightHandedTrefoilPDCode.crossingSign i = 1

Every crossing of the right-handed trefoil PD-code is positive.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_writhe : rightHandedTrefoilPDCode.writhe = 3

The standard right-handed trefoil diagram has writhe three.

@[simp]

theorem TauCeti.rightHandedTrefoilPDCode_componentCount : rightHandedTrefoilPDCode.componentCount = 1

The standard trefoil PD-code represents one link component.

@[simp]

theorem TauCeti.kauffmanBracket_rightHandedTrefoilPDCode {R : Type u_1} [CommRing R] (a : Rˣ) : rightHandedTrefoilPDCode.kauffmanBracket a = -↑a ^ 5 - ↑a⁻¹ ^ 3 + ↑a⁻¹ ^ 7

The Kauffman bracket of the standard right-handed trefoil is -A⁵ - A⁻³ + A⁻⁷.

@[simp]

theorem TauCeti.normalizedKauffmanBracket_rightHandedTrefoilPDCode {R : Type u_1} [CommRing R] (a : Rˣ) : rightHandedTrefoilPDCode.normalizedKauffmanBracket a = ↑a⁻¹ ^ 4 + ↑a⁻¹ ^ 12 - ↑a⁻¹ ^ 16

The writhe-normalized Kauffman bracket of the right-handed trefoil is A⁻⁴ + A⁻¹² - A⁻¹⁶. With t = A⁻⁴, this is t + t³ - t⁴.