Mirror rotation of closures

For an (s,t)-fragment W, a (t,u)-fragment F, and an (s,u)-fragment K,

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

where Wᵀ transposes the boundary of W. This is the left-mirror variant of pairCloseComposeRotate.

The inner-pair pullback

def RS.wkPairs (s t u : ℕ) : List ((Fin (s + t) ⊕ Fin (s + u)) × (Fin (s + t) ⊕ Fin (s + u)))

The inner composition interface of the left-rotated side, pairing W-low with K-low.

Equations

• RS.wkPairs s t u = List.map (fun (j : Fin s) => (Sum.inl ⟨↑j, ⋯⟩, Sum.inr ⟨↑j, ⋯⟩)) (List.finRange s).reverse

theorem RS.wkPairs_wf (s t u : ℕ) : Fragment.PairsWF (wkPairs s t u)

wkPairs is well-formed.

theorem RS.wk_pullback (s t u : ℕ) : Fragment.mapPairs ((transposeEquiv s t).sumCongr (Equiv.refl (Fin (s + u)))).symm (interfacePairs t s u) = wkPairs s t u

The transpose-pullback of interfacePairs gives wkPairs.

The bridge equiv and ground lemma

noncomputable def RS.leftRotBridge (s t u : ℕ) : Fin (t + u) ⊕ Fin (s + t) ⊕ Fin (s + u) ≃ (Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)

The ambient bridge for the left rotation: F ⊔ (W ⊔ K) ≃ (W ⊔ F) ⊔ K.

Equations

• RS.leftRotBridge s t u = (Equiv.sumAssoc (Fin (t + u)) (Fin (s + t)) (Fin (s + u))).symm.trans ((Equiv.sumComm (Fin (t + u)) (Fin (s + t))).sumCongr (Equiv.refl (Fin (s + u))))

theorem RS.leftRot_ground (s t u : ℕ) : Fragment.mapPairs (leftRotBridge s t u).symm.symm (Fragment.inrPairs (wkPairs s t u)) = mBlock s t u

The bridge-pullback of embedded wkPairs is mBlock.

The transport composites

noncomputable def RS.leftRotM2 (s t u : ℕ) : Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (s + u)) (wkPairs s t u) ≃ Fragment.FoldSurviving (Fin (t + s) ⊕ Fin (s + u)) (interfacePairs t s u)

The inner transport: from wkPairs survivors to the boundary of the rotated composition (no swap needed).

Equations

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

noncomputable def RS.leftRotMR (s t u : ℕ) : Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) (mBlock s t u) ≃ Fragment.FoldSurviving (Fin (t + u) ⊕ Fin (s + t) ⊕ Fin (s + u)) (Fragment.inrPairs (wkPairs s t u))

The outer bridge transport: from mBlock survivors to the embedded wkPairs fold survivors.

Equations

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

noncomputable def RS.leftRotE (s t u : ℕ) : Fin (0 + (t + u)) ⊕ Fin (t + u + 0) ≃ Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) (mBlock s t u)

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

Equations

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

Lifting the closure halves

@[reducible, inline]

abbrev RS.nBlockSwap (s t u : ℕ) : List (((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)))

The nBlock.map Prod.swap block list.

Equations

• RS.nBlockSwap s t u = List.map Prod.swap (RS.nBlock s t u)

theorem RS.mem_nBlockSwap (s t u : ℕ) (q : ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u))) : q ∈ nBlockSwap s t u ↔ ∃ (j : Fin t), q = (Sum.inl (Sum.inr ⟨↑j, ⋯⟩), Sum.inl (Sum.inl ⟨s + ↑j, ⋯⟩))

Membership in nBlockSwap.

@[reducible, inline]

abbrev RS.leftRotPairsR (s t u : ℕ) : List (((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) × ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)))

The right-side block list for the left rotation.

Equations

• RS.leftRotPairsR s t u = RS.mBlock s t u ++ (RS.pBlock s t u ++ RS.nBlockSwap s t u)

theorem RS.leftRotPairsR_wf (s t u : ℕ) : Fragment.PairsWF (leftRotPairsR s t u)

Well-formedness of leftRotPairsR.

theorem RS.leftRot_pairs_lift (s t u : ℕ) : Fragment.mapPairs (leftRotE s t u) (interfacePairs 0 (t + u) 0) = Fragment.liftPairs (mBlock s t u) (pBlock s t u ++ nBlockSwap s t u) ⋯

The transported closure pairs are the lifted right-side blocks.

The Q stages

noncomputable def RS.leftRotQ1 (s t u : ℕ) : List ((Fin (t + u) ⊕ Fragment.FoldSurviving (Fin (t + s) ⊕ Fin (s + u)) (interfacePairs t s u)) × (Fin (t + u) ⊕ Fragment.FoldSurviving (Fin (t + s) ⊕ Fin (s + u)) (interfacePairs t s u)))

