exteriorPotential
plain-language theorem explainer
Exterior posted-record potential assigns an integer bit-weight to any closed local horizon cut. It is the weight of the cut's exterior record only; interior-private data never enter. Downstream Clausius and books-balance theorems treat this integer as the discrete potential whose first difference is posted exterior heat. The body is a one-line composition of exterior record extraction with record weight.
Claim. Given a shared local-horizon context (one-sided cut model, carrier dimensions, near-horizon rate $\kappa$) and a globally closed cut configuration $c$ in that context, the exterior potential of $c$ is the integer weight of the exterior posted record of $c$.
background
The module assembles three audited legs on one shared context: a one-sided horizon cut model that double-posts the seam, posted-record heat with discrete books balance and unit-temperature Clausius as theorems about that record, and a near-horizon Rindler-form rate model (presently only $\kappa>0$). A local cut is a closed cut configuration living in that context; interior-private and rest-of-universe data are invisible in the exterior record.
LocalHorizonContext packages the horizon record size, the one-sided sums-per-side model, and the near-horizon rate model, with no thermality or curvature premise. LocalCut is then a closed CutCfg relative to that context. The exterior record is the exterior projection of the cut's posted bits; its weight is an integer in bit units.
No stress tensor, Ricci tensor, focusing law, curvature match, Unruh claim, or Einstein equation appears in the module. The physical identification of posted flux with horizon heat is inherited from the posting-rule model, not re-proved here.
proof idea
Pure definition: apply the exterior-record extractor to the closed local cut, then take the integer record weight of that bit string. No lemmas, no tactics, no hypotheses beyond the cut living in the shared context.
why it matters
This potential is the discrete state function that makes exterior heat exact. exteriorStepHeat_eq_potential states that one-step posted exterior heat equals the difference of exterior potentials. That identity is re-exported as cut-level discrete Clausius (exterior_record_potential_clausius), and telescopes to pathwise books balance (exterior_books_balance): total exterior path heat equals final minus initial potential.
In the Recognition holography stack this is the local, record-level stand-in for a horizon potential without invoking continuum GR. It sits downstream of the one-sided cut and posted-record legs and upstream of any later matching to continuum surface gravity or area laws. The module deliberately stops short of Einstein equations and Unruh thermality; those remain outside scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.