recordFlux_self
plain-language theorem explainer
A boundary record posts zero flux against itself: the six-channel ledger difference vanishes on the diagonal. Anyone proving that gauge motion is heat-free, or that exterior heat ignores hidden bulk changes, cites this identity. The proof rewrites flux as a weight difference and cancels by ring.
Claim. For every boundary record $r$ (a list of bits), the posted flux from $r$ to itself is zero: $\mathrm{flux}(r,r)=0$. Equivalently, the signed sum of bit flips over face channels vanishes when the two records coincide.
background
This module sits in step 3 of the entropy-fork holography chain: derive weak complementarity on the forced $D=3$ cell from record accounting rather than assuming full recognition complementarity. Boundary heat is identified with posted ledger flux, channel by channel, matching the Clausius selector's step-heat model but summed over the six faces of the cell.
The per-channel posted flux between two equal-length records is the signed sum of one integer per face flip ($+1$ up, $-1$ down, $0$ unchanged). Record weight is the total number of posted bits; it plays the role of a potential. Upstream, flux is exact against that potential: for equal lengths, flux equals end weight minus start weight, so nothing is created or destroyed off the books.
The present identity is the diagonal case of that exactness: a record compared to itself posts no net change.
proof idea
Apply the exactness lemma that flux equals weight difference whenever the two records have equal length (here both are $r$, so lengths match by reflexivity). The goal becomes $\mathrm{weight}(r)-\mathrm{weight}(r)=0$, which ring discharges immediately. No induction or case split is needed beyond what the upstream exactness proof already supplies.
why it matters
This is the trivial but load-bearing diagonal of the ledger bookkeeping that underwrites "no free erasure" on the forced cell. Downstream, gauge motion is heat-free precisely because a gauge pair shares the same face record, so step heat reduces to flux of a record against itself and vanishes by this theorem. The same identity feeds the one-sided exterior-heat statement: exterior heat ignores every change hidden behind a fixed exterior projection, which is the exact one-sidedness used by record bookkeeping.
In the holography manuscript's program, these facts replace a monolithic complementarity premise with independently checkable ledger rules. They sit under the generalized second-law bookkeeping (books balance along bulk trajectories; erasures export as negative boundary heat) that the module proves rather than assumes, and they support the later claim that no record-compatible protocol separates a gauge pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.