weak_complementarity_of_gsl
plain-language theorem explainer
Under the premise that physical distinguishability is always witnessed by a posting-compatible protocol, any two bulk cell configurations that share the same boundary record are physically indistinguishable. Holography and entropy-fork workers cite this as the step-3 headline: weak complementarity from generalized-second-law bookkeeping. The proof is a one-line contradiction via operational inseparability of gauge pairs.
Claim. Let $\mathrm{dist}$ be a binary relation on bulk cell configurations. Suppose every pair distinguished by $\mathrm{dist}$ is separable by a posting-compatible protocol (the kernel-is-gauge premise). Then whenever $c$ and $c'$ are gauge-related (they carry the same boundary record), one has $\neg\,\mathrm{dist}(c,c')$.
background
This module is step 3 of the entropy-fork chain on the forced $D=3$ cell. Step 1 isolated the cell-injection test; step 2 the Clausius selector. The holography manuscript treats recognition complementarity as its strongest premise and isolates the minimal form: weak complementarity, an injection from physical bulk states into boundary letter space. The module replaces that monolithic premise by record accounting.
Ledger books balance: boundary heat equals posted record flux channel by channel, exact against a record-weight potential along any bulk trajectory. Hence no free erasure of the posted record: weight drop always exports as negative boundary heat, and zero-heat steps preserve weight. Two configurations are gauge-related when they share the same boundary record; that relation is exactly the coset structure of the 16-element record kernel.
KernelIsGauge is the named operational premise: a distinguishability relation respects the ledger when every physical distinction is witnessed by a posting-compatible protocol (distinguishing bulk states requires posting the difference). Upstream, finite protocols built from record-compatible steps never separate gauge pairs (gauge_never_separated).
proof idea
Term-mode one-liner. Assume dist c c'. The kernel-is-gauge hypothesis turns that into Separated c c' (separability by a posting-compatible protocol). But gauge_never_separated already says that gauge-related configurations are never so separated. Contradiction, so $\neg,\mathrm{dist}(c,c')$. No further algebra; the work sits in the upstream inseparability lemma and the definition of the premise.
why it matters
Step-3 headline of the entropy-fork development: weak complementarity from the GSL (no-free-erasure) discipline rather than a monolithic complementarity axiom. It lands inside the bundled certificate target_record_monotonicity_holds, which packages books-balance, gauge-kernel equivalence, protocol inseparability, and this theorem as the record-monotonicity target on the forced cell.
Its immediate sibling is the falsifier horn: if any physical process distinguishes a gauge pair (a global parity move made observable), then the kernel-is-gauge premise fails and weak complementarity breaks. The module isolates the breaking set (the 16 kernel moves) without claiming no physics ever separates them. Framework landmarks: forced $D=3$ cell (T8), eight-tick posting structure, and the holography manuscript's complementarity injection, now conditional only on ledger-respecting distinguishability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.