invisible_iff_kernel
plain-language theorem explainer
A bulk move on the D=3 eight-vertex cell is invisible from every base configuration exactly when it lies in the record kernel. Anyone citing the cell-injection dichotomy or the silent-move classification needs this biconditional. The proof is a pure finite decision over Fin 256.
Claim. For every cell configuration $d \in \{0,\ldots,255\}$ (one bit per vertex of the forced $2^3$ cube), the following are equivalent: (i) for every base configuration $c$, the six face-closure parities of $c \oplus d$ equal those of $c$; (ii) $d$ belongs to the record kernel (the 16-element blind subgroup of unrecorded bulk moves).
background
The module runs the cell-injection test: flip interior bits of the forced D=3 eight-tick cell and ask whether the boundary record must change. A cell configuration is one recognition bit on each of the eight vertices of the cube $2^3$, packed as an element of $\mathrm{Fin},256$. The boundary record is the six face-closure parities (one per face), exactly the per-face closed functional read on all six faces.
Bulk moves act by bitwise XOR of configurations. The record kernel is the set of moves that leave every face record unchanged; the module already shows it is a rank-4 subgroup of order 16, generated by whole-face flips (including the global complement and the two inscribed tetrahedra). The local theoretical setting is the entropy-fork program: if bulk degeneracy can go unrecorded, complementarity stays axiomatic; if every bulk distinction posts, it moves toward a theorem.
Upstream scaffolding is purely finite combinatorics on the cube (face records, XOR action, kernel membership). No continuous geometry or Clifford data is required for this classification.
proof idea
One-line finite decision: decide. Both sides of the biconditional are decidable propositions over the finite type CellCfg = Fin 256. Lean enumerates all $d$ and, for each $d$, checks the universal quantification over base configurations against membership in the precomputed record kernel. No algebraic lemmas are invoked; the equivalence is machine-checked exhaustively.
why it matters
This is the exact classification of blindness for the cell-injection test: shift-invariance of the face record is equivalent to kernel membership, so the 16 kernel elements are the complete list of unrecorded bulk moves. Downstream, silent_iff_kernel in RecordMonotonicity is a one-line re-export of this statement under the silent-move vocabulary.
In the broader Recognition framework it pins the second arm of the module's dichotomy (every single-vertex flip posts, yet the record map is non-injective with a 16-element blind group). Blindness is only global: minimum invisible weight is 4, half the cell. That feeds the rank-nullity identity $|\mathrm{image}|\cdot|\mathrm{kernel}|=256$ and separates whole-cell coincidence of posted bits and free bits from the per-face entropy fork. The result sits on the forced T7 eight-tick octave and T8 $D=3$ cube; it does not invent new modeling freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.