faceStabilizer
plain-language theorem explainer
Explicit list of the eight square symmetries (dihedral group D₄) as permutations of the four face vertices in cyclic order 0-1-2-3. Anyone counting recognition sectors on a cube-face plaquette cites this as the group to quotient by. The body is a closed enumeration: four rotations and four reflections, nothing derived.
Claim. The face stabilizer is the ordered list of eight maps $\mathrm{Fin}\,4\to\mathrm{Fin}\,4$ realizing $D_4$ on the square vertices $0$-$1$-$2$-$3$: the rotations $\mathrm{id}$, $(0\,1\,2\,3)$, $(0\,2)(1\,3)$, $(0\,3\,2\,1)$, and the four reflections that reverse orientation while fixing the plaquette setwise.
background
In the PixelLocal module the forced D=3, eight-tick cell is the cube $2^3$. A boundary recognition pixel is one cube face: a square plaquette with four vertices, each carrying one recognition bit. Ledger closure requires the four bits to XOR to zero (even parity). That is the only admissibility condition; it comes from the recognition ledger, not from continuum geometry.
Two closed bit patterns that differ only by a symmetry of the square are the same physical sector. The module therefore quotients by the square's symmetry group $D_4$ (order 8: four rotations and four reflections). This definition supplies that group concretely as permutations of vertex labels in cyclic order 0-1-2-3.
The surrounding construction aims at a pure combinatorial count: the number of ledger-closed face configurations modulo $D_4$. The module claims that count equals 4, matching $2^{D-1}$ on the forced lattice, without importing Bekenstein-Hawking area laws or continuum isotropy.
proof idea
Pure definitional enumeration, not a derived proof. The list hard-codes the eight elements of $D_4$ acting on $\mathrm{Fin},4$: identity and the three nontrivial cyclic shifts (rotations), then the four orientation-reversing permutations (reflections). No lemmas are applied; the value is the literal list of vector notations.
why it matters
This is the group action that turns raw face configurations into physical recognition sectors. Downstream, isSectorRep declares a configuration canonical when it is the numerically least element of its $D_4$-orbit under this list, and sectorOf folds the same list to send every configuration to that least orbit element. Together they make sector identity a total, deterministic function of the edge bits alone.
The parent goal in PixelLocal is the axiom-clean theorem that the number of admissible boundary sectors is exactly 4: the empty loop, adjacent-edge loops modulo rotation, diagonal loops, and the full loop. That integer is the substrate-native stand-in for the geometric coefficient written as 4 in $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$. The module deliberately does not prove that this sector count is the area coefficient; it only enumerates the orbits on the forced $8=2^3$ lattice (T7 eight-tick octave, T8 $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.