actBy
plain-language theorem explainer
Group action of vertex permutations on a 4-bit face configuration: pull bits through σ and repack them into Fin 16. Anyone counting D₄ orbits of ledger-closed plaquettes cites this as the concrete action. The body is a pure bit-reassembly formula with a trivial mod-16 bound.
Claim. Given a map $\sigma : \{0,1,2,3\} \to \{0,1,2,3\}$ and a face configuration $c \in \mathrm{Fin}\,16$ (four recognition bits on the vertices of a cube face), return the configuration whose bit $i$ equals the bit of $c$ at vertex $\sigma(i)$, packed as the integer $\sum_{i=0}^{3} b_{\sigma(i)}\,2^{i} \bmod 16$.
background
PixelLocal works on the forced $D=3$, eight-tick cube $2^3$: eight vertices, six faces. A boundary recognition pixel is one square face. Each of its four vertices carries one recognition bit, packed into the low four bits of a value in $\mathrm{Fin},16$ (the type FaceCfg).
Ledger closure forces even parity of those four bits; physical sectors further identify configurations that differ only by a symmetry of the square. The face stabilizer is the dihedral group $D_4$ (four rotations and four reflections), realized as a finite list of vertex permutations $\sigma : \mathrm{Fin},4 \to \mathrm{Fin},4$.
Acting by such a $\sigma$ must move bits with the vertices and leave a well-typed configuration. That is exactly what this definition supplies: read bit $\sigma(i)$ of $c$ and write it into slot $i$ of the output integer.
proof idea
Definition, not a proof. For each output slot $i\in{0,1,2,3}$, test the vertex bit of $c$ at $\sigma(i)$ and contribute weight $2^i$ if set. Sum the four contributions, reduce modulo 16, and package the result as an element of $\mathrm{Fin},16$ via the standard Nat.mod_lt witness (discharged by decide). No lemmas beyond that bound are used.
why it matters
This is the group action underlying the entire sector enumeration on one cube face. Downstream, isSectorRep declares $c$ a canonical sector representative precisely when $c \le \mathrm{actBy},\sigma,c$ for every stabilizer element $\sigma$; sectorOf folds actBy over the stabilizer and takes the numerical minimum, so sector identity is read off the edge bits alone.
The same pattern is copied for glued $2\times 1$ dominoes in PixelGluedPlaquette (six bits, Klein-four stabilizer). Together these actions make the admissible-sector count a finite, decide-able combinatorial fact. The module obtains exactly four orbits, matching the geometric coefficient $2^{D-1}=4$ in the RS pixel area $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$, on the forced eight-tick substrate (T7/T8) without continuum isotropy or Bekenstein-Hawking input. The count-to-area-coefficient link remains a separate open step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.