physRecord
plain-language theorem explainer
The boundary record of a physical bulk state is the six face-closure parities, lifted from configurations to the gauge quotient. Anyone citing weak complementarity or the bulk-to-boundary injection on the forced cell uses this readout. The definition is the quotient lift of the face-record map; well-definedness is immediate from the gauge setoid.
Claim. The boundary record of a physical state $s$ is the list of six face-closure parities obtained by lifting the configuration-level face record through the gauge quotient: configurations that differ by a record-kernel move share the same boundary record, so the map is well-defined on physical states $s \in \mathrm{PhysState}$.
background
This module is step 3 of the entropy-fork chain on the forced $D=3$ cell. Physical states are bulk cell configurations modulo gauge: two configurations are identified when they carry the same boundary record, equivalently when their XOR difference lies in the 16-element record kernel. The type of physical states is that quotient.
Upstream, the face record of a configuration is the six Boolean face-closure parities (one per cube face), each parity collecting the four vertices on that face. That list is everything the ledger posts at the cell boundary. Because gauge equivalence is defined by equality of those records, the face-record map is constant on equivalence classes and descends to the quotient.
The local goal is weak complementarity: an injection from physical bulk states into boundary letter space, derived from record accounting rather than assumed as a monolithic holography premise.
proof idea
One-line definition by quotient lift: apply the configuration face-record map on representatives, and discharge the well-definedness obligation with the setoid witness itself (gauge-related pairs already have identical face records). No further lemmas are invoked at the definition site.
why it matters
This is the bulk-to-boundary readout on physical states. Downstream, injectivity of the map is exactly weak complementarity (the holography manuscript's minimal sufficient form of recognition complementarity, here a theorem on the gauge quotient). Simp lemmas identify the record of a class with the face record of any representative; image and surjectivity facts show every physical state's record is a posted record and every posted record is realized, so with injectivity one obtains a bijection between physical states and posted records.
The record-monotonicity target packages this injectivity as clause (4) of the module's checklist, alongside books-balance (no free erasure), kernel cosets as gauge classes, and inseparability under record-compatible protocols. In the broader RS holography program this replaces a strong complementarity premise by ledger bookkeeping on the forced cell (T8, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.