The interface shift

Permuting the outgoing boundary of the left factor of a composition is the same as permuting the incoming boundary of the right factor by the inverse (interfaceShift): both sides glue F's high label s + j to G's low label σ j, merely enumerating the interface in different orders. This is the engine of the permutation calculus of §3.1: strand fragments compose by composing their permutations.

noncomputable def RS.shiftPairs (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : List ((Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u)))

The permuted interface pairs: F's high label s + j against G's low label σ j, top pair first.

Equations

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

theorem RS.shiftPairs_perm (s : ℕ) {t : ℕ} (σ τ : Equiv.Perm (Fin t)) (u : ℕ) : (List.map (fun (k : Fin t) => (Sum.inl ⟨s + ↑(τ k), ⋯⟩, Sum.inr ⟨↑(σ (τ k)), ⋯⟩)) (List.finRange t).reverse).Perm (shiftPairs s σ u)

The permuted interface pairs are a permutation of the σ-precomposed enumeration.

theorem RS.outPermEquiv_symm_high (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (k : Fin t) : (outPermEquiv s σ).symm (Fin.natAdd s k) = Fin.natAdd s ((Equiv.symm σ) k)

The inverse outgoing permutation on high labels.

theorem RS.inPermEquiv_symm_low {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) (k : Fin t) : (inPermEquiv σ u).symm (Fin.castAdd u k) = Fin.castAdd u ((Equiv.symm σ) k)

The inverse incoming permutation on low labels.

theorem RS.shift_ground_right (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : Fragment.mapPairs ((Equiv.refl (Fin (s + t))).sumCongr (inPermEquiv (Equiv.symm σ) u)).symm (interfacePairs s t u) = shiftPairs s σ u

The right ground list is the permuted interface.

theorem RS.shift_ground_left (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : Fragment.mapPairs ((outPermEquiv s σ).sumCongr (Equiv.refl (Fin (t + u)))).symm (interfacePairs s t u) = List.map (fun (k : Fin t) => (Sum.inl ⟨s + ↑((Equiv.symm σ) k), ⋯⟩, Sum.inr ⟨↑k, ⋯⟩)) (List.finRange t).reverse

The left ground list, in enumerated form.

theorem RS.shift_ground_left_perm (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : (List.map (fun (k : Fin t) => (Sum.inl ⟨s + ↑((Equiv.symm σ) k), ⋯⟩, Sum.inr ⟨↑k, ⋯⟩)) (List.finRange t).reverse).Perm (shiftPairs s σ u)

The left ground list is a permutation of the permuted interface.

theorem RS.mem_shiftPairs (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) (q : (Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u))) : q ∈ shiftPairs s σ u ↔ ∃ (k : Fin t), q = (Sum.inl ⟨s + ↑k, ⋯⟩, Sum.inr ⟨↑(σ k), ⋯⟩)

Membership in the permuted interface pairs.

theorem RS.shiftPairs_wf (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : Fragment.PairsWF (shiftPairs s σ u)

The permuted interface pairs are well-formed.

noncomputable def RS.shiftLabelL (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u)) (shiftPairs s σ u) ≃ Fin (s + u)

The composed label identification of the shifted left side.

Equations

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

noncomputable def RS.shiftLabelR (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u)) (shiftPairs s σ u) ≃ Fin (s + u)

The composed label identification of the shifted right side.

Equations

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

noncomputable def RS.shiftNormalLeft {s t u : ℕ} (σ : Equiv.Perm (Fin t)) (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : ((F.relabel (outPermEquiv s σ)).compose G).Equiv (((F.disjUnion G).glueList (shiftPairs s σ u) ⋯).relabel (shiftLabelL s σ u))

The shifted left side, normalized.

Equations

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

noncomputable def RS.shiftNormalRight {s t u : ℕ} (σ : Equiv.Perm (Fin t)) (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : (F.compose (G.relabel (inPermEquiv (Equiv.symm σ) u))).Equiv (((F.disjUnion G).glueList (shiftPairs s σ u) ⋯).relabel (shiftLabelR s σ u))

The shifted right side, normalized.

Equations

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

theorem RS.shiftLabel_meet (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : shiftLabelL s σ u = shiftLabelR s σ u

The two shifted label identifications agree: the boundary permutation only touches interface labels, which do not survive.

noncomputable def RS.interfaceShift {s t u : ℕ} (σ : Equiv.Perm (Fin t)) (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : ((F.relabel (outPermEquiv s σ)).compose G).Equiv (F.compose (G.relabel (inPermEquiv (Equiv.symm σ) u)))

The interface shift (accompanying paper §3.1): permuting the outgoing boundary of the left factor is permuting the incoming boundary of the right factor by the inverse.

Equations

• RS.interfaceShift σ F G = (RS.shiftNormalLeft σ F G).trans ((RS.Fragment.Equiv.relabelEq ((F.disjUnion G).glueList (RS.shiftPairs s σ u) ⋯) ⋯).trans (RS.shiftNormalRight σ F G).symm)