The interface pair list of a composition

The pairs glued by glueInterface, top pair first, as data for the iterated-gluing fold: their well-formedness, the membership characterization of the glued labels, and the identification of the surviving labels with Fin s ⊕ Fin u. The normalization of glueInterface as a glueList builds on these.

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

The interface pairs glued by glueInterface, top pair first.

Equations

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

theorem RS.mem_interfacePairs_flat (s t u : ℕ) (x : Fin (s + t) ⊕ Fin (t + u)) : x ∈ List.flatMap (fun (p : (Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u))) => [p.1, p.2]) (interfacePairs s t u) ↔ (∃ (a : Fin (s + t)), x = Sum.inl a ∧ s ≤ ↑a) ∨ ∃ (b : Fin (t + u)), x = Sum.inr b ∧ ↑b < t

Membership in the flattened interface pairs.

theorem RS.interfacePairs_wf (s t u : ℕ) : Fragment.PairsWF (interfacePairs s t u)

The interface pairs are well-formed.

def RS.finLtEquiv (s t : ℕ) : { a : Fin (s + t) // ↑a < s } ≃ Fin s

Left labels below the interface.

Equations

• RS.finLtEquiv s t = { toFun := fun (a : { a : Fin (s + t) // ↑a < s }) => ⟨↑↑a, ⋯⟩, invFun := fun (a : Fin s) => ⟨⟨↑a, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def RS.finGeEquiv (t u : ℕ) : { b : Fin (t + u) // ¬↑b < t } ≃ Fin u

Right labels beyond the interface.

Equations

• RS.finGeEquiv t u = { toFun := fun (b : { b : Fin (t + u) // ¬↑b < t }) => ⟨↑↑b - t, ⋯⟩, invFun := fun (b : Fin u) => ⟨⟨t + ↑b, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def RS.interfaceSurvPred (s t u : ℕ) : Fin (s + t) ⊕ Fin (t + u) → Prop

The survival predicate of the interface gluing.

Equations

• RS.interfaceSurvPred s t u = Sum.elim (fun (a : Fin (s + t)) => ↑a < s) fun (b : Fin (t + u)) => ¬↑b < t

theorem RS.forall_ne_iff_not_mem_flat {α : Type} (ps : List (α × α)) (x : α) : (∀ p ∈ ps, x ≠ p.1 ∧ x ≠ p.2) ↔ x ∉ List.flatMap (fun (p : α × α) => [p.1, p.2]) ps

Avoiding every pair component is avoiding the flat list.

theorem RS.interfaceSurv_iff (s t u : ℕ) (x : Fin (s + t) ⊕ Fin (t + u)) : x ∉ List.flatMap (fun (p : (Fin (s + t) ⊕ Fin (t + u)) × (Fin (s + t) ⊕ Fin (t + u))) => [p.1, p.2]) (interfacePairs s t u) ↔ interfaceSurvPred s t u x

Survival equals the survival predicate.

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

The labels surviving the interface gluing: left labels below s and right labels beyond t.

Equations

• RS.interfaceSurvEquiv s t u = ((Equiv.subtypeEquivRight ⋯).trans Equiv.subtypeSum).trans ((RS.finLtEquiv s t).sumCongr (RS.finGeEquiv t u))

The step decomposition of the interface pairs

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

The tail pairs of the (t+1)-interface: the same pairs one level down, embedded in the larger index types.

Equations

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

theorem RS.interfacePairs_succ (s t u : ℕ) : interfacePairs s (t + 1) u = (Sum.inl ⟨s + t, ⋯⟩, Sum.inr ⟨t, ⋯⟩) :: tailPairs s t u

The (t+1)-interface pairs decompose as the top pair followed by the tail pairs.

theorem RS.interfaceStepEquiv_inl (s t u : ℕ) (a : Fin (s + t + 1)) (h : Sum.inl a ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ Sum.inl a ≠ Sum.inr ⟨t, ⋯⟩) (ha : ↑a < s + t) : (interfaceStepEquiv s t u) ⟨Sum.inl a, h⟩ = Sum.inl ⟨↑a, ha⟩

The step re-indexing on surviving left labels: values are preserved.

theorem RS.interfaceStepEquiv_inr_below (s t u : ℕ) (b : Fin (t + 1 + u)) (h : Sum.inr b ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ Sum.inr b ≠ Sum.inr ⟨t, ⋯⟩) (hb : ↑b < t) : (interfaceStepEquiv s t u) ⟨Sum.inr b, h⟩ = Sum.inr ⟨↑b, ⋯⟩

The step re-indexing on surviving right labels below the glued index: values are preserved.

theorem RS.interfaceStepEquiv_inr_above (s t u : ℕ) (b : Fin (t + 1 + u)) (h : Sum.inr b ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ Sum.inr b ≠ Sum.inr ⟨t, ⋯⟩) (hb : t < ↑b) : (interfaceStepEquiv s t u) ⟨Sum.inr b, h⟩ = Sum.inr ⟨↑b - 1, ⋯⟩

The step re-indexing on surviving right labels above the glued index: values drop by one.

The coerced tail as a mapped pair list

theorem RS.interfaceStepEquiv_symm_inl (s t u k : ℕ) (hk : k < t) : (interfaceStepEquiv s t u).symm (Sum.inl ⟨s + k, ⋯⟩) = ⟨Sum.inl ⟨s + k, ⋯⟩, ⋯⟩

The step re-indexing pulls tail-pair left components back to themselves.

theorem RS.interfaceStepEquiv_symm_inr (s t u k : ℕ) (hk : k < t) : (interfaceStepEquiv s t u).symm (Sum.inr ⟨k, ⋯⟩) = ⟨Sum.inr ⟨k, ⋯⟩, ⋯⟩

The step re-indexing pulls tail-pair right components back to themselves.

theorem RS.mapPairs_symm_cancel {α β : Type} (e : α ≃ β) (ps : List (β × β)) : Fragment.mapPairs e (Fragment.mapPairs e.symm ps) = ps

Mapping back and forth through an equivalence is the identity on pair lists.

theorem RS.interface_coerce_eq (s t u : ℕ) (hsep : Fragment.PairsSep (Sum.inl ⟨s + t, ⋯⟩) (Sum.inr ⟨t, ⋯⟩) (tailPairs s t u)) : Fragment.mapPairs (interfaceStepEquiv s t u).symm (interfacePairs s t u) = Fragment.coercePairsList (Sum.inl ⟨s + t, ⋯⟩) (Sum.inr ⟨t, ⋯⟩) (tailPairs s t u) hsep

The mapped-back interface pairs are the coerced tail pairs.

theorem RS.interfaceSurvEquiv_inl (s t u : ℕ) (x : Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u)) (interfacePairs s t u)) (a : Fin (s + t)) (hx : ↑x = Sum.inl a) (ha : ↑a < s) : (interfaceSurvEquiv s t u) x = Sum.inl ⟨↑a, ha⟩

The surviving-label identification on left labels.

theorem RS.interfaceSurvEquiv_inr (s t u : ℕ) (x : Fragment.FoldSurviving (Fin (s + t) ⊕ Fin (t + u)) (interfacePairs s t u)) (b : Fin (t + u)) (hx : ↑x = Sum.inr b) (hb : t ≤ ↑b) : (interfaceSurvEquiv s t u) x = Sum.inr ⟨↑b - t, ⋯⟩

The surviving-label identification on right labels.

The normalization of glueInterface

noncomputable def RS.glueInterfaceNormal (s u t : ℕ) (W : Fragment (Fin (s + t) ⊕ Fin (t + u))) : (glueInterface s t u W).Equiv ((W.glueList (interfacePairs s t u) ⋯).relabel (interfaceSurvEquiv s t u))

glueInterface is the iterated gluing along the interface pairs, relabelled by the surviving-label identification.

Equations

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

noncomputable def RS.composeNormal {s t u : ℕ} (F : Fragment (Fin (s + t))) (G : Fragment (Fin (t + u))) : (F.compose G).Equiv (((F.disjUnion G).glueList (interfacePairs s t u) ⋯).relabel ((interfaceSurvEquiv s t u).trans finSumFinEquiv))

Composition as a fold: composing two fragments is the iterated gluing of the interface pairs in their disjoint union, relabelled by the surviving-label identification.

Equations

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

Boundary permutations across an interface

def RS.outPermEquiv (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) : Fin (s + t) ≃ Fin (s + t)

Permuting the last t labels of Fin (s + t).

Equations

• RS.outPermEquiv s σ = finSumFinEquiv.symm.trans (((Equiv.refl (Fin s)).sumCongr σ).trans finSumFinEquiv)

def RS.inPermEquiv {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) : Fin (t + u) ≃ Fin (t + u)

Permuting the first t labels of Fin (t + u).

Equations

• RS.inPermEquiv σ u = finSumFinEquiv.symm.trans ((Equiv.sumCongr σ (Equiv.refl (Fin u))).trans finSumFinEquiv)

theorem RS.outPermEquiv_low (s : ℕ) {t : ℕ} (σ : Equiv.Perm (Fin t)) (a : Fin s) : (outPermEquiv s σ) (Fin.castAdd t a) = Fin.castAdd t a

The outgoing permutation fixes the low labels.

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

The outgoing permutation acts on the high labels.

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

The incoming permutation acts on the low labels.

theorem RS.inPermEquiv_high {t : ℕ} (σ : Equiv.Perm (Fin t)) (u : ℕ) (b : Fin u) : (inPermEquiv σ u) (Fin.natAdd t b) = Fin.natAdd t b

The incoming permutation fixes the high labels.