compB_closed
plain-language theorem explainer
Any interior-side reading of seam and private bits extends to a globally closed cut configuration by zeroing the exterior and parking the residual parity on a free spike vertex. Holography and Bekenstein-count arguments cite this to justify that every B-marginal is realized by some closed ledger. The proof unfolds the completion, cancels the exterior sum, and uses the spike-sum identity plus ring arithmetic over GF(2).
Claim. For natural numbers $a,s,b,r$ and any seam assignment $g_S:\mathrm{Fin}\,s\to\mathbb{Z}/2\mathbb{Z}$ with interior private assignment $g_B:\mathrm{Fin}\,b\to\mathbb{Z}/2\mathbb{Z}$, the interior completion (exterior private bits set to zero, free rest vertex spiked to cancel total parity) is a closed cut configuration: its total recognition parity vanishes.
background
Module HorizonOneSidedCut discharges LEG-A of the Bekenstein master plan: a one-sided causal cut forces private duplicated edge records. The model is exact linear algebra over $\mathbb{Z}/2\mathbb{Z}$. A cut configuration splits vertices into exterior private $\mathrm{Fin},a$, seam $\mathrm{Fin},s$, interior private $\mathrm{Fin},b$, and a nonempty rest $\mathrm{Fin}(r+1)$. Regions are $A=a\sqcup s$ and $B=s\sqcup b$.
Global ledger closure cutClosed is the single balanced-loop constraint that the total recognition parity cutSum (sum of all four blocks) equals zero. The interior completion builds a closed config from an interior-side reading $(g_S,g_B)$ by setting exterior bits to zero and placing a spike on the free rest vertex equal to $-(\sum g_S+\sum g_B)$. Upstream, sum_spike states that the spike sums exactly to the value it carries, so the free vertex can cancel any prescribed parity.
proof idea
Term-mode proof that rewrites the goal as cutSum of the completion equals zero. Unfold compB and cutSum; the exterior block is the zero function, so its sum vanishes (Pi.zero_apply, Finset.sum_const_zero). The rest block is a spike whose sum equals the prescribed canceling value by sum_spike. What remains is an identity in $\mathbb{Z}/2\mathbb{Z}$ discharged by ring.
why it matters
This is the interior half of the completion toolkit that makes the one-sided cut surjective onto B-readings. Downstream, margB_image_univ applies it directly: every pair $(g_S,g_B)$ is the B-projection of the closed config built by this completion, so the closed-set image under projB is the full universe. That surjectivity feeds seam_posted_by_B, which states that tracing out the exterior, the interior marginal realizes all $2^s$ seam readings — "both sides independently carry the severed-edge records — they are duplicated across the cut."
In the module's physical claim, that private duplication is exactly why horizon entropy is the sum of per-pixel traced marginals ($\kappa=4$), not the joint marginal ($\kappa\to 1$): each side posts its own copy of the seam (T0 double-entry at the cut; Donnelly–Freidel–Geiller–Wall edge modes). Without interior closure of completions, the LEG-A forcing chain would not reach the additive reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.