PhysState
plain-language theorem explainer
Physical states of the forced D=3 cell are bulk configurations modulo gauge equivalence: two configs are identified when they post the same boundary record (equivalently, when their XOR difference lies in the 16-element record kernel). Anyone citing weak complementarity or the bulk-to-boundary record map works over this quotient type. The definition is the plain setoid quotient by the gauge relation.
Claim. Define the type of physical states of the cell as the quotient of bulk cell configurations by gauge equivalence: two configurations are equivalent precisely when they carry the same boundary face-record (equivalently, when their XOR difference lies in the 16-element record kernel).
background
This module is step 3 of the entropy-fork chain toward weak complementarity on the forced D=3 cell: an injection from physical bulk states into boundary letter space, derived from record accounting rather than assumed as a monolithic premise.
Gauge equivalence identifies bulk configurations that post the same boundary record. By the already-proved kernel classification, that relation is exactly the coset structure of a named 16-element record kernel (global parity moves). The gauge setoid packages that relation as an equivalence on cell configurations.
The upstream carried construction (monochromatic adjacencies of the polarized birth field) sits in the broader lattice-edge bookkeeping; here the relevant local object is the gauge setoid itself, whose quotient is the type of physical states.
proof idea
One-line definition: the type is the quotient of cell configurations by the gauge setoid (the setoid whose relation is gauge equivalence, already shown equivalent to membership of the XOR difference in the record kernel). No proof obligations beyond the setoid instance.
why it matters
This is the carrier type for weak complementarity on the cell. Downstream, the boundary record lifts to a well-defined map on physical states; every physical state's record is a posted record; and every posted record is realized by some physical state. Together with the injection theorem on the quotient, physical states biject with posted records.
In the holography manuscript's terms, recognition complementarity is isolated to its minimal sufficient form (weak complementarity). The quotient is where that statement lives: bulk configurations modulo the only candidate complementarity violations (the 16 kernel moves). It sits after books-balance / no-free-erasure and the gauge-kernel classification, and before the operational inseparability and quotient-level injection results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.