physState
plain-language theorem explainer
Canonical projection from a bulk cell configuration to its physical state: the gauge class of that configuration. Physical states are bulk configs modulo the 16-element record kernel (same boundary record). Anyone citing weak complementarity or the bulk-to-boundary injection on the forced D=3 cell uses this map. The body is the standard quotient constructor for the gauge setoid.
Claim. For any bulk cell configuration $c$ (an element of $\mathrm{Fin}\,256$, one recognition bit on each of the $8=2^3$ vertices of the forced $D=3$ cell), write $\pi(c)$ for its physical state: the equivalence class of $c$ under the gauge relation (two configurations are gauge-equivalent precisely when they induce the same boundary face record). Thus $\pi$ is the canonical quotient map $\mathrm{CellCfg}\to\mathrm{PhysState}:=\mathrm{CellCfg}/\sim_{\mathrm{gauge}}$.
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.
A full-cell configuration packs one recognition bit on each of the eight vertices of the cube into $\mathrm{Fin},256$. Two configurations are gauge-related when they carry the same boundary record; by the injection test that relation is exactly membership of their XOR difference in the 16-element record kernel. The gauge setoid is that equivalence relation, and physical states are the corresponding quotient type.
The ledger side of the module already proves books balance (path heat equals the change of record-weight potential) and no free erasure. The present definition packages bulk data into the objects on which the quotient form of weak complementarity is stated.
proof idea
One-line definitional wrapper: apply the standard quotient constructor for the gauge setoid to the given cell configuration. No lemmas are invoked; the type of the result is the quotient of cell configurations by gauge equivalence.
why it matters
Weak complementarity is stated on physical states, not raw configurations: distinct gauge classes must carry distinct boundary records. Downstream, the simp lemma physRecord_mk says the boundary readout of $\pi(c)$ is exactly the face record of $c$, and physRecord_surjective_on_records shows every posted record is hit by some physical state. Together they give the bulk-phys $\hookrightarrow$ records injection (and, with surjectivity, a bijection onto posted records) that the holography manuscript isolates as the minimal sufficient form of recognition complementarity.
In the forcing chain this sits on the $D=3$ cell forced at T8 and the eight-tick octave at T7. It replaces the strongest holography premise with the quotient of the finite, classified gauge kernel already isolated by the cell-injection test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.