compB
plain-language theorem explainer
Completes an interior-side reading (seam bits plus interior private bits) to a globally closed cut configuration by zeroing the exterior private factor and parking the residual parity on a single free rest-of-universe vertex. Used whenever one needs an explicit closed lift of a B-side marginal. The construction is a pure data packing: zero exterior, keep the given interior data, spike the rest factor with the negated total parity.
Claim. Given seam bits $g_S:\mathrm{Fin}\,s\to\mathbb{Z}/2\mathbb{Z}$ and interior private bits $g_B:\mathrm{Fin}\,b\to\mathbb{Z}/2\mathbb{Z}$, form the cut configuration whose exterior private factor is identically $0$, whose seam and interior factors are $g_S$ and $g_B$, and whose rest-of-universe factor is the single-vertex spike carrying $-\bigl(\sum g_S+\sum g_B\bigr)$.
background
The module formalizes LEG-A of the Bekenstein master plan: a horizon as a one-sided causal cut forces private duplicated edge records on each side. Configurations live in CutCfg a s b r, a four-factor product over $\mathbb{Z}/2\mathbb{Z}$: exterior private vertices $\mathrm{Fin},a$, seam $\mathrm{Fin},s$ (severed-edge endpoints shared by both sides), interior private vertices $\mathrm{Fin},b$, and a nonempty rest-of-universe factor $\mathrm{Fin}(r+1)$.
Global ledger closure is even total parity across all four factors. The free rest factor always admits a one-vertex spike (value $x$ at index $0$, else $0$) that can absorb any residual parity a partial reading demands. The two pixels sharing the seam are region $A=a\sqcup s$ (exterior) and $B=s\sqcup b$ (interior).
This definition is the interior-side completion: it builds a closed global config from a pure $B$-reading without touching exterior private data beyond zeroing it.
proof idea
Pure definitional packing, not a proof. The four-tuple is assembled as (zero exterior map, given seam $g_S$, given interior $g_B$, spike of the negated sum of those two factors). The spike construction guarantees the rest factor contributes exactly the parity needed so the total cut sum vanishes; that cancellation is discharged later by the companion closedness lemma via sum_spike and a one-line ring identity.
why it matters
Supplies the explicit closed lift used by three downstream results that discharge the interior half of LEG-A. First, closedness of the lift is immediate. Second, the image of the closed set under the $B$-projection is the full product of seam and interior readings: every interior-side marginal is realized. Third, specializing the interior private factor to zero yields seam_posted_by_B: tracing out the exterior, the interior's accessible marginal realizes all $2^s$ seam readings.
Together with the symmetric exterior completion, this forces the Donnelly–Freidel–Geiller–Wall edge-mode prescription in RS terms (T0 double-entry at the cut): each side independently carries a full private copy of the severed-edge records, so summing the two traced marginals double-posts the seam and yields the additive $\kappa=4$ reading rather than the joint $\kappa\to 1$ reading. That is the geometric mechanism behind PerPixelRecordAdditivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.