runProtocol
plain-language theorem explainer
Finite bulk protocols act by left-fold composition: apply each cell map in list order to a starting configuration. Anyone stating protocol closure, operational separation, or the record-monotonicity target cites this runner. The body is the standard list fold of successive maps; no extra hypotheses.
Claim. Given a finite list of bulk evolution maps $U_1,\ldots,U_n : \mathrm{CellCfg}\to\mathrm{CellCfg}$ and a cell configuration $c$, the protocol result is $U_n(\cdots U_1(c)\cdots)$ (left-to-right composition via fold).
background
Module RecordMonotonicity 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 bulk state is a CellCfg. Dynamics enter as maps CellCfg → CellCfg. A finite protocol is just a list of such maps. Record compatibility (used downstream) means a step never manufactures a boundary distinction between states whose difference was never posted; that is the difference-ledger form of the proved no-free-erasure bookkeeping (books_balance, no_free_erasure).
Gauge relatedness (gaugeRel) equates configurations with the same boundary record and coincides with the 16-element record-kernel cosets. This runner supplies the operational action of a protocol so those gauge facts can be lifted from single steps to finite sequences.
proof idea
Pure definition: List.foldl of the function $(x,U)\mapsto U(x)$ starting at $c$. Empty list returns $c$; cons applies the head map then recurses on the tail. No lemmas, no tactics.
why it matters
This is the operational semantics for finite bulk dynamics in the holography ledger argument. Downstream, no_protocol_separates inducts on the list and uses the runner to show every finite protocol of record-compatible steps preserves gaugeRel: gauge pairs stay gauge-related after the run. Separated packages existence of a compatible protocol that drives two configs to distinct boundary records via this runner; gauge_never_separated then says gauge pairs are never operationally separated.
Both facts appear as clause (3) of target_record_monotonicity, the packaged target for the module: books balance, gauge = kernel cosets, protocol closure, injectivity of the physical record readout (weak complementarity), and the 16-state / 4-posted-bit count inside 6-bit boundary capacity. In the manuscript framing, that closes the gap between proved record bookkeeping and weak complementarity on the forced cell (T8, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.