no_protocol_separates
plain-language theorem explainer
Any finite sequence of record-compatible bulk maps preserves gauge equivalence on the forced D=3 cell: if two configurations share a boundary record, so do their images under the whole protocol. Holography and entropy-fork arguments cite this as the closure step that turns single-step no-free-record into operational inseparability of gauge pairs. The proof is list induction, applying record-compatibility at the head and the inductive hypothesis on the tail.
Claim. Let $U_1,\ldots,U_n$ be bulk maps $C\to C$ on cell configurations, each record-compatible (gauge-related inputs yield gauge-related outputs). Then for every pair $c,c'$ with the same boundary record, the configurations obtained by running the protocol $U_n\circ\cdots\circ U_1$ on $c$ and on $c'$ again share the same boundary record.
background
This module is step 3 of the entropy-fork chain toward weak complementarity on the forced $D=3$ cell. A cell configuration is one recognition bit on each of the eight vertices of the cube, packed as an element of $\mathrm{Fin},256$. Two configurations are gauge-related when they carry the same boundary record (identical posted face data).
A bulk dynamics is record-compatible when it never turns an unposted difference into a posted one: gauge-related inputs go to gauge-related outputs. That single-step discipline is the difference-ledger form of the module's no-free-erasure bookkeeping (boundary heat equals record-weight change along any trajectory).
A protocol is a finite list of such maps, run by left-fold composition. The claim is that the whole fold still preserves gauge equivalence, so no posting-compatible dynamics can manufacture a boundary distinction from a pure gauge pair.
proof idea
Induct on the protocol list. The empty protocol is the identity, so gauge relation is immediate. For a cons step $U::\mathrm{rest}$, apply the head's record-compatibility hypothesis (membership in the cons list) to obtain gauge relation after $U$. Restrict the compatibility hypothesis to the tail and feed the inductive hypothesis the pair $(U c, U c')$. Rewrite the fold definition of running the protocol to finish.
why it matters
This is item 3 in the module's argument outline: protocol closure under record-compatible steps. It feeds gauge_never_separated, which states that gauge pairs are operationally inseparable (no posting-compatible protocol drives them to distinct boundary records), by a one-line contradiction against the definition of separation.
It is also packaged into the module certificate target_record_monotonicity_holds, alongside books-balance, the gauge-kernel identification, and weak complementarity on the quotient. Together these replace the holography manuscript's monolithic complementarity premise with weaker, independently checkable record-accounting inputs on the forced cell (T8: $D=3$, eight-tick octave structure underlying the cell).
Without protocol closure, single-step no-free-record would not rule out multi-step manufacturing of free boundary distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.