The right side's closure pairs, boundary stage.

Equations

• RS.leftRotQ1 s t u = RS.Fragment.mapPairs (RS.rotSigma t u s).symm (RS.interfacePairs 0 (t + u) 0)

noncomputable def RS.leftRotQ2 (s t u : ℕ) : List ((Fin (t + u) ⊕ Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (s + u)) (wkPairs s t u)) × (Fin (t + u) ⊕ Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (s + u)) (wkPairs s t u)))

The right side's closure pairs, inner stage.

Equations

• RS.leftRotQ2 s t u = RS.Fragment.mapPairs ((Equiv.refl (Fin (t + u))).sumCongr (RS.leftRotM2 s t u)).symm (RS.leftRotQ1 s t u)

noncomputable def RS.leftRotQ3 (s t u : ℕ) : List (Fragment.FoldSurviving (Fin (t + u) ⊕ Fin (s + t) ⊕ Fin (s + u)) (Fragment.inrPairs (wkPairs s t u)) × Fragment.FoldSurviving (Fin (t + u) ⊕ Fin (s + t) ⊕ Fin (s + u)) (Fragment.inrPairs (wkPairs s t u)))

The right side's closure pairs, embedded stage.

Equations

• RS.leftRotQ3 s t u = RS.Fragment.mapPairs (RS.Fragment.inrFoldEquiv (RS.wkPairs s t u)).symm (RS.leftRotQ2 s t u)

noncomputable def RS.leftRotQ4 (s t u : ℕ) : List (Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) (mBlock s t u) × Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) (mBlock s t u))

The right side's closure pairs, ambient stage.

Equations

• RS.leftRotQ4 s t u = RS.Fragment.mapPairs (RS.leftRotMR s t u).symm (RS.leftRotQ3 s t u)

theorem RS.leftRot_q4_eq (s t u : ℕ) : leftRotQ4 s t u = Fragment.liftPairs (mBlock s t u) (pBlock s t u ++ nBlockSwap s t u) ⋯

The fully transported closure pairs are the lifted right-side blocks.

The label composite

noncomputable def RS.leftRotLabelR (s t u : ℕ) : Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) (mBlock s t u ++ (pBlock s t u ++ nBlockSwap s t u)) ≃ Fin (0 + 0)

The label composite for the left-rotated right side: peels through every Q-stage and finishes at the empty surviving type.

Equations

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

The right side, normalized

noncomputable def RS.leftRotNormalRight {s t u : ℕ} (W : Fragment (Fin (s + t))) (F : Fragment (Fin (t + u))) (K : Fragment (Fin (s + u))) : Fragment.Equiv (pairClose F ((W.relabel (transposeEquiv s t)).compose K)) ((((W.disjUnion F).disjUnion K).glueList (mBlock s t u ++ (pBlock s t u ++ nBlockSwap s t u)) ⋯).relabel (leftRotLabelR s t u))

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

Equations

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

Bridge helpers

theorem RS.leftRotate_liftPairs_map_swap {α : Type} (ps qs : List (α × α)) (h : Fragment.PairsSepAll ps qs) (h' : Fragment.PairsSepAll ps (List.map Prod.swap qs)) : List.map Prod.swap (Fragment.liftPairs ps qs h) = Fragment.liftPairs ps (List.map Prod.swap qs) h'

Swapping each pair in a liftPairs list amounts to lifting the swapped suffix.

theorem RS.leftRotatePairs_perm (s t u : ℕ) : (nBlock s t u ++ (pBlock s t u ++ mBlock s t u)).Perm (mBlock s t u ++ (pBlock s t u ++ nBlock s t u))

Permutation from rotatePairsL to the intermediate form mBlock ++ (pBlock ++ nBlock).

The meet

theorem RS.leftRot_surv_empty (s t u : ℕ) (x : Fragment.FoldSurviving ((Fin (s + t) ⊕ Fin (t + u)) ⊕ Fin (s + u)) (mBlock s t u ++ (pBlock s t u ++ nBlockSwap s t u))) : False

No label survives the full left-rotation gluing.

The final theorem

theorem RS.leftRotatePairs_assoc_wf (s t u : ℕ) : Fragment.PairsWF (mBlock s t u ++ pBlock s t u ++ nBlock s t u)

The reassociated left-rotation pairs form a well-formed gluing list.

noncomputable def RS.pairCloseComposeRotateLeft {s t u : ℕ} (W : Fragment (Fin (s + t))) (F : Fragment (Fin (t + u))) (K : Fragment (Fin (s + u))) : Fragment.Equiv (pairClose (W.compose F) K) (pairClose F ((W.relabel (transposeEquiv s t)).compose K))

Mirror rotation of closures: the closure of a composite equals the closure of the second factor against the left-rotated composite.

Equations

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