The bundle closure is the straight-matching self-glue

The full closure of an (m + m)-fragment against the strand bundle is the self-glue of its straight matching i ↔ m + i. The proof fuses and splits folds using only established machinery: the closure's interface fold splits into the high-block glues followed by the low-block glues (interfacePairs_split and glueListAppend); the high-block stage is itself a composition against the transposed bundle (composeNormal read backwards), which the right identity law collapses to the fragment; and the lifted low-block pairs are then exactly the straight matching.

Flat membership of the two blocks

theorem RS.mem_highCross_flat (m : ℕ) (z : Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) : z ∈ List.flatMap (fun (p : (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) × (Fin (0 + (m + m)) ⊕ Fin (m + m + 0))) => [p.1, p.2]) (highCross m) ↔ (∃ (a : Fin (0 + (m + m))), z = Sum.inl a ∧ m ≤ ↑a) ∨ ∃ (b : Fin (m + m + 0)), z = Sum.inr b ∧ m ≤ ↑b

The high block's flags are exactly the labels at or above m on either side.

theorem RS.highCross_wf (m : ℕ) : Fragment.PairsWF (highCross m)

The high block is a well-formed gluing list.

theorem RS.splitCross_wf (m : ℕ) : Fragment.PairsWF (highCross m ++ lowCross m)

And so is the whole closure list, high block then low.

The surviving labels of the high-block stage

noncomputable def RS.bcPhiFun (m : ℕ) (x : Fin (m + m)) : Fragment.FoldSurviving (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) (highCross m)

The forward survivor map: low labels to the surviving left slots, high labels to the surviving right slots.

Equations

• RS.bcPhiFun m x = if h : ↑x < m then ⟨Sum.inl ⟨↑x, ⋯⟩, ⋯⟩ else ⟨Sum.inr ⟨↑x - m, ⋯⟩, ⋯⟩

noncomputable def RS.bcPhiInv (m : ℕ) (s : Fragment.FoldSurviving (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) (highCross m)) : Fin (m + m)

The inverse survivor map.

Equations

• RS.bcPhiInv m s = match hs : ↑s with | Sum.inl a => ⟨↑a, ⋯⟩ | Sum.inr b => ⟨m + ↑b, ⋯⟩

noncomputable def RS.bcPhi (m : ℕ) : Fin (m + m) ≃ Fragment.FoldSurviving (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) (highCross m)

The survivor identification of the high-block stage.

Equations

• RS.bcPhi m = { toFun := RS.bcPhiFun m, invFun := RS.bcPhiInv m, left_inv := ⋯, right_inv := ⋯ }

The ambient relabelling

noncomputable def RS.bcDelta (m : ℕ) : Fin (m + m) ⊕ Fin (m + m) ≃ Fin (0 + (m + m)) ⊕ Fin (m + m + 0)

From the (m,m,m)-interface ambient to the full-closure ambient: a cast on the left factor, the block transpose threaded through a cast on the right.

Equations

• RS.bcDelta m = (finCongr ⋯).sumCongr ((RS.transposeEquiv m m).symm.trans (finCongr ⋯))

theorem RS.mapPairs_bcDelta (m : ℕ) : Fragment.mapPairs (bcDelta m) (interfacePairs m m m) = highCross m

The mapped (m,m,m)-interface pairs are the high-block pairs.

The high-block stage collapses to the fragment

noncomputable def RS.bcAmbient (m : ℕ) (V : Fragment (Fin (m + m))) : Fragment (Fin (0 + (m + m)) ⊕ Fin (m + m + 0))

The full-closure ambient.

Equations

• RS.bcAmbient m V = (V.relabel (finCongr ⋯)).disjUnion ((RS.strandBundle m).relabel (finCongr ⋯))

noncomputable def RS.bcAmbient2 (m : ℕ) (V : Fragment (Fin (m + m))) : Fragment (Fin (m + m) ⊕ Fin (m + m))

