weak_complementarity
plain-language theorem explainer
Boundary record readout is injective on physical bulk states: distinct physical states carry distinct boundary records. Holography researchers cite this as the weak complementarity injection from physical bulk into boundary letter space. The proof is a short quotient argument: after reducing to configuration representatives, equal lifted face-records mean the representatives are gauge-related, so the physical-state classes coincide.
Claim. The boundary-record map on physical states is injective: whenever two physical bulk states determine the same boundary record, they are equal as physical states. Equivalently, there is an injection $\mathrm{bulk}_{\mathrm{phys}}(B)\hookrightarrow\mathrm{records}(\partial B)$.
background
This module is step 3 of the entropy-fork holography chain. Weak complementarity is the minimal form of recognition complementarity assumed by the holography manuscript: an injection from physical bulk states into boundary letter space. Here that injection is obtained on the forced $D=3$ cell from record accounting rather than postulated.
Physical states are gauge classes of bulk configurations. Two configurations are gauge-related when they carry the same boundary face-record; the physical-state quotient collapses exactly those pairs. The boundary readout is the lift of the face-record map through that quotient, so it is well-defined on classes by construction.
Upstream, the same Quotient.sound pattern appears in the integer and rational constructions from logic: equality of representatives under the defining relation yields equality of classes. The face-record lift is the local instance of that pattern.
proof idea
Four-line quotient induction. Fix two physical states and assume their boundary records agree. Reduce both sides by double quotient induction to configuration representatives. After the lift, the hypothesis becomes equality of face-records on those representatives, which is exactly the gauge relation. Apply quotient soundness to conclude the classes are equal. No arithmetic or combinatorial content beyond the definition of the lift.
why it matters
Quotient-form weak complementarity is the injection the holography manuscript treats as its strongest premise; this module derives it from record bookkeeping on the forced cell ($D=3$ in the RS forcing chain). Downstream it is packaged into the target certificate target_record_monotonicity_holds alongside books-balance, gauge-kernel identification, and no-protocol-separation. It also feeds the image membership fact (every physical record is a posted record) and the cardinality identity (16 physical states = 16 posted records = 4 posted bits), which together embed the 8-vertex bulk into the posted-record set inside the 6-bit boundary. Closes the complementarity half of the entropy-fork plan by replacing a monolithic assumption with a theorem of the gauge quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.