Exact torsion order on arbitrary theta strands

This file removes the (0,1) normalization from the exact-torsion theorem by reindexing the three strand occurrences. The reindexing is orientation preserving and fixes the two core vertices, so normalized strand coordinates and the ordered pair of marks are preserved.

def Bananas.thetaNormalizeSlots (alpha beta : Fin 3) : Equiv.Perm (Fin 3)

A permutation sending two distinct indices to 0 and 1.

Equations

• Bananas.thetaNormalizeSlots alpha beta = Equiv.trans (Equiv.swap alpha 0) (Equiv.swap ((Equiv.swap alpha 0) beta) 1)

theorem Bananas.thetaNormalizeSlots_apply_left (alpha beta : Fin 3) (h : alpha ≠ beta) : (thetaNormalizeSlots alpha beta) alpha = 0

theorem Bananas.thetaNormalizeSlots_apply_right (alpha beta : Fin 3) : (thetaNormalizeSlots alpha beta) beta = 1

def Bananas.thetaNormalizedBanana (B : Banana 2) (alpha beta : Fin 3) : Banana 2

The same banana presentation with its strand occurrences normalized so that alpha and beta become slots 0 and 1.

Equations

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

def Bananas.thetaNormalizationRelabeling (B : Banana 2) (alpha beta : Fin 3) : Utilities.Certificate.SubdivisionGraph.Spec.Relabeling B (thetaNormalizedBanana B alpha beta)

The relabeling identifying a theta banana with the normalization of its two chosen strands.

Equations

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

theorem Bananas.thetaNormalization_length (B : Banana 2) (alpha beta gamma : Fin 3) : (thetaNormalizedBanana B alpha beta).length ((thetaNormalizeSlots alpha beta) gamma) = B.length gamma

theorem Bananas.thetaNormalization_position_val (B : Banana 2) (alpha beta gamma : Fin 3) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) : ↑((Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv B (thetaNormalizedBanana B alpha beta) (thetaNormalizationRelabeling B alpha beta) gamma) p) = ↑p

theorem Bananas.thetaNormalization_strandVertex (B : Banana 2) (alpha beta gamma : Fin 3) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B gamma) : (Utilities.Certificate.SubdivisionGraph.Spec.vertexEquiv B (thetaNormalizedBanana B alpha beta) (thetaNormalizationRelabeling B alpha beta)) (strandVertex B gamma p) = strandVertex (thetaNormalizedBanana B alpha beta) ((thetaNormalizeSlots alpha beta) gamma) ((Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv B (thetaNormalizedBanana B alpha beta) (thetaNormalizationRelabeling B alpha beta) gamma) p)

theorem Bananas.pathPosition_slot_cast_val (B : Banana 2) {alpha beta : Fin 3} (h : alpha = beta) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : ↑(h ▸ p) = ↑p

Transporting a path position along equality of strand slots does not change its numerical coordinate.

theorem Bananas.strandVertex_slot_cast (B : Banana 2) {alpha beta : Fin 3} (h : alpha = beta) (p : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : strandVertex B alpha p = strandVertex B beta (h ▸ p)

strandVertex respects dependent transport along equality of strand slots.

theorem Bananas.evenlyMarkedTheta_isTorsionOrder_relabel (B : Banana 2) (alpha beta : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hEven : EvenlyMarkedTheta B alpha beta i j) : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) (B.length alpha / (B.length alpha).gcd ↑i)

Lemma 4.15 without a normalization of the two distinct theta strands.