RecordCompatible
plain-language theorem explainer
A bulk map on forced D=3 cell configurations is record-compatible when it preserves gauge equivalence: equal boundary face records stay equal after the map. Entropy-fork and holography arguments cite this as the dynamics-side form of "no free record." It is a pure predicate definition (universal quantification over gauge pairs), not a proved theorem.
Claim. A bulk dynamics $U$ on cell configurations is record-compatible when, for all configurations $c,c'$, if $c$ and $c'$ carry the same boundary face record then so do $U(c)$ and $U(c')$.
background
Module RecordMonotonicity is step 3 of the entropy-fork chain toward weak complementarity on the forced D=3 cell: replace monolithic recognition complementarity by ledger bookkeeping plus a dynamics discipline. A cell configuration is one recognition bit on each of the eight vertices of the cube, packed as an element of a 256-point space.
Two configurations are gauge-related when they post the same six-face boundary record. That relation is the candidate "physically identical" relation of the fork selector: an unposted bulk difference is not a performed distinction. The module already proves that boundary heat equals the change in a record-weight potential along any trajectory (books balance), so posted bits cannot be silently erased.
Record compatibility lifts that ledger discipline from static accounting to maps: a dynamics must not manufacture a boundary distinction between states whose difference was never posted.
proof idea
Definitional: the predicate is the universal closure of gauge-relation under the map $U$. No tactics or lemmas; the body is exactly $\forall c,c',,\mathrm{gaugeRel}(c,c')\Rightarrow\mathrm{gaugeRel}(U c,U c')$. Downstream theorems treat this Prop as the hypothesis class of posting-compatible steps.
why it matters
This is the named dynamics hypothesis in the entropy-fork argument that weak complementarity follows from record accounting rather than from a monolithic complementarity premise. It is literally identified with the no-free-record condition (recordCompatible_iff_no_free_record): the generalized-second-law discipline of Part 1, imposed on bulk maps.
Protocol closure (no_protocol_separates) inducts on finite lists of such maps to show gauge pairs stay gauge-related under any posting-compatible protocol. Operational separation (Separated) is defined as existence of a record-compatible protocol that breaks gauge relation; gauge pairs are then inseparable. The composite target (target_record_monotonicity) packages books balance, kernel cosets, protocol closure, injectivity of the physical record readout, and the 16-state / 4-posted-bit count on the forced cell (T8: D=3, eight-tick octave).
Together these replace the holography manuscript's strongest premise by two weaker, independently falsifiable inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.