Rotation of closures

The closure of a composite equals the closure of the first factor against the rotated composite (pairCloseComposeRotate): for an (m,n)-fragment F, an (n,p)-fragment H, and an (m+p)-fragment K,

(F ∘ H) ∗ K  ≃  F ∗ (K ∘ Hᵀ),

where Hᵀ transposes the boundary of H. Both sides glue the same three interface blocks over the common ambient (F ⊔ H) ⊔ K — the n-interface between F and H, the m-block between F and K, and the p-block between H and K — so the two closures are equivalent closed fragments. This is the engine of the ideal lemma and the trace calculus (accompanying paper, Lemma 3.3(a) and Lemma 3.5(a)).

noncomputable def RS.transposeEquiv (n p : ℕ) : Fin (n + p) ≃ Fin (p + n)

The boundary transpose: exchange the two sides of an (n,p)-boundary.

Equations

• RS.transposeEquiv n p = (finSumFinEquiv.symm.trans (Equiv.sumComm (Fin n) (Fin p))).trans finSumFinEquiv

theorem RS.transposeEquiv_low (n p j : ℕ) (hj : j < n) (h1 : j < n + p) (h2 : p + j < p + n) : (transposeEquiv n p) ⟨j, h1⟩ = ⟨p + j, h2⟩

The transpose sends low labels beyond the split.

theorem RS.transposeEquiv_high (n p i : ℕ) (hi : i < p) (h1 : n + i < n + p) (h2 : i < p + n) : (transposeEquiv n p) ⟨n + i, h1⟩ = ⟨i, h2⟩

The transpose sends high labels below the split.

theorem RS.transposeEquiv_symm_low (n p l : ℕ) (hl : l < p) (h1 : l < p + n) (h2 : n + l < n + p) : (transposeEquiv n p).symm ⟨l, h1⟩ = ⟨n + l, h2⟩

The inverse transpose sends low labels beyond the split.

theorem RS.transposeEquiv_symm_high (n p j : ℕ) (hj : j < n) (h1 : p + j < p + n) (h2 : j < n + p) : (transposeEquiv n p).symm ⟨p + j, h1⟩ = ⟨j, h2⟩

The inverse transpose sends high labels below the split.

The three interface blocks over the common ambient

def RS.mBlock (m n p : ℕ) : List (((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)))

The m-block: the low labels of F against the low labels of K, top pair first.

Equations

• RS.mBlock m n p = List.map (fun (i : Fin m) => (Sum.inl (Sum.inl ⟨↑i, ⋯⟩), Sum.inr ⟨↑i, ⋯⟩)) (List.finRange m).reverse

def RS.pBlock (m n p : ℕ) : List (((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)))

The p-block: the high labels of H against the high labels of K, top pair first.

Equations

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

def RS.nBlock (m n p : ℕ) : List (((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)))

The n-block: the high labels of F against the low labels of H, top pair first — the embedded composition interface.

Equations

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

theorem RS.mem_mBlock (m n p : ℕ) (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) : q ∈ mBlock m n p ↔ ∃ (i : Fin m), q = (Sum.inl (Sum.inl ⟨↑i, ⋯⟩), Sum.inr ⟨↑i, ⋯⟩)

Membership in the m-block.

theorem RS.mem_pBlock (m n p : ℕ) (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) : q ∈ pBlock m n p ↔ ∃ (ℓ : Fin p), q = (Sum.inl (Sum.inr ⟨n + ↑ℓ, ⋯⟩), Sum.inr ⟨m + ↑ℓ, ⋯⟩)

Membership in the p-block.

theorem RS.mem_nBlock (m n p : ℕ) (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) : q ∈ nBlock m n p ↔ ∃ (j : Fin n), q = (Sum.inl (Sum.inl ⟨m + ↑j, ⋯⟩), Sum.inl (Sum.inr ⟨↑j, ⋯⟩))

Membership in the n-block.

theorem RS.mBlock_wf (m n p : ℕ) : Fragment.PairsWF (mBlock m n p)

The m-block is well-formed.

