closedOn
plain-language theorem explainer
Face-closure on a D=3 cell is the even-parity (XOR-zero) condition on four designated vertices. It is the local closed-loop bit the ledger posts per cube face. Holography and cell-injection arguments cite it as the atomic boundary observable. The body is a one-line Boolean: negate the four-bit XOR of the vertex recognition bits.
Claim. Let $c$ be a cell configuration (one recognition bit on each of the eight vertices of the cube $2^3$). For vertex indices $i,j,k,l \in \{0,\ldots,7\}$, the face is closed on $c$ if and only if the XOR of the four vertex bits is zero: $\neg\bigl(b_i(c)\oplus b_j(c)\oplus b_k(c)\oplus b_l(c)\bigr)$.
background
The module studies the cell-injection test on the forced D=3 eight-tick cell (the cube $2^3$: eight vertices, six faces). A cell 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 closed-loop condition: the four vertices of that face must have even parity. This definition is exactly that predicate, written as the negation of the four-bit XOR (matching the per-face closed functional used elsewhere in the pixel-local layer).
The six faces of the cube are the natural boundary observables. Each face is specified by an axis and a side, and collects the four vertices whose axis-bit equals that side. The present predicate is the atomic check applied to any such four-tuple.
proof idea
Pure definition, not a proof. Read the four vertex bits of $c$ at indices $i,j,k,l$, XOR them, and return the Boolean negation. True means even parity (closed loop); false means odd parity (open).
why it matters
This is the atomic boundary observable for the cell-injection / entropy-fork program. Downstream, the six-face boundary record is assembled by evaluating it on the six standard face vertex-quadruples (the two sides of each of the three axes). That record is everything the ledger posts at the cell boundary.
The larger test asks whether a bulk flip necessarily changes the boundary record. The module's machine-checked dichotomy (every single-vertex flip posts on the three incident faces; yet the full record map has a rank-4 kernel of whole-face moves) is built on this predicate. Framework landmarks: T7 eight-tick octave and T8 $D=3$ force the cube substrate; the definition carries no new modeling freedom.
It does not itself settle complementarity. It only supplies the local closed-loop bit whose global assembly feeds the injectivity and kernel analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.