Lemma. Composition of framed transports [frap-000R]
✍️source
mul_left
L∃∀N

    Let \(I\) be finite and let \(K\) act faithfully on a nonempty \(\Omega \), with bijective frames \(c_i:\Omega \to X_i\). Write two framed transports as \(g=(\pi ,a)\) and \(h=(\sigma ,b)\), acting in coordinates by \(g(i,x)=(\pi (i),a_i x)\) and \(h(i,x)=(\sigma (i),b_i x)\). With left actions, applying \(g\) and then \(h\) gives the composition law

    \[hg=(\sigma \pi ,(b_{\pi (i)}a_i)_{i\in I}).\]

    Proof. 

      The intermediate coordinates are \((\pi (i),a_i x)\). Applying \(h\) evaluates its local map at that intermediate position, giving \((\sigma \pi (i),b_{\pi (i)}a_i x)\). Thus a local factor must be multiplied at its transported position index.

      The vertical arrows are the chosen frames; the bottom arrows are the restrictions of the actual transports. Each square commutes. Along the top row, the second factor is evaluated at \(\pi (i)\), explaining the shifted index in the composite. This expands the wreath-product coordinates of [marchetti2025rubik, Section 3.1, pp. 6--7]. The wreath product uses destination-indexed factors in the linked formalization.

      The linked multiplication theorem uses destination-indexed factors. Set \(A_j=a_{\pi ^{-1}(j)}\) and \(B_j=b_{\sigma ^{-1}(j)}\). Its factor for \(hg\) at destination \(j\) is

      \[B_j A_{\sigma ^{-1}(j)} =b_{\sigma ^{-1}(j)}a_{\pi ^{-1}\sigma ^{-1}(j)}.\]

      Putting \(i=(\sigma \pi )^{-1}(j)\) makes this exactly \(b_{\pi (i)}a_i\). Thus the theorem and the displayed source-indexed law use the same multiplication order.