complement_invisible
plain-language theorem explainer
Flipping every vertex bit of the D=3 eight-tick cell leaves the six face-closure parities unchanged: the global complement and the empty cell post the same boundary record. Holography and entropy-fork arguments cite this as the simplest bulk degeneracy that the ledger does not see. The proof is a pure `decide` check on the finite configuration space.
Claim. Let the empty cell be the all-zero assignment on the eight cube vertices, and let the global complement be the assignment with every vertex bit flipped. Then the six face-closure parities of the complement equal those of the empty cell: each face has four vertices, so an even number of flips leaves every face parity unchanged.
background
The module runs the cell-injection test on the forced D=3 eight-tick cube: eight vertices, six faces, one recognition bit per vertex (CellCfg ranges over 256 states). The boundary record is the list of six face-closure parities (faceRecord), each the XOR/parity of the four vertices on that face (closedOn). That is everything ledger closure posts at the cell boundary.
Two distinguished states appear here: the empty cell (all bits off) and the global complement (all eight bits on). The module asks whether bulk distinctions necessarily change the posted record. Single-vertex flips do post, but larger coordinated flips need not.
The parity reason is elementary: each face meets four vertices. Flipping all eight vertices flips exactly four bits on every face, an even count, so every face parity is invariant.
proof idea
One-line decidability proof: both sides are concrete finite objects (cell0, cellComplement, and the six Boolean face parities), so Lean closes the equality by decide with no lemmas. The mathematical content is the even-cardinality observation already in the doc-comment; the machine check simply evaluates the six parities on both configurations.
why it matters
This is the seed counterexample for non-injectivity of the cell boundary record. Downstream, record_not_injective applies it directly: if faceRecord were injective it would separate the complement from the empty cell, contradicting this equality. That feeds the module's sharp dichotomy: every single bulk flip posts (single_flip_posts), yet the record map still has a rank-4 kernel of 16 invisible moves (whole-face flips, inscribed tetrahedra, and the global complement).
In the entropy-fork program this shows that bulk degeneracy can be unrecorded at whole-cell granularity unless record-equal states are physically identified. It sits inside the forced T7/T8 substrate (eight-tick octave, D=3 cube) with no extra modeling freedom. Complementarity therefore remains closer to an axiom than a theorem until identification of the kernel is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.