The (m,m,m)-interface ambient: the fragment against the transposed bundle.

Equations

• RS.bcAmbient2 m V = V.disjUnion ((RS.strandBundle m).relabel (RS.transposeEquiv m m))

noncomputable def RS.bcAmbientEquiv (m : ℕ) (V : Fragment (Fin (m + m))) : (bcAmbient m V).Equiv ((bcAmbient2 m V).relabel (bcDelta m))

The two ambients agree through the ambient relabelling.

Equations

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

theorem RS.bcPhi_eq (m : ℕ) : (((interfaceSurvEquiv m m m).trans finSumFinEquiv).symm.trans (Fragment.foldSurvivingMapEquiv (bcDelta m) (interfacePairs m m m))).trans (Fragment.foldSurvivingPermEquiv ⋯) = bcPhi m

The assembled survivor identification equals the direct one.

noncomputable def RS.bcStageA (m : ℕ) (V : Fragment (Fin (m + m))) : ((bcAmbient m V).glueList (highCross m) ⋯).Equiv (V.relabel (bcPhi m))

The high-block stage: gluing the high-block pairs in the closure ambient is the identity composition against the bundle, hence the fragment itself.

Equations

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

The lifted low-block pairs are the straight matching

theorem RS.liftPairs_length {α : Type} (ps qs : List (α × α)) (h : Fragment.PairsSepAll ps qs) : (Fragment.liftPairs ps qs h).length = qs.length

Lifting a pair list past an earlier fold keeps its length.

theorem RS.liftPairs_getElem_val {α : Type} (ps qs : List (α × α)) (h : Fragment.PairsSepAll ps qs) (j : ℕ) (hj : j < (Fragment.liftPairs ps qs h).length) (hj' : j < qs.length) : ↑(Fragment.liftPairs ps qs h)[j].1 = qs[j].1 ∧ ↑(Fragment.liftPairs ps qs h)[j].2 = qs[j].2

And keeps each pair's underlying labels.

theorem RS.bcPhi_symm_val_inl (m : ℕ) (s : Fragment.FoldSurviving (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) (highCross m)) (a : Fin (0 + (m + m))) (hs : ↑s = Sum.inl a) : (bcPhi m).symm s = ⟨↑a, ⋯⟩

The inverse survivor identification on left values.

theorem RS.bcPhi_symm_val_inr (m : ℕ) (s : Fragment.FoldSurviving (Fin (0 + (m + m)) ⊕ Fin (m + m + 0)) (highCross m)) (b : Fin (m + m + 0)) (hs : ↑s = Sum.inr b) (hb : ↑b < m) : (bcPhi m).symm s = ⟨m + ↑b, ⋯⟩

The inverse survivor identification on right values.

theorem RS.mapPairs_bcPhi_lift (m : ℕ) : Fragment.mapPairs (bcPhi m).symm (Fragment.liftPairs (highCross m) (lowCross m) ⋯) = (matchPairs m).reverse

Read through the high stage's survivor identification, the lifted low block is the straight matching reversed.

theorem RS.lift_eq_mapPairs (m : ℕ) : Fragment.liftPairs (highCross m) (lowCross m) ⋯ = Fragment.mapPairs (bcPhi m) (matchPairs m).reverse

Equivalently, the lifted low block is the transported straight matching — the identification the closure theorem runs on.

noncomputable def RS.pairCloseStrandBundle (m : ℕ) (V : Fragment (Fin (m + m))) : Fragment.Equiv (pairClose V (strandBundle m)) ((V.glueList (matchPairs m) ⋯).relabel (Equiv.equivOfIsEmpty (Fragment.FoldSurviving (Fin (m + m)) (matchPairs m)) (Fin 0)))

The bundle closure is the straight-matching self-glue: the full closure of an (m + m)-fragment against the strand bundle is the self-glue of its straight matching.

Equations

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