CreatesFreeRecord
plain-language theorem explainer
A dynamics on cell configurations creates a free record when it sends some gauge pair (identical posted boundary data) to a pair that is no longer gauge-related: a boundary distinction with no posted source. Anyone citing the entropy-fork or weak-complementarity argument uses this predicate as the difference-ledger form of no-free-erasure imposed on maps. The body is a pure existential Prop, not a proved claim.
Claim. A map $U$ on cell configurations creates a free record if there exist configurations $c,c'$ that are gauge-related (same posted boundary record, zero-heat difference channel) while $U(c)$ and $U(c')$ are not gauge-related.
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.
Two configurations are gauge-related when they carry the same boundary record. Upstream, that relation is exactly the coset structure of the 16-element record kernel from the cell-injection test: gauge pairs differ by a global parity move in that kernel. Boundary heat equals posted record flux channel by channel; along any bulk trajectory the books balance exactly against a record-weight potential, so posted bits cannot be silently destroyed.
A free record is the dual failure mode for dynamics: manufacturing a new boundary distinction between states whose difference was never posted. That is the generalized-second-law discipline of Part 1, now stated as a property of maps rather than of heat bookkeeping along paths.
proof idea
Definitional, not a proof. The predicate is the existential statement that some gauge pair is separated by $U$: there exist $c,c'$ with gauge relation holding before the step and failing after. No lemmas are applied; downstream theorems unfold or negate this Prop directly.
why it matters
This predicate is the right-hand side of the equivalence recordCompatible_iff_no_free_record: a dynamics is record-compatible if and only if it does not create a free record. That equivalence is the hinge between the proved ledger balance (no free erasure of posted weight) and the dynamical discipline used later: finite protocols built from record-compatible steps never separate gauge pairs, so gauge pairs are operationally inseparable.
In the holography manuscript's entropy-fork plan, weak complementarity is the minimal sufficient form of recognition complementarity. Replacing the monolithic premise by independently falsifiable ledger and compatibility inputs is the module's job; this definition names the dynamical half of that split. It sits on the forced cell geometry ($D=3$, eight-tick octave context) but does not itself invoke $J$-cost uniqueness or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.