gaugeRel
plain-language theorem explainer
Two bulk cell configurations are gauge-related when they post the same six face-closure parities. Entropy-fork and weak-complementarity arguments cite this as the candidate physical-identity relation: an unposted bulk difference is not a performed distinction. The body is plain equality of boundary records, with decidability inherited from list equality.
Claim. Two cell configurations $c,c'$ (each a recognition-bit assignment on the eight vertices of the forced $D=3$ cube) are gauge-related when their boundary records agree: the six face-closure parities of $c$ equal those of $c'$.
background
This module is step 3 of the entropy-fork chain on the forced $D=3$ cell. It aims to replace monolithic recognition complementarity by weak complementarity: an injection from physical bulk states into boundary letter space, derived from record accounting plus two weaker inputs.
A cell configuration is one bit on each of the $8=2^3$ vertices, packed as an element of $\mathrm{Fin},256$. The boundary record of a configuration is the list of six face-closure parities (one per cube face), each parity the XOR of the four vertices on that face. That list is everything the ledger posts at the cell boundary.
The gauge relation is the equality relation on those posted records. Configurations that differ only by bulk data invisible to the six face channels are treated as candidates for physical identity under the fork selector.
proof idea
Definitional: the relation is literally equality of the two face-record lists. The accompanying DecidableRel instance is a one-line inheritance of decidability of list equality on Bool, so every later decide proof over pairs can treat gauge membership as a computable predicate.
why it matters
This is the primitive relation for the gauge half of the holography argument. Downstream, it is proved equivalent to membership of the XOR-difference in the 16-element record kernel (gauge_iff_kernel, via the exhaustive gauge_iff_kernel_record), shown to be an equivalence (gaugeRel_equivalence), and packaged as the setoid whose quotient carries physical states (gaugeSetoid).
Creates-free-record dynamics are defined as maps that send some gauge pair to a non-gauge pair; record-compatible protocols never do that, which yields operational inseparability (gauge_never_separated). Together with the books-balance / no-free-erasure ledger theorems, the relation lets the module obtain weak complementarity on the gauge quotient from record accounting rather than from a monolithic complementarity premise. It sits on the forced eight-vertex cell (T7/T8 landmarks: eight-tick octave and $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.