exterior_record_potential_clausius
plain-language theorem explainer
The exterior posted-record potential on closed local horizon cuts obeys unit-temperature discrete Clausius: step heat equals the change of that potential. Horizon and holography workers cite it when treating exterior bit records as thermodynamic carriers. The argument is a one-line term identification with the already-proved equality of exterior step heat and potential difference.
Claim. Fix a local horizon context $H$ (one-sided cut model, posted-record carrier dimensions, near-horizon rate $\kappa>0$). Let $S$ be the exterior posted-record potential on closed local cuts of $H$, valued in integer bit units. Then $S$ satisfies discrete Clausius at unit temperature: for all closed local cuts $c,c'$, the posted exterior step heat from $c$ to $c'$ equals $S(c')-S(c)$.
background
This module packages three audited legs on one shared context: a one-sided horizon cut model (seam double-posting), posted-record heat with discrete books balance, and a near-horizon Rindler-form rate model with $\kappa>0$. A local cut is a globally closed cut configuration in that context. Interior-private and rest-of-universe data never appear in the exterior record. No stress tensor, Ricci curvature, focusing law, Unruh claim, or Einstein equation is present.
The exterior potential of a local cut is the integer record weight of its exterior bit string. Exterior step heat is the posted heat between two such cuts. The discrete Clausius predicate on a candidate entropy map $S$ asserts that step heat equals $S(c')-S(c)$ for every pair of cuts: record thermodynamics in bit units, not continuum Unruh thermality.
Upstream, posted exterior heat is already identified with the change of record potential via the flux-versus-weight lemma on equal-length exterior records.
proof idea
One-line term proof. The target predicate ExteriorClausius applied to the exterior potential is definitionally the statement that exterior step heat equals the potential difference for every pair of local cuts. That identity is exactly the prior theorem that exterior step heat equals the change of exterior potential (itself a short appeal to record-flux equaling weight difference on equal-length exterior records). Supplying that theorem discharges the predicate.
why it matters
In the Recognition holography stack this seals cut-level discrete Clausius for the exterior record potential inside the local recognition horizon-cut setting. It converts the flux-versus-weight identity into the named thermodynamic interface used by later path-heat and books-balance developments in the same module (total posted exterior heat along paths of closed cuts, exterior books balance).
The module deliberately stops short of continuum thermality: Clausius here is unit-temperature bookkeeping on bit records. That matches the RS program of deriving thermodynamic bookkeeping from recognition/record structure before any curvature or Unruh identification. No forcing-chain landmark (T5–T8, RCL, $\phi$, eight-tick) is invoked; the result is pure discrete record thermodynamics on the local cut carrier.
No downstream consumers are wired yet; the declaration is the Clausius interface those path-level results are expected to quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.