dominoLeftClosed
plain-language theorem explainer
Boolean left-face closure flag on a two-face domino configuration: true exactly when the four vertex bits on the cycle 0-1-4-3 have even parity. Anyone computing the local closure map, domino rank, or nullity in the recognition-multiplicity ledger cites it. The body is a one-line XOR-then-negate on those four bits.
Claim. Given a two-face domino configuration $c$, the left-face closure bit is $\mathsf{true}$ if and only if $v_0(c)\oplus v_1(c)\oplus v_4(c)\oplus v_3(c)=0$ (even parity on the face cycle $0$-$1$-$4$-$3$).
background
This module treats recognition multiplicity as a rank-consistency check on a T-1 ledger: one posted distinction per unit face, with cost read from the free ledger floor. The module header stresses that the ledger shape is a modeling choice, not a derivation of the Bekenstein 1/4 selector; what is proved is that the rank reading and the nullity reading are mutually exclusive on glued cells.
A DominoCfg is the bit assignment on the two-face (pixel-glued) domino from the plaquette layer. The helper vbit reads the Boolean at a numbered vertex of that configuration. The left face is the 4-cycle of vertices $0,1,4,3$; closure means even parity of those four bits, i.e. the face is a closed recognition loop in the discrete sense used throughout the holography stack.
The companion right-face flag uses the cycle $1$-$2$-$5$-$4$. Together the two flags are the local closure map whose image cardinality supplies the domino rank.
proof idea
Pure definition, not a proof. Evaluate the four vertex bits of $c$ at indices $0,1,4,3$, take their Boolean XOR, and negate: the flag is true exactly on even parity. No lemmas are applied.
why it matters
Feeds dominoLocalMap, which pairs left and right face-closure flags. Downstream, that map's image is all of $\mathsf{Bool}\times\mathsf{Bool}$, so the domino rank is $2$ and the nullity is $4$; those identities underwrite the multiplicity-versus-rank comparison on the glued cell.
In the broader Recognition story this sits inside the holography rank-consistency check (T-1 ledger floor, one generator per face). It does not itself force the Bekenstein selector: the module audit retagged that claim as a modeling choice, with the live candidate forcing deferred to gluing extensivity in the quad-plaquette development. The definition is the concrete left-face coordinate of that check on the minimal two-face glue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.