exteriorStepHeat_zero_of_same_projection
plain-language theorem explainer
If two closed local horizon cuts share the same exterior-accessible projection (exterior-private bits plus seam), the exterior step heat between them vanishes. Horizon bookkeeping and one-sided Clausius arguments cite this as the exact one-sidedness of posted exterior heat. The proof recovers equal exterior records from the projection equality and applies self-flux vanishing on that record.
Claim. Fix a local horizon context $H$ (one-sided cut model, carrier dimensions, near-horizon rate $\kappa$). For closed local cuts $c,c'$ in $H$, if the exterior projections agree—$\mathrm{proj}_A(c)=\mathrm{proj}_A(c')$, i.e. the exterior-private and seam bit strings match—then the exterior step heat between $c$ and $c'$ is zero.
background
The module assembles three audited legs on one shared LocalHorizonContext: a one-sided cut model (HorizonSumsPerSide), posted-record heat on exterior projections of closed cut configurations, and a near-horizon Rindler-form rate model (kappa > 0). A LocalCut is a closed CutCfg living in that context. Interior-private and rest-of-universe data are invisible to the exterior record; no stress tensor, Ricci focusing, Unruh claim, or Einstein equation appears here.
The exterior projection projA keeps exterior-private and seam bits and traces the rest. The exterior record is the concatenated Boolean readout of those two blocks. Exterior step heat is the posted heat (record flux) between two such exterior records. The cost algebra's shifted cost $H(x)=J(x)+1$ sits upstream in the broader Recognition stack but is not invoked in this short argument; the local content is pure record bookkeeping on the one-sided cut.
proof idea
From projA c.cfg = projA c'.cfg, project to the two factors: exterior-private bits agree and seam bits agree. Rewrite the definition of the exterior record under those equalities to obtain identical exterior records. Unfold exterior step heat (the record flux between the two exterior records) and reduce to flux of a record against itself, which is zero by recordFlux_self.
why it matters
Doc-comment states the role directly: exterior heat ignores every change hidden behind the same exterior projection; this is the exact one-sidedness statement used by the record bookkeeping. Sibling results in the module (exterior_record_potential_clausius, exterior_books_balance, exterior path heat) rely on heat depending only on the posted exterior record, not on interior-private or rest-of-universe data.
In the Recognition holography layer this encodes the one-sided cut: the horizon double-posts the seam while interior degrees of freedom drop out of exterior heat. It supports the module's claim that posted-record heat and unit-temperature Clausius statements are theorems about the exterior record alone. No downstream consumers are wired yet (used_by empty); the lemma is infrastructure for local horizon thermodynamics without curvature or Einstein matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.