exteriorStepHeat
plain-language theorem explainer
One-step exterior heat between two closed local cuts is the integer record flux of their exterior bit strings (exterior-private plus seam bits only). Horizon and gravity modules cite it as the discrete posted heat carrier before real casting or channel sums. The body is a one-line alias of record flux on the two exterior records.
Claim. Given a shared local-horizon context $H$ (one-sided cut data, carrier sizes $a,s,b,r$, and near-horizon rate $\kappa$) and two closed local cuts $c,c'$ in that context, the one-step exterior heat is the integer $$Q^{\mathrm{ext}}(c,c') := \mathrm{recordFlux}\bigl(R^{\mathrm{ext}}(c), R^{\mathrm{ext}}(c')\bigr) \in \mathbb{Z},$$ where $R^{\mathrm{ext}}$ is the exterior-accessible Boolean record (exterior-private bits followed by seam bits).
background
The module builds local recognition horizon cuts by joining three audited legs on one shared context: a one-sided 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 MODEL (presently only $\kappa>0$). No stress tensor, Ricci, focusing, Unruh, or Einstein equation appears here.
A LocalHorizonContext packages the horizon record size, the one-sided sums-per-side premise, and the near-horizon rate. A LocalCut is a globally closed cut configuration relative to that context. The exterior record of a cut is the Boolean list of exterior-private entries followed by seam entries; interior-private and rest-of-universe data are traced out.
Record flux is the integer bit-level flux between two Boolean lists. The physical reading of that posted flux as horizon heat is inherited from the posting-rule MODEL, not proved in this definition.
proof idea
Definitional one-liner: evaluate record flux on the exterior records of the two cuts. No tactics, no lemmas beyond the in-module exterior-record projection and the imported record-flux carrier.
why it matters
This is the discrete heat atom for exterior books. Downstream, exteriorPathHeat sums it along paths and ExteriorClausius packages the Clausius-side balance. In gravity, exteriorStepHeat_eq_sum_channelDeltaZ and exteriorStepHeat_cast_eq_sum_channelDelta rewrite it as a sum of signed exterior channel deltas (integer and real), feeding quadContr_cutEventStress_eq_sq_mul_heat and the calibrated match matchesPostedBoostHeat_of_attachment (posted heat versus surface gravity times boost moment times null stress flux). The certificate RecordFluxBoostHeatCert and the decoy zero_covectors_fail_nonzero_posted_heat both quantify over this quantity. It sits in the holography leg that supplies posted exterior heat without claiming curvature or Einstein dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.