stepHeatCell_eq_potential
plain-language theorem explainer
A single bulk step on the forced D=3 cell posts boundary heat equal to the change of the record potential: δQ = ΔΦ. Anyone proving ledger balance, no-free-erasure, or record monotonicity cites this identity. The proof is a one-line application of exact flux-to-weight difference once both face records are known to have length six.
Claim. For any two full-cell configurations $c,c'$, the boundary heat of the step from $c$ to $c'$ equals the difference of their record potentials: $\delta Q(c,c')=\Phi(c')-\Phi(c)$.
background
This module is step 3 of the entropy-fork chain toward weak complementarity on the forced D=3 cell. A cell configuration is one recognition bit on each of the eight vertices of the cube, packed as an element of $\mathrm{Fin},256$. Each configuration posts a six-bit face record (one channel per face of the cell).
The record weight of a bit-list is the integer count of posted bits; the cell potential $\Phi(c)$ is that weight on the face record of $c$. Boundary heat of one bulk step is the record flux between the two face records: channel-by-channel signed change of posted bits. Upstream, flux between equal-length records is exactly the weight difference ("Nothing is created or destroyed off the books").
The local goal is double-entry bookkeeping for the posted record: every erasure must export as negative boundary heat, so the generalized second law for the ledger is proved rather than assumed.
proof idea
One-line term proof. Apply the exact flux identity: for equal-length bit-lists, record flux equals weight difference. Discharge the length hypothesis by rewriting both sides with the fact that every face record has length six. The definitions of step heat and cell potential then match the two sides of the identity.
why it matters
This is the single-step ledger identity that makes the books balance. Path heat telescopes via this equality to $\Phi(\mathrm{end})-\Phi(\mathrm{start})$ (books_balance). Immediate corollaries: a zero-heat step preserves potential exactly (no_free_erasure); any potential drop forces strictly negative heat (erasure_exports_debit); closed trajectories with non-negative heat at every step are record-monotone (recordMonotone_of_no_export).
Those facts replace the monolithic complementarity premise of the holography manuscript with independently checkable record accounting. The identity is packaged into the module certificate target_record_monotonicity_holds, which assembles weak complementarity on the forced cell from the GSL half of the argument plus the kernel and protocol results. Framework landmark: D=3 is already forced (T8); the six face channels are the boundary of that cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.