cellPotential
plain-language theorem explainer
The record potential of a bulk cell is the integer weight of the six-face boundary record: how many bits are posted on the cell boundary. Downstream balance and no-free-erasure theorems treat this as the thermodynamic potential conjugate to boundary heat. The definition is a one-line composition of face readout and Hamming-style weight.
Claim. For a bulk cell configuration $c$, the record potential is $\Phi(c) := w(\partial c)$, the integer weight of the posted bits on the six faces of $c$.
background
This module is step 3 of the entropy-fork chain toward weak complementarity on the forced $D=3$ cell. The holography manuscript isolates weak complementarity (injection of physical bulk states into boundary letter space) as the strongest premise; here it is rebuilt from record accounting.
A cell configuration carries a six-face boundary record. The record weight counts posted bits on those faces. Boundary heat of a bulk step is the posted flux across the six face channels (same posting rule as the Clausius selector, summed over faces). The record potential is the state function against which that flux is exact.
Local setting: ledger books must balance along bulk trajectories so that erasures export as negative boundary heat rather than silent destruction of posted bits. That bookkeeping is the generalized-second-law half of the argument, before gauge classes and protocol inseparability.
proof idea
Pure definition: compose the face-record map of a cell with the integer record-weight functional. No proof obligations; the body is recordWeight (faceRecord c). Downstream equalities (flux equals potential difference) inherit length hypotheses on the face records from sibling lemmas.
why it matters
This potential is the state function in the books-balance theorem: along any bulk path, total posted heat equals $\Phi(\mathrm{end})-\Phi(\mathrm{start})$. From that identity follow no-free-erasure (zero heat preserves weight), erasure-exports-debit (weight drop forces negative heat), and the record-monotone predicate on trajectories.
Those facts discharge the first clause of the module target (boundary heat exact against the record potential) and feed the weak-complementarity program: replace monolithic complementarity by falsifiable record accounting on the forced cell. Framework landmark: $D=3$ eight-tick cell geometry (T7–T8) supplies the six-face boundary on which the potential is evaluated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.