gauge_iff_kernel_record
plain-language theorem explainer
Two bulk cell configurations are gauge-related exactly when the boundary face-record of their XOR difference equals the empty-cell record. Anyone citing the gauge-class = kernel-coset identification uses this form. The proof is a single `decide` over all 65 536 configuration pairs on the forced D=3 cell.
Claim. For every pair of cell configurations $c,c'$, one has $\mathrm{gaugeRel}(c,c')$ if and only if the six-face boundary record of the bitwise XOR $c\oplus c'$ equals the boundary record of the empty cell.
background
This sits in step 3 of the entropy-fork holography chain (RecordMonotonicity): derive weak complementarity on the forced D=3 cell from record accounting rather than from a monolithic complementarity premise. Bulk states are CellCfg (8 vertex bits). The empty cell is the zero configuration. Boundary data are the six face-channel records; faceRecord posts those channels. Two configs are gauge-related when they induce the same boundary record.
The XOR difference $c\oplus c'$ is the natural group operation on the finite configuration space. The empty-cell face record is the neutral boundary value, so the predicate "face record of the difference equals the empty record" is the kernel form of gauge equivalence. Upstream, CellInjection isolates the 16-element record kernel and the empty cell; the books-balance and no-free-erasure theorems already show that posted record weight cannot be silently destroyed.
proof idea
One-line decidability proof: decide. Both sides of the biconditional are Boolean predicates on a finite type (CellCfg has $2^8=256$ inhabitants, so $256^2=65536$ pairs). Lean’s kernel decides the universal quantification by exhaustive evaluation. No algebraic lemmas are invoked; the check is the proof.
why it matters
This is the kernel-predicate form of the module’s second main theorem: gauge classes are exactly the cosets of the 16-element record kernel. The immediate parent gauge_iff_kernel rewrites membership in recordKernel via mem_recordKernel_iff and applies this result, so the entire candidate failure of complementarity collapses to one named finite group of global parity moves.
That classification feeds the later no-protocol-separates / gauge-never-separated block: record-compatible dynamics cannot split a gauge pair. In the holography manuscript this replaces the strongest complementarity premise by two weaker, falsifiable inputs (ledger balance and the finite kernel). It is local to the forced D=3 cell (T8) and the eight-tick posting geometry, not a continuum AdS/CFT statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.