faceRecord
plain-language theorem explainer
The boundary record of a D=3 eight-vertex cell is the ordered 6-tuple of face-closure parities, one per cube face. Each entry is the even-parity (closed-loop) bit on the four vertices of that face. Anyone working the cell-injection or entropy-fork arguments cites this as the ledger's posted boundary data. The definition is a direct six-fold assembly of the single-face closure functional.
Claim. For a full-cell configuration $c$ (one recognition bit on each of the $8=2^3$ vertices), the boundary record is the list of six Boolean face-closure parities: for each of the six faces of the cube (two sides along each of $x,y,z$), the even-parity bit of the four vertices on that face. Explicitly, faces are the vertex quadruples with fixed axis-bit equal to the side.
background
The module runs the cell-injection test on the forced D=3 eight-tick cell: the cube $2^3$ with eight vertices and six faces. A configuration packs one recognition bit per vertex into an element of $\mathrm{Fin},256$. Vertex $v$ has coordinate bits $(v&1,,v&2,,v&4)$.
Ledger closure on a single face is the Boolean closedOn: the four vertex bits XOR to even parity (negated XOR), matching the closed-loop condition of the local pixel functional. The boundary record is exactly that functional read once on each of the six faces of one cell; the module doc states this is everything the ledger posts at the cell boundary.
The surrounding program asks whether a bulk flip necessarily changes this record. That separates two futures for recognition complementarity: unrecorded bulk degeneracy keeps complementarity axiomatic; universal posting pushes it toward a theorem.
proof idea
Pure definitional assembly, not a proof. The body lists six applications of the single-face closure functional on the standard face vertex sets: $x=0$ vertices ${0,2,4,6}$, $x=1$ ${1,3,5,7}$, $y=0$ ${0,1,4,5}$, $y=1$ ${2,3,6,7}$, $z=0$ ${0,1,2,3}$, $z=1$ ${4,5,6,7}$. Each entry is the even-parity bit of those four vertices. No lemmas or tactics are involved.
why it matters
This is the map whose injectivity properties decide the cell-injection test and feed the entropy-fork program (panel holo_bigger_discovery). Downstream results all evaluate or quantify it: the global complement is invisible; whole-face flips of weight 4 leave the record unchanged from every base; blindness is classified exactly by membership in the record kernel; any two distinct record-equal configurations differ in at least four vertices; the image has cardinality 16 and $|\mathrm{image}|\cdot|\mathrm{kernel}|=256$.
At whole-cell grain the posted rank (4 bits) and fiber nullity (4 bits) coincide. That makes the CoefficientBridge entropy fork (rank-vs-nullity mismatch per face or on glued surfaces) invisible at cell scale. The definition sits on the forced T7 eight-tick / T8 $D=3$ substrate: no extra modeling freedom beyond the cube $2^3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.