theorem RS.pBlock_wf (m n p : ℕ) : Fragment.PairsWF (pBlock m n p)

The p-block is well-formed.

theorem RS.nBlock_wf (m n p : ℕ) : Fragment.PairsWF (nBlock m n p)

The n-block is well-formed.

theorem RS.nBlock_pBlock_disjoint (m n p : ℕ) (x : (Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) : x ∈ List.flatMap (fun (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) => [q.1, q.2]) (nBlock m n p) → x ∉ List.flatMap (fun (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) => [q.1, q.2]) (pBlock m n p)

The n-block and p-block glue disjoint labels.

theorem RS.nBlock_mBlock_disjoint (m n p : ℕ) (x : (Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) : x ∈ List.flatMap (fun (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) => [q.1, q.2]) (nBlock m n p) → x ∉ List.flatMap (fun (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) => [q.1, q.2]) (mBlock m n p)

The n-block and m-block glue disjoint labels.

theorem RS.pBlock_mBlock_disjoint (m n p : ℕ) (x : (Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) : x ∈ List.flatMap (fun (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) => [q.1, q.2]) (pBlock m n p) → x ∉ List.flatMap (fun (q : ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p))) => [q.1, q.2]) (mBlock m n p)

The p-block and m-block glue disjoint labels.

theorem RS.rotatePairsL_wf (m n p : ℕ) : Fragment.PairsWF (nBlock m n p ++ (pBlock m n p ++ mBlock m n p))

The combined block list of the left association is well-formed.

theorem RS.rotatePairs_perm (m n p : ℕ) : (nBlock m n p ++ (pBlock m n p ++ mBlock m n p)).Perm (pBlock m n p ++ (nBlock m n p ++ mBlock m n p))

The middle-swap permutation between the two block orders.

theorem RS.rotatePairsR_wf (m n p : ℕ) : Fragment.PairsWF (pBlock m n p ++ (nBlock m n p ++ mBlock m n p))

The combined block list of the right association is well-formed.

Splitting closure lists

theorem RS.mapPairs_append {α β : Type} (e : α ≃ β) (ps qs : List (α × α)) : Fragment.mapPairs e (ps ++ qs) = Fragment.mapPairs e ps ++ Fragment.mapPairs e qs

mapPairs distributes over appends.

theorem RS.Fragment.PairsSepAll.append_left' {α : Type} {ps qs₁ qs₂ : List (α × α)} (h : PairsSepAll ps (qs₁ ++ qs₂)) : PairsSepAll ps qs₁

The separation of an append restricts to the left part.

theorem RS.Fragment.PairsSepAll.append_right' {α : Type} {ps qs₁ qs₂ : List (α × α)} (h : PairsSepAll ps (qs₁ ++ qs₂)) : PairsSepAll ps qs₂

The separation of an append restricts to the right part.

theorem RS.liftPairs_append {α : Type} (ps qs₁ qs₂ : List (α × α)) (h : Fragment.PairsSepAll ps (qs₁ ++ qs₂)) : Fragment.liftPairs ps (qs₁ ++ qs₂) h = Fragment.liftPairs ps qs₁ ⋯ ++ Fragment.liftPairs ps qs₂ ⋯

liftPairs distributes over appends.

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

The high half of a full-closure interface list.

Equations

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

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

The low half of a full-closure interface list.

Equations

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

theorem RS.interfacePairs_closure_split (m p : ℕ) : interfacePairs 0 (m + p) 0 = ipHigh m p ++ ipLow m p

A full-closure interface list splits into its high and low halves.

theorem RS.nBlock_eq_inlPairs (m n p : ℕ) : nBlock m n p = Fragment.inlPairs (interfacePairs m n p)

The n-block is the embedded composition interface.

Lifting the closure halves

theorem RS.lhs_close_pairs_eq (m n p : ℕ) (ps₀ : List (((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) × ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)))) (E : Fin (0 + (m + p)) ⊕ Fin (m + p + 0) ≃ Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) ps₀) (hEhi1 : ∀ ℓ < p, ∀ (h1 : m + ℓ < 0 + (m + p)) (h2 : n + ℓ < n + p), ↑(E (Sum.inl ⟨m + ℓ, h1⟩)) = Sum.inl (Sum.inr ⟨n + ℓ, h2⟩)) (hEhi2 : ∀ ℓ < p, ∀ (h1 : m + ℓ < m + p + 0) (h2 : m + ℓ < m + p), ↑(E (Sum.inr ⟨m + ℓ, h1⟩)) = Sum.inr ⟨m + ℓ, h2⟩) (hElo1 : ∀ i < m, ∀ (h1 : i < 0 + (m + p)) (h2 : i < m + n), ↑(E (Sum.inl ⟨i, h1⟩)) = Sum.inl (Sum.inl ⟨i, h2⟩)) (hElo2 : ∀ i < m, ∀ (h1 : i < m + p + 0) (h2 : i < m + p), ↑(E (Sum.inr ⟨i, h1⟩)) = Sum.inr ⟨i, h2⟩) (hsep : Fragment.PairsSepAll ps₀ (pBlock m n p ++ mBlock m n p)) : Fragment.mapPairs E (interfacePairs 0 (m + p) 0) = Fragment.liftPairs ps₀ (pBlock m n p ++ mBlock m n p) hsep

