vbit
plain-language theorem explainer
Extracts the i-th vertex recognition bit from a square-plaquette face configuration packed as four low bits of a Fin 16 value. Anyone working the PixelLocal sector count, ledger-closure parity, or D₄ orbit enumeration cites this accessor. The body is a one-line Nat.testBit unpack of the packed integer.
Claim. Let $c$ be a boundary plaquette configuration (four recognition bits on the vertices of a cube face, packed into $\{0,\ldots,15\}$). For each vertex index $i\in\{0,1,2,3\}$, the $i$-th vertex bit of $c$ is the $i$-th binary digit of the integer value of $c$.
background
PixelLocal works on the forced D=3, eight-tick substrate: the cube $2^3$ has eight vertices and six faces. A boundary recognition pixel is one cube face, a square plaquette with four vertices. Configurations place one recognition bit on each vertex and pack those four bits into the low nibble of a Fin 16 value (the face configuration type).
The module's only admissibility condition is ledger closure: a closed recognition loop posts a balanced zero-sum ledger around the face, so the four vertex bits XOR to even parity. Configurations that differ by a symmetry of the square are identified via the face stabilizer $D_4$. The bit accessor is the primitive that both the parity check and the stabilizer action read.
Upstream ledger language (balanced ledgers, double-entry event lists) supplies the physical meaning of even parity; the bit packing itself is pure discrete combinatorics on the forced lattice, with no continuum or Bekenstein–Hawking input.
proof idea
Definitional one-liner. The face configuration is a Fin 16 whose underlying natural number holds the four vertex bits in positions 0–3. The bit at index $i$ is read by Nat.testBit on that value at bit position $i$. No lemmas are applied.
why it matters
This is the shared vertex-bit primitive for the whole holography panel that isolates the integer 4 in $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$. Downstream, local ledger closure is the even parity of the four bits; the face stabilizer action rebuilds configurations by permuting those bits; the admissible-sector count then quotients closed configs by $D_4$ and obtains exactly four orbits ($2^{D-1}=4$ on the forced lattice).
CellInjection lifts the same idea to the full cube (eight vertex bits, six face-closure parities). PixelGluedPlaquette reuses the pattern on a two-face domino. The definition itself carries no physics claim; it is the substrate-native bit read that makes the pure plaquette enumeration (T7 eight-tick / T8 $D=3$) decideable. The open gap remains the separate count-to-area-coefficient link, not this accessor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.