Partial closure as a composition

The partial closure is a composition in disguise: reshuffle the test fragment's boundary so that the z-blocks form the incoming interface and the x-blocks the outgoing free side (pcReshuffle), and gluing z into G is composing z (as a (0, u+v)-fragment) with the reshuffled G. This lets the entire compose-calculus (identity laws, free-side relabels, permutation absorption) act on partial closures.

noncomputable def RS.pcReshuffle (s t u v : ℕ) : Fin (s + u + (t + v)) ≃ Fin (u + v + (s + t))

The reshuffle of the test boundary: z-blocks first (the interface), x-blocks last (the free side).

Equations

• RS.pcReshuffle s t u v = (RS.interleaveEquiv s t u v).symm.trans ((Equiv.sumComm (Fin (s + t)) (Fin (u + v))).trans finSumFinEquiv)

theorem RS.pcReshuffle_zlow (s t u v : ℕ) (j : Fin u) : (pcReshuffle s t u v) (Fin.castAdd (t + v) (Fin.natAdd s j)) = Fin.castAdd (s + t) (Fin.castAdd v j)

The reshuffle on the low z-block.

theorem RS.pcReshuffle_zhigh (s t u v : ℕ) (l : Fin v) : (pcReshuffle s t u v) (Fin.natAdd (s + u) (Fin.natAdd t l)) = Fin.castAdd (s + t) (Fin.natAdd u l)

The reshuffle on the high z-block.

theorem RS.pcReshuffle_xlow (s t u v : ℕ) (i : Fin s) : (pcReshuffle s t u v) (Fin.castAdd (t + v) (Fin.castAdd u i)) = Fin.natAdd (u + v) (Fin.castAdd t i)

The reshuffle on the low x-block.

theorem RS.pcReshuffle_xhigh (s t u v : ℕ) (k : Fin t) : (pcReshuffle s t u v) (Fin.natAdd (s + u) (Fin.castAdd v k)) = Fin.natAdd (u + v) (Fin.natAdd s k)

The reshuffle on the high x-block.

theorem RS.pcReshuffle_symm_low (s t u v : ℕ) (j : Fin u) : (pcReshuffle s t u v).symm (Fin.castAdd (s + t) (Fin.castAdd v j)) = Fin.castAdd (t + v) (Fin.natAdd s j)

The inverse reshuffle on the low interface.

theorem RS.pcReshuffle_symm_high (s t u v : ℕ) (l : Fin v) : (pcReshuffle s t u v).symm (Fin.castAdd (s + t) (Fin.natAdd u l)) = Fin.natAdd (s + u) (Fin.natAdd t l)

The inverse reshuffle on the high interface.

The peeled ground pairs are the z-gluing pairs

theorem RS.interfacePairs_zsplit (s t u v : ℕ) : interfacePairs 0 (u + v) (s + t) = List.map (fun (l : Fin v) => (Sum.inl ⟨u + ↑l, ⋯⟩, Sum.inr ⟨u + ↑l, ⋯⟩)) (List.finRange v).reverse ++ List.map (fun (j : Fin u) => (Sum.inl ⟨↑j, ⋯⟩, Sum.inr ⟨↑j, ⋯⟩)) (List.finRange u).reverse

The full-interface split of the composition pairs at (0, u + v, s + t).

theorem RS.pc_compose_ground (s t u v : ℕ) : Fragment.mapPairs ((finCongr ⋯).sumCongr (pcReshuffle s t u v)).symm (interfacePairs 0 (u + v) (s + t)) = zClosePairs s t u v

The peeled composition pairs of the reshuffled test fragment are the z-gluing pairs.

The label meet

noncomputable def RS.pcComposeQs (s t u v : ℕ) : List ((Fin (u + v) ⊕ Fin (s + u + (t + v))) × (Fin (u + v) ⊕ Fin (s + u + (t + v))))

The peeled composition pairs.

Equations

• RS.pcComposeQs s t u v = RS.Fragment.mapPairs ((finCongr ⋯).sumCongr (RS.pcReshuffle s t u v)).symm (RS.interfacePairs 0 (u + v) (s + t))

theorem RS.pc_compose_meet (s t u v : ℕ) : (Fragment.foldSurvivingPermEquiv ⋯).symm.trans ((Fragment.foldSurvivingMapEquiv ((finCongr ⋯).sumCongr (pcReshuffle s t u v)) (pcComposeQs s t u v)).trans ((Fragment.foldSurvivingPermEquiv ⋯).symm.trans (((interfaceSurvEquiv 0 (u + v) (s + t)).trans finSumFinEquiv).trans (finCongr ⋯)))) = pcSurvEquiv s t u v

The composed label of the compose-side normalization is the partial-closure survivor identification.

noncomputable def RS.partialCloseEqCompose {s t u v : ℕ} (z : Fragment (Fin (u + v))) (G : Fragment (Fin (s + u + (t + v)))) : (partialClose z G).Equiv (((z.relabel (finCongr ⋯)).compose (G.relabel (pcReshuffle s t u v))).relabel (finCongr ⋯))

Partial closure as a composition: gluing z into G is composing z with the reshuffled G.

Equations

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