The transported closure pairs of the left side are the lifted p- and m-blocks.

The inner pairs of the right side

def RS.khPairs (m n p : ℕ) : List ((Fin (m + p) ⊕ Fin (n + p)) × (Fin (m + p) ⊕ Fin (n + p)))

The rotated composition interface over K ⊔ H, K-first.

Equations

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

def RS.hkPairs (m n p : ℕ) : List ((Fin (m + p) ⊕ Fin (n + p)) × (Fin (m + p) ⊕ Fin (n + p)))

The rotated composition interface over K ⊔ H, H-first.

Equations

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

theorem RS.hkPairs_swap (m n p : ℕ) : List.map Prod.swap (hkPairs m n p) = khPairs m n p

The two orientations are component swaps of each other.

theorem RS.hkPairs_wf (m n p : ℕ) : Fragment.PairsWF (hkPairs m n p)

The H-first pairs are well-formed.

theorem RS.kh_pullback (m n p : ℕ) : Fragment.mapPairs ((Equiv.refl (Fin (m + p))).sumCongr (transposeEquiv n p)).symm (interfacePairs m p n) = khPairs m n p

The transpose-pullback of the rotated interface is the K-first pair list.

noncomputable def RS.rotBridge (m n p : ℕ) : Fin (m + n) ⊕ Fin (m + p) ⊕ Fin (n + p) ≃ (Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)

The associativity-and-commutativity ambient bridge.

Equations

• RS.rotBridge m n p = ((Equiv.refl (Fin (m + n))).sumCongr (Equiv.sumComm (Fin (m + p)) (Fin (n + p)))).trans (Equiv.sumAssoc (Fin (m + n)) (Fin (n + p)) (Fin (m + p))).symm

theorem RS.rot_ground (m n p : ℕ) : Fragment.mapPairs (rotBridge m n p).symm.symm (Fragment.inrPairs (hkPairs m n p)) = pBlock m n p

The bridge-pullback of the embedded H-first pairs is the p-block.

The right side's transport composites

noncomputable def RS.rotM2 (m n p : ℕ) : Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (n + p)) (hkPairs m n p) ≃ Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (p + n)) (interfacePairs m p n)

The inner transport of the right side: from the H-first fold survivors to the boundary of the rotated composition.

Equations

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

noncomputable def RS.rotMR (m n p : ℕ) : Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (pBlock m n p) ≃ Fragment.FoldSurviving (Fin (m + n) ⊕ Fin (m + p) ⊕ Fin (n + p)) (Fragment.inrPairs (hkPairs m n p))

The outer bridge transport of the right side: from the p-block survivors to the embedded H-first fold survivors.

Equations

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

noncomputable def RS.rotSigma (m n p : ℕ) : Fin (m + n) ⊕ Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (p + n)) (interfacePairs m p n) ≃ Fin (0 + (m + n)) ⊕ Fin (m + n + 0)

