admissibleSectors
plain-language theorem explainer
Defines the finite set of admissible boundary recognition sectors on one cube face: ledger-closed 4-bit plaquette configurations that are canonical under the square stabilizer D₄. Anyone citing the forced sector count 4 = 2^(D-1), or the Bekenstein/κ=4/3 coefficient branches, depends on this set. The body is a plain Finset filter of the universe of FaceCfg by closure and representative predicates.
Claim. Let a face configuration be a 4-bit assignment on the vertices of one cube face (an element of $\mathrm{Fin}\,16$). The admissible boundary sectors are the finite set of all such configurations that are ledger-closed (even parity on the four vertices) and are the chosen canonical representative of their orbit under the face stabilizer $D_4$.
background
PixelLocal isolates the integer coefficient in the recognition-pixel area $a_{\mathrm{pix}} = 4 \cdot H \cdot \ell_P^2$ on the forced $D=3$, $8=2^3$ cube substrate. A boundary recognition pixel is one square face: four vertices, one recognition bit each, packed as a face configuration in $\mathrm{Fin},16$.
Two structures alone define admissibility. Ledger closure requires the four vertex bits to XOR to zero (balanced plaquette loop). The face stabilizer $D_4$ (four rotations and four reflections fixing the square) identifies configurations that differ only by square symmetry; sectors are counted by canonical representatives of those orbits.
Spatial dimension $D=3$ is the T8/T9-forced value used throughout the chain. No cost functional $H$, Planck area, or continuum isotropy enters the definition: pure plaquette combinatorics on the forced lattice.
proof idea
Definition, not a proof. The set is Finset.univ on face configurations, filtered by the conjunction of the ledger-closure predicate and the sector-representative predicate. Downstream cardinality theorems (recognition_sector_count, sector_count_eq_two_pow) then evaluate the filtered set by decide and obtain card $= 4 = 2^{D-1}$.
why it matters
This set is the substrate-native carrier of the geometric coefficient written as 4 in the holography panel. CoefficientBridge uses its cardinality in coefficient_of_multiplicity, bekenstein_branch (ratio $1/4$ when multiplicity is closure rank), kappa_four_thirds_branch (ratio $3/4$ when multiplicity is free-bit nullity), and the selector-conditioned Bekenstein theorem. EdgeSectorBridgeCert requires every closed configuration to map into this set, surjectivity of the sector map onto it, and the exact 2-to-1 lossy quotient card(admissibleSectors) * 2 = card(closedConfigs).
It realizes $2^{D-1}$ on the T7 eight-tick / T8 $D=3$ lattice without importing Bekenstein–Hawking input. The open Gap 1 remains: linking this sector count to the area coefficient in $a_{\mathrm{pix}}$ is a separate physical selector, not discharged by the enumeration alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.