recordCompatible_iff_no_free_record
plain-language theorem explainer
Record-compatible bulk dynamics are exactly those that never create a free record: gauge pairs stay gauge pairs under the map if and only if no gauge pair is driven to distinct boundary records. Anyone citing the no-free-record discipline as a dynamical constraint uses this equivalence. The proof is a two-line logical dualization (constructor plus by_contra).
Claim. For any bulk cell map $U : \mathrm{CellCfg} \to \mathrm{CellCfg}$, $U$ is record-compatible (gauge-related inputs yield gauge-related outputs) if and only if $U$ does not create a free record (there do not exist gauge-related $c,c'$ with $U(c)$ and $U(c')$ not gauge-related).
background
This module is step 3 of the entropy-fork chain toward weak complementarity on the forced $D=3$ cell. Configurations are full-cell states CellCfg $= \mathrm{Fin},256$: one recognition bit on each of the $8=2^3$ vertices. Two configurations are gauge-related when they carry the same boundary record (identical posted face data).
Record compatibility says a bulk map never turns an unposted difference into a posted one: if $c$ and $c'$ are gauge-related, so are $U(c)$ and $U(c')$. Creating a free record is the existential dual: some gauge pair is driven to distinct boundary records, a boundary distinction with no posted source.
Part 1 of the module already proves ledger bookkeeping for the posting rule itself (books_balance, no_free_erasure, erasure_exports_debit). The present statement lifts that GSL discipline from static flux accounting onto dynamics.
proof idea
Pure logical equivalence of a universal implication and the negation of its existential dual. One direction: from record-compatibility, unpack a free-record witness $\langle c,c',h_{\mathrm{gauge}},h_{\mathrm{ne}}\rangle$ and apply compatibility to $h_{\mathrm{gauge}}$ to contradict $h_{\mathrm{ne}}$. Other direction: assume no free record, take gauge-related $c,c'$, and by_contra on the image pair; the resulting witness is exactly a free record. No holography lemmas are invoked; the two defs are dual by construction.
why it matters
The module doc names this as the bridge that turns Part 1's no-free-erasure bookkeeping into a dynamical constraint: "record compatibility IS the no-free-record condition... imposed on dynamics." Downstream in the same module, finite protocols built from record-compatible steps preserve gauge equivalence (no_protocol_separates), so gauge pairs are operationally inseparable (gauge_never_separated). That inseparability is the operational half of weak complementarity on the forced cell, replacing the manuscript's monolithic complementarity premise with independently falsifiable record accounting.
No external used-by edges are recorded yet; the declaration is an internal hinge of the holography entropy-fork panel. Framework landmarks: forced $D=3$ cell (T8) and the eight-tick/eight-vertex packing (T7) fix the configuration space on which the gauge kernel lives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.