The transported boundary equivalence of the right side.

Equations

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

noncomputable def RS.rotE (m n p : ℕ) : Fin (0 + (m + n)) ⊕ Fin (m + n + 0) ≃ Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (pBlock m n p)

The composed transport of the right side's closure pairs.

Equations

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

theorem RS.rot_pairs_lift (m n p : ℕ) : Fragment.mapPairs (rotE m n p) (interfacePairs 0 (m + n) 0) = Fragment.liftPairs (pBlock m n p) (nBlock m n p ++ mBlock m n p) ⋯

The right side's closure pairs are the lifted blocks.

noncomputable def RS.rotQ1 (m n p : ℕ) : List ((Fin (m + n) ⊕ Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (p + n)) (interfacePairs m p n)) × (Fin (m + n) ⊕ Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (p + n)) (interfacePairs m p n)))

The right side's closure pairs, boundary stage.

Equations

• RS.rotQ1 m n p = RS.Fragment.mapPairs (RS.rotSigma m n p).symm (RS.interfacePairs 0 (m + n) 0)

noncomputable def RS.rotQ2 (m n p : ℕ) : List ((Fin (m + n) ⊕ Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (n + p)) (hkPairs m n p)) × (Fin (m + n) ⊕ Fragment.FoldSurviving (Fin (m + p) ⊕ Fin (n + p)) (hkPairs m n p)))

The right side's closure pairs, inner-transport stage.

Equations

• RS.rotQ2 m n p = RS.Fragment.mapPairs ((Equiv.refl (Fin (m + n))).sumCongr (RS.rotM2 m n p)).symm (RS.rotQ1 m n p)

noncomputable def RS.rotQ3 (m n p : ℕ) : List (Fragment.FoldSurviving (Fin (m + n) ⊕ Fin (m + p) ⊕ Fin (n + p)) (Fragment.inrPairs (hkPairs m n p)) × Fragment.FoldSurviving (Fin (m + n) ⊕ Fin (m + p) ⊕ Fin (n + p)) (Fragment.inrPairs (hkPairs m n p)))

The right side's closure pairs, embedded-fold stage.

Equations

• RS.rotQ3 m n p = RS.Fragment.mapPairs (RS.Fragment.inrFoldEquiv (RS.hkPairs m n p)).symm (RS.rotQ2 m n p)

noncomputable def RS.rotQ4 (m n p : ℕ) : List (Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (pBlock m n p) × Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (pBlock m n p))

The right side's closure pairs, ambient stage.

Equations

• RS.rotQ4 m n p = RS.Fragment.mapPairs (RS.rotMR m n p).symm (RS.rotQ3 m n p)

theorem RS.rot_q4_eq (m n p : ℕ) : rotQ4 m n p = Fragment.liftPairs (pBlock m n p) (nBlock m n p ++ mBlock m n p) ⋯

The fully transported closure pairs are the lifted blocks.

The left side, normalized

theorem RS.lhsCA_wf (m n p : ℕ) : Fragment.PairsWF (Fragment.inlPairs (interfacePairs m n p) ++ (pBlock m n p ++ mBlock m n p))

The combined pair list of the left side, embedded form.

noncomputable def RS.lhsSigma (m n p : ℕ) : Fragment.FoldSurviving (Fin (m + n) ⊕ Fin (n + p)) (interfacePairs m n p) ⊕ Fin (m + p) ≃ Fin (0 + (m + p)) ⊕ Fin (m + p + 0)

The transported boundary equivalence of the left side.

Equations

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

noncomputable def RS.lhsE (m n p : ℕ) : Fin (0 + (m + p)) ⊕ Fin (m + p + 0) ≃ Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (Fragment.inlPairs (interfacePairs m n p))

The composed transport of the left side's closure pairs.

Equations

• RS.lhsE m n p = (RS.lhsSigma m n p).symm.trans (RS.Fragment.inlFoldEquiv (RS.interfacePairs m n p)).symm

