FaceCfg
plain-language theorem explainer
A face configuration is an element of a 16-element set: four recognition bits, one per vertex of a cube face, packed as the low nibble. Anyone counting admissible boundary sectors or applying ledger closure on the forced 8-tick cube cites this type. It is a pure type abbreviation with no proof content.
Claim. A boundary plaquette configuration is an element of $\{0,\ldots,15\}$, encoding one recognition bit on each of the four vertices of a cube face (the four low bits of a 4-bit word).
background
The PixelLocal module isolates the integer coefficient in the recognition-pixel area $a_{\mathrm{pix}} = 4 \cdot H \cdot \ell_P^2$ on the forced discrete substrate: the $D=3$ eight-tick cell is the cube $2^3$ (8 vertices, 6 faces). A boundary recognition pixel is one square face of that cube.
Each of the four face vertices carries one recognition bit. The full configuration space of those bits is therefore $2^4 = 16$ states. This abbreviation names that finite type; ledger closure (even parity of the four bits) and the face stabilizer $D_4$ act on it later in the module.
Upstream geometry supplies periodic cubic vertices and Boolean-to-nat bit packing used elsewhere on the lattice; the face maps from singular simplices are only incidental name collisions and do not enter the definition.
proof idea
No proof: a one-line type abbreviation equating the face-configuration type with $\mathrm{Fin},16$. The packing convention (four low bits = four vertex bits) is fixed by the doc-comment and by the sibling extractor that reads bit $i\in\mathrm{Fin},4$.
why it matters
This is the raw domain for the entire holography coefficient bridge. Downstream, rawBits is $\log_2|\mathrm{FaceCfg}|=4$; closed filters the even-parity kernel; rank-nullity on that map yields $|\mathrm{image}|\cdot|\mathrm{kernel}|=16$ and pins closureRank=1, freeBits=3. Edge-sector work uses the same type for closed configs before the $D_4$ quotient.
In the RS panel split of $a_{\mathrm{pix}}$, the integer 4 is meant to arise as the count of admissible boundary sectors after ledger closure and face-stabilizer quotient on this configuration space (realized as $2^{D-1}=4$ on the forced lattice). The type itself carries none of $H$ or $\ell_P$; it only supplies the finite set those enumerations run over. T7 (eight-tick octave) and T8 ($D=3$) fix why the plaquette has four vertices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.