cutClosed
plain-language theorem explainer
Global ledger closure for a one-sided causal cut: a cut configuration is closed when the total GF(2) recognition parity over exterior private vertices, seam, interior private vertices, and rest-of-universe vanishes. Horizon and Bekenstein LEG-A arguments cite this as the closed-config predicate. It is a one-line definitional equality of the four-region parity sum with zero, with a decidable instance.
Claim. For $a,s,b,r\in\mathbb{N}$ and a cut configuration $c$ (parity maps 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)$), $c$ is closed when the sum of all four region parities equals $0$ in $\mathbb{Z}/2\mathbb{Z}$.
background
This module formalizes LEG-A of the Bekenstein master plan: a horizon as a one-sided causal cut forces privately duplicated seam records, yielding the additive $\kappa=4$ reading rather than a joint $\kappa\to 1$ marginal. Configurations live in exact linear algebra over $\mathbb{Z}/2\mathbb{Z}$.
A cut configuration is a 4-tuple of parity assignments: exterior private vertices, the seam (severed-edge endpoints shared by both sides), interior private vertices, and a nonempty rest-of-universe factor. The total recognition parity is the sum of the four region sums in $\mathbb{Z}/2\mathbb{Z}$.
The same closure idea appears locally as even face parity on a plaquette and as both unit faces balanced on a glued domino. Here it is lifted to one global balanced-loop constraint on the whole cut system.
proof idea
Definitional: closed means the four-region parity sum equals zero in $\mathbb{Z}/2\mathbb{Z}$. No proof body beyond that equality. A companion DecidablePred instance unfolds the definition and inherits decidability of equality in $\mathbb{Z}/2\mathbb{Z}$.
why it matters
This is the global closed-ledger predicate for the one-sided cut model. It defines the closed-configuration set (universe filtered by this predicate) and is the closedness obligation on side-completion maps: exterior-only, interior-only, and joint exterior-seam-interior completions all land in the closed set by cancelling the rest-of-universe spike against the partial sum.
Downstream, a local horizon cut structure packages a configuration together with this closedness proof inside a shared local-horizon context. That is the geometric input LEG-A needs so each side's trace independently realizes every seam bit and summing sides double-posts the seam (Donnelly–Freidel–Geiller–Wall edge modes; RS T0 double-entry at the cut), forcing additive $\kappa=4$ rather than a joint marginal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.