LocalCut
plain-language theorem explainer
A local cut is a globally closed one-sided ledger configuration packaged inside a shared local-horizon context (one-sided seam model, exterior record dimensions, and positive surface-gravity rate). Gravity and holography developments that transport posted exterior heat into channel stress or boost-calibrated flux cite this carrier. It is a pure structure: a cut configuration plus a closedness witness, with rate and one-sided premises held on the ambient context.
Claim. Fix natural numbers $a,s,b,r$ and a real surface-gravity parameter $\kappa$. Given a local-horizon context $H$ (horizon record length, one-sided seam model, and near-horizon Rindler form with that $\kappa$), a local cut relative to $H$ is a pair $(\mathrm{cfg},\mathrm{closed})$ where $\mathrm{cfg}$ is a globally closed cut configuration on exterior private vertices $\mathrm{Fin}\,a$, seam $\mathrm{Fin}\,s$, interior private vertices $\mathrm{Fin}\,b$, and rest-of-universe $\mathrm{Fin}(r+1)$, and $\mathrm{closed}$ asserts that configuration is closed.
background
The module assembles three audited legs on one shared context: the one-sided cut model (horizon record double-posts the seam), posted-record heat on the exterior projection of a closed cut, and a near-horizon rate model requiring only $\kappa>0$. No thermality, curvature, stress tensor, or Einstein equation is assumed here.
A cut configuration splits a globally closed ledger into exterior private bits, seam bits, interior private bits, and a nonempty rest-of-universe block. Closedness is the global parity/closure condition on that four-block assignment. The ambient local-horizon context carries the horizon record, the one-sided sums-per-side model, and the Rindler rate form; cut data are relative to that context rather than re-stating those premises.
Upstream, the shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ appears in the broader cost algebra (RCL becomes d'Alembert under $H$), but this declaration itself only packages discrete cut data and closedness.
proof idea
No proof body: this is a structure definition. Fields are the cut configuration (four-block $\mathbb{Z}/2$ assignment on exterior, seam, interior, and rest-of-universe) and a closedness witness for that configuration. Rate and one-sided premises are not fields; they live on the ambient local-horizon context parameter.
why it matters
Local cuts are the standard carrier for exterior posted heat and record-flux stress in the gravity layer. Downstream, exterior step heat equals the sum of real channel weights; uniform channel attachment calibrates posted heat against surface gravity, boost moment, and null stress flux; quadratic contractions of cut event stress reduce to posted heat times a squared pairing; and channel bit readouts extract exterior Boolean bits from a local cut.
In the Recognition holography program this is the discrete object that makes interior-private and rest-of-universe data invisible in the exterior record while still supporting books balance and unit-temperature Clausius theorems on that record. It sits under the local recognition horizon cut stack (one-sided cut, posted heat, near-horizon rate) without claiming Unruh thermality or a focusing law. Parent certificates such as the record-flux boost-heat certificate quantify over pairs of local cuts in a fixed context.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.