recognition_sector_count
plain-language theorem explainer
On the forced D=3 cube lattice, each boundary face (square plaquette) carries exactly four recognition sectors: ledger-closed 4-bit configurations modulo the square's D₄ stabilizer. Anyone deriving the integer coefficient in a_pix = 4 · H · ℓ_P² cites this count. The proof is a pure finite enumeration discharged by decide; no continuum geometry or Bekenstein input enters.
Claim. The set of admissible boundary sectors on one cube face—ledger-closed 4-vertex bit configurations (even parity) taken up to the face stabilizer $D_4$ and counted by canonical representatives—has cardinality exactly $4$. Equivalently, $\lvert \mathrm{AdmissibleBoundarySectors}/D_4 \rvert = 4 = 2^{D-1}$ for the forced $D=3$ substrate.
background
The holography panel splits the recognition-pixel area $a_{\mathrm{pix}} = 4 \cdot H \cdot \ell_P^2$ into three separately derived quantities: the integer 4, the per-event entropy $H = (\varphi+2)\log\varphi$, and the area scale $\ell_P^2$. This module isolates the integer on the forced discrete substrate (the 8-tick cell is the cube $2^3$: eight vertices, six faces).
A boundary recognition pixel is one cube face: a square plaquette with four vertices, each carrying one recognition bit. Two structures alone define the count. Ledger closure requires the four bits to XOR to zero (even parity), so only balanced recognition loops are admissible. The face stabilizer is the dihedral group $D_4$ (four rotations and four reflections fixing the plaquette); configurations related by a square symmetry are the same physical sector.
Admissible sectors are therefore the finite filter of closed configurations that are canonical representatives under the stabilizer action. The module doc records that the four orbits are the empty loop $0000$, an adjacent-edge loop, a diagonal loop, and the full loop $1111$.
proof idea
One-line finite check: decide evaluates the cardinality of the filtered Finset of face configurations that are both ledger-closed and stabilizer representatives, and confirms it equals 4. No algebraic lemmas are invoked; the entire argument is exhaustive enumeration on a type small enough for the kernel to decide equality of natural numbers.
why it matters
This is the substrate-native realization of the geometric coefficient the paper writes as 4, forced by T8 ($D=3$) and T7 (eight-tick octave $2^3$) rather than continuum isotropy. Downstream, CoefficientBridge uses the count everywhere the pixel-to-sector ratio appears: coefficient_of_multiplicity reduces any multiplicity $m$ to $m/4$; bekenstein_branch and bekenstein_of_selector obtain the Bekenstein ratio $1/4$ when entropy attaches to closure rank; kappa_four_thirds_branch obtains $3/4$ when entropy attaches to free-bit nullity; and target_coefficient_bridge_holds packages both branches.
PixelGluedPlaquette.glued_sector_count cites it as the single-face baseline: two faces glued along an edge yield 9 sectors, not $2\cdot 4=8$, so the count is super-additive and not an extensive area density. RecordCostAsymmetry likewise feeds the same card into Bekenstein and $\kappa=4/3$ coefficient extractions from record and microstate cost.
The open gap flagged by the panel remains: many cube invariants equal 4 in $D=3$; that this sector count is the area coefficient in $a_{\mathrm{pix}}$ is a separate argument, not the enumeration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.