theorem RS.lhs_pairs_lift (m n p : ℕ) : Fragment.mapPairs (Fragment.inlFoldEquiv (interfacePairs m n p)).symm (Fragment.mapPairs (lhsSigma m n p).symm (interfacePairs 0 (m + p) 0)) = Fragment.liftPairs (Fragment.inlPairs (interfacePairs m n p)) (pBlock m n p ++ mBlock m n p) ⋯

The left side's closure pairs are the lifted blocks.

noncomputable def RS.lhsQs1 (m n p : ℕ) : List ((Fragment.FoldSurviving (Fin (m + n) ⊕ Fin (n + p)) (interfacePairs m n p) ⊕ Fin (m + p)) × (Fragment.FoldSurviving (Fin (m + n) ⊕ Fin (n + p)) (interfacePairs m n p) ⊕ Fin (m + p)))

The left side's transported closure pairs.

Equations

• RS.lhsQs1 m n p = RS.Fragment.mapPairs (RS.lhsSigma m n p).symm (RS.interfacePairs 0 (m + p) 0)

noncomputable def RS.lhsQs2 (m n p : ℕ) : List (Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (Fragment.inlPairs (interfacePairs m n p)) × Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (Fragment.inlPairs (interfacePairs m n p)))

The left side's closure pairs in the fold survivors.

Equations

• RS.lhsQs2 m n p = RS.Fragment.mapPairs (RS.Fragment.inlFoldEquiv (RS.interfacePairs m n p)).symm (RS.lhsQs1 m n p)

noncomputable def RS.rotateLabelL (m n p : ℕ) : Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (Fragment.inlPairs (interfacePairs m n p) ++ (pBlock m n p ++ mBlock m n p)) ≃ Fin (0 + 0)

The composed label identification of the left side.

Equations

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

noncomputable def RS.rotateNormalLeft {m n p : ℕ} (F : Fragment (Fin (m + n))) (H : Fragment (Fin (n + p))) (K : Fragment (Fin (m + p))) : Fragment.Equiv (pairClose (F.compose H) K) ((((F.disjUnion H).disjUnion K).glueList (Fragment.inlPairs (interfacePairs m n p) ++ (pBlock m n p ++ mBlock m n p)) ⋯).relabel (rotateLabelL m n p))

The left side, normalized: the closure of a composite against K is iterated gluing of the three interface blocks over the common ambient.

Equations

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

The right side, normalized

noncomputable def RS.rotateLabelR (m n p : ℕ) : Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (pBlock m n p ++ (nBlock m n p ++ mBlock m n p)) ≃ Fin (0 + 0)

The composed label identification of the right side.

Equations

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

noncomputable def RS.rotateNormalRight {m n p : ℕ} (F : Fragment (Fin (m + n))) (H : Fragment (Fin (n + p))) (K : Fragment (Fin (m + p))) : Fragment.Equiv (pairClose F (K.compose (H.relabel (transposeEquiv n p)))) ((((F.disjUnion H).disjUnion K).glueList (pBlock m n p ++ (nBlock m n p ++ mBlock m n p)) ⋯).relabel (rotateLabelR m n p))

The right side, normalized: the closure of F against the rotated composite is iterated gluing of the three interface blocks over the common ambient, p-block first.

Equations

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

The meet

theorem RS.rotate_surv_empty (m n p : ℕ) (x : Fragment.FoldSurviving ((Fin (m + n) ⊕ Fin (n + p)) ⊕ Fin (m + p)) (pBlock m n p ++ (nBlock m n p ++ mBlock m n p))) : False

No label survives the full triangle gluing.

noncomputable def RS.pairCloseComposeRotate {m n p : ℕ} (F : Fragment (Fin (m + n))) (H : Fragment (Fin (n + p))) (K : Fragment (Fin (m + p))) : Fragment.Equiv (pairClose (F.compose H) K) (pairClose F (K.compose (H.relabel (transposeEquiv n p))))

Rotation of closures (accompanying paper, Lemma 3.3(a) and Lemma 3.5(a)): the closure of a composite equals the closure of the first factor against the rotated composite.

Equations

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