Definition. Framed transports [frap-000Q]
Definition. Framed transports [frap-000Q]
Let \(I\) be a finite set of positions, \(\Omega \) a nonempty set, and \(K\) a group acting faithfully on \(\Omega \). At each position \(i\), choose a set \(X_i\) of local labels and a bijective local frame \(c_i:\Omega \to X_i\). Keep the fibers distinct by using the tagged union
\[E=\coprod _{i\in I}X_i=\{(i,y):i\in I,\ y\in X_i\}.\]A framed transport is a permutation of \(E\) given by a position permutation \(\pi \in \operatorname {Sym}(I)\) and elements \(a_i\in K\), with
\[g(i,c_i(x))=(\pi (i),c_{\pi (i)}(a_i x)).\]Write \(g=(\pi ,a)\). Its local factors are indexed by the source position. Nonempty fibers determine \(\pi \) uniquely, and faithfulness determines each \(a_i\) uniquely. Conversely every such pair gives a permutation: in framed coordinates its inverse sends \((j,x)\) to \((\pi ^{-1}(j),a_{\pi ^{-1}(j)}^{-1}x)\).
This finite-position model isolates the coordinate mechanism of [marchetti2025rubik, Section 3.1, Definition 7 and equation (5)]. Which local label sets and local group describe a particular puzzle must still be justified for that puzzle. The requirement that a transport moves whole fibers is part of the model.
Under composition these transports form a wreath product
\(K\wr \operatorname {Sym}(I)\). The normal subgroup \(K^I\) acts within
fibers, and position permutations reorder its factors. In
TauCeti.WreathProduct, a pair is stored using the
destination-indexed function \(A_j=a_{\pi ^{-1}(j)}\). Its permutation
action is TauCeti.WreathProduct.imprimitiveToPerm_apply;
the nonempty-fiber and faithful-action hypotheses give its injectivity in
TauCeti.WreathProduct.imprimitiveToPerm_injective.
The bijections \(c_i\) identify that action on \(I\times \Omega \) with
the action on \(E\) above.