Preparations for the bundle closure

Three ingredients for identifying the strand-bundle closure with the straight-matching self-glue: the straight matching is well-formed and leaves no survivors (generically, for any m); the strand bundle is invariant under transposing its two boundary blocks; and the interface pairs of a full closure split into the high-block pairs followed by the low-block pairs.

The straight matching, generically

theorem RS.matchPairs_flat (m : ℕ) : List.flatMap (fun (p : Fin (m + m) × Fin (m + m)) => [p.1, p.2]) (matchPairs m) = List.flatMap (fun (j : Fin m) => [Fin.castAdd m j, Fin.natAdd m j]) (List.finRange m)

The straight matching's flags, listed.

theorem RS.mem_matchPairs_flat (m : ℕ) (z : Fin (m + m)) : z ∈ List.flatMap (fun (p : Fin (m + m) × Fin (m + m)) => [p.1, p.2]) (matchPairs m)

It uses every label: the matching is perfect.

theorem RS.matchPairs_wf (m : ℕ) : Fragment.PairsWF (matchPairs m)

It is a well-formed gluing list.

theorem RS.matchPairs_surv_isEmpty (m : ℕ) : IsEmpty (Fragment.FoldSurviving (Fin (m + m)) (matchPairs m))

And leaves no survivor, so gluing it closes the fragment.

Block-swap invariance of the strand bundle

noncomputable def RS.strandBundleTranspose (m : ℕ) : ((strandBundle m).relabel (transposeEquiv m m)).Equiv (strandBundle m)

Transposing the two boundary blocks of the strand bundle returns the strand bundle: each strand just swaps its two ends.

Equations

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

The interface split of a full closure

def RS.highCross (m : ℕ) : List ((Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) × (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)))

The high-block interface pairs of a full (m + m)-closure.

Equations

• RS.highCross m = List.map (fun (k : Fin m) => (Sum.inl ⟨m + ↑k, ⋯⟩, Sum.inr ⟨m + ↑k, ⋯⟩)) (List.finRange m).reverse

def RS.lowCross (m : ℕ) : List ((Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) × (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)))

The low-block interface pairs of a full (m + m)-closure.

Equations

• RS.lowCross m = List.map (fun (k : Fin m) => (Sum.inl ⟨↑k, ⋯⟩, Sum.inr ⟨↑k, ⋯⟩)) (List.finRange m).reverse

theorem RS.interfacePairs_split (m : ℕ) : interfacePairs 0 (m + m) 0 = highCross m ++ lowCross m

A full closure's interface pairs split into the high block followed by the low block.