ofExteriorReading
plain-language theorem explainer
Every exterior-and-seam bit reading on a shared local-horizon context extends to a closed local cut. Horizon holography arguments use this constructor when only boundary and seam data are available. It is a definitional package: compose the readings into a cut configuration and discharge closedness by the companion composition lemma.
Claim. Fix a local horizon context $H$ with exterior length $a$, seam length $s$, bulk and rest dimensions $b,r$, and surface gravity parameter $\kappa$. For any exterior bit map $g_A:\{0,\ldots,a-1\}\to\mathbb{Z}/2\mathbb{Z}$ and seam bit map $g_S:\{0,\ldots,s-1\}\to\mathbb{Z}/2\mathbb{Z}$, there exists a closed local cut in $H$ whose configuration is the composition of $g_A$ and $g_S$.
background
The module joins three audited legs on one shared context: a one-sided-cut model that double-posts the seam into the horizon record; posted-record heat theorems (discrete books balance and unit-temperature Clausius) about the exterior projection of a closed cut; and a near-horizon Rindler-form model with positive surface gravity. No stress tensor, Ricci curvature, focusing law, Unruh claim, or Einstein equation appears here.
A local horizon context packages the horizon record length, the one-sided-cut model, and the near-horizon rate model, without thermality or curvature premises. A local cut is then a cut configuration relative to that context together with a global closedness witness. Interior-private and rest-of-universe data stay invisible in the exterior record.
Bit readings are maps into $\mathbb{Z}/2\mathbb{Z}$; the Boolean-to-natural bit map used elsewhere in the stack sends false to 0 and true to 1. The shifted cost $H(x)=J(x)+1$ and related counting utilities sit upstream but are not invoked by this constructor itself.
proof idea
Definitional constructor, not a tactic proof. The cut configuration field is set to the composition of the exterior and seam readings (with bulk and rest dimensions taken from the context parameters). Closedness is discharged in one step by the companion lemma that the same composition yields a closed cut. No further rewriting or case analysis is required.
why it matters
This is the canonical way to promote pure exterior-plus-seam data into a closed local cut inside the shared horizon context. Downstream exterior-record, potential, step-heat, and Clausius statements in the same module are stated about such cuts; without this constructor those theorems would have no standard inhabitant built only from boundary readings.
In the broader Recognition stack the construction supports the holographic claim that interior-private data never enter the exterior record, while the one-sided-cut model forces the horizon record to double-post the seam. It sits on the holography leg rather than the T0–T8 forcing chain, and deliberately stops short of curvature matching or Einstein dynamics. No downstream dependents are recorded yet; the immediate consumers are the sibling exterior-record and books-balance results in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.