xorCfg
plain-language theorem explainer
Bitwise XOR on the forced D=3 eight-vertex cell packs the group difference of two bulk bit configurations into another configuration. Anyone proving record blindness, gauge cosets, or the cell-injection dichotomy cites it as the move that takes one bulk state to another. The definition is a one-line Fin packing: XOR the underlying Nat values and reduce mod 256.
Claim. For cell configurations $c,d\in\{0,\ldots,255\}$ (one recognition bit on each of the $8=2^3$ vertices of the forced $D=3$ cube), the configuration XOR is the packed bitwise exclusive-or of their vertex bits: $\mathrm{xor}(c,d)\equiv c\oplus d\pmod{256}$, again a valid cell configuration.
background
The module studies the cell-injection test on the forced eight-tick $D=3$ cube: eight vertices, six faces, one recognition bit per vertex. A full-cell configuration is therefore an element of $\mathrm{Fin},256$, with vertex $v\in\mathrm{Fin},8$ carrying coordinate bits $(v&1,v&2,v&4)$.
The boundary record of a cell is the six face-closure parities (one per face). The entropy-fork program asks whether bulk distinctions necessarily post on that record. Moves between bulk states are differences in the abelian group $(\mathbb{Z}/2\mathbb{Z})^8$; packing that group law as bitwise XOR on the $\mathrm{Fin},256$ encoding is the natural group operation on configurations.
Downstream statements measure Hamming weight of such differences and test whether $c\mapsto$ face-record of $c\oplus d$ is constant, so the XOR packing is the ambient group law for the whole dichotomy.
proof idea
Pure definition, not a proof. Unpack the two $\mathrm{Fin},256$ values, apply Nat bitwise XOR (^^^), reduce modulo 256, and discharge the residual bound with Nat.mod_lt and decide. The result is again a CellCfg.
why it matters
This is the group law that turns bulk configurations into a translation space for the cell-injection program (T7 eight-tick octave, T8 $D=3$). Parent results use it everywhere: record_blind_only_global states that equal face records and distinct bulk states force Hamming weight of the XOR at least 4; face_flip_invisible_everywhere shows a weight-4 face flip leaves the record unchanged from every base; invisible_iff_kernel classifies moves invisible from every base as exactly the 16-element record kernel.
In RecordMonotonicity, gauge relatedness is rewritten as membership of the XOR difference in that kernel, so the entire candidate failure of complementarity is the coset structure of one finite group. The bundled target target_cell_injection packages the dichotomy that every local flip posts while global kernel moves of weight $\ge 4$ remain blind. Without this packing, none of those decide-checked statements have a uniform move language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.