admissibleSectors_eq
plain-language theorem explainer
On a D=3 cube-face plaquette the admissible recognition sectors are exactly the four orbit minima {0000, 0011, 0101, 1111}. Anyone citing the forced sector count 4 = 2^(D-1) needs this explicit identification of the representatives. The proof is a one-line finite decision of Finset equality after the parity-and-stabilizer filter.
Claim. The set of admissible boundary sectors equals $\{0, 3, 5, 15\} \subseteq \mathrm{Fin}\,16$, i.e. the four bit patterns $0000$, $0011$, $0101$, and $1111$ (empty loop, an adjacent-edge loop, a diagonal loop, and the full loop).
background
PixelLocal works on the forced 8-tick cell in spatial dimension $D=3$: the cube $2^3$ with 8 vertices and 6 faces. A boundary recognition pixel is one cube face (a square plaquette). A face configuration packs one recognition bit on each of the four vertices into the low four bits of $\mathrm{Fin},16$.
Two structures alone define admissibility. Ledger closure requires a balanced (zero-sum) recognition loop, so the four vertex bits XOR to zero (even parity). The face stabilizer is the dihedral group $D_4$ of the square (four rotations and four reflections); configurations related by a square symmetry are the same physical sector, so one keeps orbit minima only.
The module isolates the integer coefficient in the recognition-pixel area formula $a_{\mathrm{pix}} = 4 \cdot H \cdot \ell_P^2$ as pure plaquette combinatorics on the forced lattice, without continuum isotropy or Bekenstein–Hawking input. Upstream, $D=3$ is the spatial dimension forced by the T8 step of the forcing chain.
proof idea
The statement is a concrete Finset equality on a finite type. After admissibleSectors is defined as the orbit-minima filter of even-parity face configurations, Lean closes the equality to ${0,3,5,15}$ by decide: exhaustive evaluation of the finite predicate. No algebraic lemmas are invoked beyond the decidable instances on Fin and Finset.
why it matters
This pins the four sectors that realize $2^{D-1}=2^2=4$ on the forced $D=3$, eight-tick ($2^3$) substrate, matching the geometric coefficient the holography panel writes as the integer 4 in $a_{\mathrm{pix}}$. It is the substrate-native enumeration behind T7 (eight-tick octave) and T8 ($D=3$), not an imported continuum count.
Downstream, EightTickSubperiodExclusion.hits uses the four orbits (empty ${0}$, adjacent-edge ${3,6,12,9}$, diagonal ${5,10}$, full) for census completeness of walks on the plaquette. PixelGluedPlaquette.admissibleSectors_eq is the parallel explicit listing for the glued-domino configuration space.
The module doc is explicit about the remaining gap: equating this sector count with the area coefficient in $a_{\mathrm{pix}}=c\cdot H\cdot\ell_P^2$ is a separate argument; many cube invariants equal 4 in $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.