isSectorRep
plain-language theorem explainer
A face configuration is a canonical sector representative exactly when it is the numerically least element of its D4 orbit under the square's face stabilizer. Anyone enumerating admissible boundary sectors on the forced 8-tick cube cites this predicate as the orbit filter. The body is a direct Boolean fold: check c ≤ σ·c for every stabilizer element.
Claim. Let $c$ be a boundary plaquette configuration (one recognition bit on each of the four vertices of a cube face, packed as an element of $\mathrm{Fin}\,16$). Write $D_4$ for the face stabilizer (four rotations and four reflections fixing the plaquette) and $\sigma\cdot c$ for the action of $\sigma\in D_4$ on $c$. Then $c$ is a sector representative if and only if $c\le\sigma\cdot c$ for every $\sigma\in D_4$.
background
PixelLocal works on the forced D=3, eight-tick substrate: the cube $2^3$ with eight vertices and six faces. A boundary recognition pixel is one cube face, a square plaquette carrying four vertex bits. Configurations are elements of FaceCfg ≃ Fin 16 (the four low bits).
Two structures alone define the sector count. Ledger closure requires the four bits to XOR to zero (even parity around the plaquette). The face stabilizer $D_4$ identifies configurations that differ only by a square symmetry, so physical sectors are $D_4$-orbits of closed configurations.
This definition supplies the canonical-representative test used when those orbits are counted by picking one element per orbit: the numerically smallest configuration in the orbit.
proof idea
Pure definition, not a proof. The body folds over every element σ of the face stabilizer and asks whether c ≤ actBy σ c holds (via decide). The Boolean is true exactly when c is minimal in its D4-orbit under the numerical order on FaceCfg. Sibling definitions closed, faceStabilizer, and actBy supply the parity check, the eight-element group, and the group action respectively.
why it matters
This predicate is the orbit filter inside admissibleSectors, the Finset of ledger-closed, canonically represented face configurations. That Finset is what the module decides has cardinality exactly 4, realizing $2^{D-1}=4$ on the forced lattice and supplying the integer coefficient in the holography panel's split $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$.
Downstream, EdgeSectorBridge reuses the same minimality criterion when mapping raw edge bits to sector identity, and PixelGluedPlaquette copies the pattern for the 2×1 domino (Klein-four stabilizer, nine sectors). The definition itself does not close the open count-to-area-coefficient gap flagged in the module doc; it only makes the sector enumeration decide-able and orbit-canonical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.