exteriorStepHeat_eq_potential
plain-language theorem explainer
Posted exterior heat between two closed local cuts equals the difference of their exterior record potentials. Holography and discrete-thermodynamics arguments cite this as the single-step identity behind cut-level Clausius and path books balance. The proof is a short application of the record-flux weight-subtraction lemma once exterior record lengths match.
Claim. Fix a shared local-horizon context $H$ (one-sided cut model, carrier dimensions, near-horizon rate $\kappa$). For any two closed local cuts $c,c'$ in that context, the posted exterior step heat from $c$ to $c'$ equals the change of exterior record potential: $Q_{\mathrm{ext}}(c,c') = \Phi_{\mathrm{ext}}(c') - \Phi_{\mathrm{ext}}(c)$.
background
This module packages three audited legs on one carrier: a one-sided horizon cut model (seam double-posting), posted-record exterior heat with discrete books balance, and a near-horizon Rindler-form rate model with $\kappa>0$. A LocalHorizonContext holds the shared horizon record size, the one-sided sums premise, and the rate model; it deliberately omits thermality and curvature. A LocalCut is a globally closed cut configuration relative to that context.
Exterior data are the projection of the closed cut onto the exterior record. Interior-private and rest-of-universe bits are invisible there. The exterior potential is the integer weight of that exterior bit record; exterior step heat is the posted heat of one cut-to-cut transition in those bit units. The module states explicitly that this is record thermodynamics at unit temperature, not continuum Unruh thermality, and that no stress tensor, Ricci tensor, focusing law, or Einstein equation appears.
Upstream, the cost algebra $H(x)=J(x)+1$ and bit readouts supply the ledger language in which record weights and fluxes are written; the present identity is the cut-level specialization of flux equaling weight difference when record lengths agree.
proof idea
Term-mode one-liner. Apply the general record-flux identity that flux between two records equals the difference of their weights, once both records have the same length. Discharge the length hypothesis by rewriting both sides with the exterior-record length lemma (same length for every closed local cut in the shared context). No further case splits or induction.
why it matters
This is the single-step engine for exterior record thermodynamics on local recognition horizons. Downstream, exterior_record_potential_clausius is literally this identity packaged as the unit-temperature discrete Clausius predicate on the exterior potential ("record thermodynamics in bit units, not continuum Unruh thermality"). The path-level theorem exterior_books_balance then telescopes step heat along any finite trajectory of closed local cuts to endpoint potential difference.
In the broader Recognition holography stack, the result sits on the posted-record leg of the local horizon cut: one-sided seam double-posting plus exterior projection, without claiming Einstein equations or Unruh temperature. It converts the abstract flux-weight calculus into a concrete Clausius/books-balance statement usable by later horizon and ledger arguments. It does not close LEG-B curvature or focusing gaps; it only locks the exterior heat-potential link once the cut is closed in the shared context.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.