gauge_iff_kernel
plain-language theorem explainer
Two bulk cell configurations are gauge-related (identical boundary face records) exactly when their XOR difference lies in the 16-element record kernel. Anyone working the entropy-fork / weak-complementarity argument on the forced D=3 cell cites this coset identification. The proof rewrites kernel membership and hands off to the fully decided pairwise form.
Claim. For cell configurations $c,c'\in\{0,\ldots,255\}$ (one recognition bit on each of the $2^3$ vertices), $\mathrm{faceRecord}(c)=\mathrm{faceRecord}(c')$ if and only if the bitwise XOR $c\oplus c'$ lies in the record kernel: the finite set of configurations whose six-face boundary record equals that of the empty cell.
background
Module RecordMonotonicity is step 3 of the entropy-fork chain: derive weak complementarity (injection of physical bulk states into boundary letter space) on the forced D=3 cell from record accounting, rather than assuming monolithic complementarity. A cell configuration is an 8-bit packing Fin 256; faces post a six-channel boundary record.
Gauge relation means two bulk states carry the same face record: an unposted difference is not a performed distinction. The record kernel is the Finset of configurations sharing the empty cell's boundary record (the record-invisible states). XOR of two configurations is the move taking one to the other.
Upstream, gauge_iff_kernel_record already states the same biconditional in predicate form (faceRecord(xor) = faceRecord(empty)) and discharges it by exhaustive decide over all 65 536 pairs. Kernel membership is the Finset packaging of that same predicate.
proof idea
Term-mode, two steps. Rewrite membership in the record-kernel Finset via mem_recordKernel_iff, which unpacks c ∈ recordKernel into the face-record predicate against the empty cell. The goal is then exactly the statement of gauge_iff_kernel_record, applied at the pair (c, c'). No new search or case split: the heavy lifting is the upstream decide proof.
why it matters
This is item 2 of the module's four-part argument: gauge classes are exactly the cosets of one named 16-element finite group (the record kernel isolated by the cell-injection test). The entire candidate failure set of complementarity collapses to those global parity moves.
Downstream, gaugeSetoid builds the setoid of bulk configurations modulo gauge, and the physical-state quotient is defined as configurations modulo that kernel. The certificate theorem target_record_monotonicity_holds packages this biconditional together with books-balance, no-protocol-separates, and weak complementarity as the module's verify-target.
Framework landmark: forced D=3 cell (T8) with eight vertices (T7 eight-tick octave structure). Replaces the holography manuscript's strongest premise with a finite, explicitly classified coset structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.