The block splice

Partially closing an (n, n)-fragment against the block rotation on K + 2n strands splices it into the block rotation on K + n strands: the fragment is absorbed and the rotation drops one block. This is the geometric step behind the block cycle trace, and the reason a diagonal power of g closes to a power of its trace.

The proof identifies the two fragments flag by flag. It runs through the block rotation and its outer boundary permutation, the value tables of the label maps they induce, and two bridges: the reshuffled rotation as through-strands tensored with K cups, and the same after the outer relabel is collapsed.

The block rotation

noncomputable def RS.blockRot (a b : ℕ) : Equiv.Perm (Fin (a + b))

The block rotation: cyclically permute the first a and last b elements of Fin (a + b). Value: x < a ↦ b + x, x ≥ a ↦ x - a.

Equations

• RS.blockRot a b = (RS.transposeEquiv a b).trans (finCongr ⋯)

theorem RS.blockRot_val (a b : ℕ) (x : Fin (a + b)) : ↑((blockRot a b) x) = if ↑x < a then b + ↑x else ↑x - a

Forward value of blockRot.

The outer boundary permutation

def RS.blockOuterPerm (K n : ℕ) : Equiv.Perm (Fin (K + n + (K + n)))

The outer boundary permutation for the block splice: w < n ↦ (K+K+n)+w, w ≥ n ↦ w-n. At K = 0 this is the reversal (finRotate (2n)).symm.

Equations

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

The label map of the reshuffled rotation

The splice flag identification

def RS.blockSpliceFlagEquiv (K n : ℕ) : Fin (K + n + n) × Bool ≃ Fin (n + n) × Bool ⊕ Fin K × Bool

The flag identification of the block splice: wires 0..n-1 and K+n..K+2n-1 are the 2n through-strands, wires n..K+n-1 are the K cups.

Equations

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

The collapsed outer relabel and the rotated transpose

Collapsing a value-identity recast

noncomputable def RS.relabelDefeqCollapse {a : ℕ} (F : Fragment (Fin a)) (p : a = a) : (F.relabel (finCongr p)).Equiv F

Collapse a value-identity recast.

Equations

• RS.relabelDefeqCollapse F p = (RS.Fragment.Equiv.relabelEq F ⋯).trans (RS.Fragment.Equiv.relabelRefl F)

noncomputable def RS.composeRelabelCastOut {s t u u' : ℕ} (h : u = u') (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : (F.compose (G.relabel (finCongr ⋯))).Equiv ((F.compose G).relabel (finCongr ⋯))

Composition against an outer-boundary recast.

Equations

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

The bridge: the rotation as through-strands and cups

noncomputable def RS.blockBridge (K n : ℕ) : ((strandBundle (K + n + n)).relabel ((permHighEquiv (Equiv.symm (blockRot (K + n) n))).trans (pcReshuffle (K + n) (K + n) n n))).Equiv (((tensorFragment (strandBundle (n + n)) ((strandBundle K).relabel (finCongr ⋯))).relabel (finCongr ⋯)).relabel (outPermEquiv (n + n) (blockOuterPerm K n)))

The bridge: the reshuffled big block rotation, as a relabelled bundle, is the through-strands tensored with K cups, up to the outer boundary permutation.

Equations

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

The reshuffle decomposition

noncomputable def RS.blockReshuffleDecomp (K n : ℕ) : ((permFragment (Equiv.symm (blockRot (K + n) n))).relabel (pcReshuffle (K + n) (K + n) n n)).Equiv (((tensorFragment (strandBundle (n + n)) ((strandBundle K).relabel (finCongr ⋯))).relabel (finCongr ⋯)).relabel (outPermEquiv (n + n) (blockOuterPerm K n)))

The reshuffle decomposition: the reshuffled big block rotation is the through-strands tensored with K cups, up to the outer boundary permutation.

Equations

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

The final flag map and bridge

def RS.blockFinalFlagEquiv (K n : ℕ) (𝔊 : Fragment (Fin (n + n))) : 𝔊.Flag ⊕ Fin K × Bool ≃ Fin K × Bool ⊕ 𝔊.Flag

The flag map of the final comparison: the G-flags cross sides, the cups flip into through-strands.

Equations

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

noncomputable def RS.blockSpliceBridge (K n : ℕ) (𝔊 : Fragment (Fin (n + n))) : ((tensorFragment (𝔊.relabel (finCongr ⋯)) ((strandBundle K).relabel (finCongr ⋯))).relabel (((finCongr ⋯).trans (outPermEquiv 0 (blockOuterPerm K n))).trans (finCongr ⋯))).Equiv ((tensorFragment (strandBundle K) 𝔊).relabel ((transposeEquiv (K + n) (K + n)).trans (inPermEquiv (Equiv.symm (blockRot K n)).symm (K + n))))

The last comparison of the block splice: the leg-extended tensor against the rotated through-tensor.

Equations

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

The splice

noncomputable def RS.partialCloseBlockSplice (K n : ℕ) (𝔊 : Fragment (Fin (n + n))) : (partialClose 𝔊 (permFragment (Equiv.symm (blockRot (K + n) n)))).Equiv ((permFragment (Equiv.symm (blockRot K n))).compose ((tensorFragment (strandBundle K) 𝔊).relabel (transposeEquiv (K + n) (K + n))))

The block splice: partially closing an (n,n)-fragment against the block rotation on K + 2n strands splices it into the block rotation on K + n strands.

Equations

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