compAB
plain-language theorem explainer
Completes an arbitrary joint boundary reading on exterior private vertices, seam, and interior private vertices to a globally closed ledger configuration by placing a compensating parity spike in the rest-of-universe factor. Anyone building closed cut configs from free boundary data cites this constructor. The body is a direct four-tuple assembly: the three given maps plus a spike whose value cancels their total GF(2) sum.
Claim. Given boundary assignments $g_A:\{0,\ldots,a-1\}\to\mathbb{Z}/2\mathbb{Z}$, $g_S:\{0,\ldots,s-1\}\to\mathbb{Z}/2\mathbb{Z}$, and $g_B:\{0,\ldots,b-1\}\to\mathbb{Z}/2\mathbb{Z}$, form the cut configuration $(g_A,g_S,g_B,\sigma)$ whose rest-of-universe factor $\sigma$ is the single-vertex spike carrying $-(\sum g_A+\sum g_S+\sum g_B)$ in $\mathbb{Z}/2\mathbb{Z}$, so the total recognition parity of the completed configuration is zero.
background
This module formalizes LEG-A of the Bekenstein master plan: a horizon is a one-sided causal cut, so the exterior observer cannot condition on the interior. The ledger is exact linear algebra over $\mathbb{Z}/2\mathbb{Z}$. A cut configuration splits a globally closed recognition ledger into four factors: exterior private vertices $\mathrm{Fin},a$, the seam $\mathrm{Fin},s$ (severed-edge endpoints shared by both sides), interior private vertices $\mathrm{Fin},b$, and a nonempty rest-of-universe $\mathrm{Fin}(r+1)$.
The rest factor is nonempty precisely so a free vertex can always absorb whatever parity a partial reading demands. The spike map places a single value $x$ at index $0$ and zero elsewhere; its sum equals $x$. Completing a three-factor boundary reading therefore means choosing that free parity to cancel the boundary sum, restoring global closedness (total recognition parity zero).
proof idea
Pure definitional constructor, not a proof. Pack the three supplied boundary maps with a spike whose value is the additive inverse (in $\mathbb{Z}/2\mathbb{Z}$) of the sum of all three boundary totals. No lemmas are applied at the definition site; downstream closedness follows by simplifying the total cut sum against the spike-sum identity and cancelling in the ring.
why it matters
This is the canonical way to lift free joint boundary data $(g_A,g_S,g_B)$ into the closed configuration set used throughout the one-sided-cut argument. Downstream, closedness of the completion is immediate (compAB_closed), and that fact is the witness step in margAB_image_univ: every joint boundary triple is the projection of some closed config, so the joint marginal image is the full product space.
That surjectivity is part of the geometric mechanism forcing per-pixel record additivity: each side's trace independently realizes every seam bit, so summing the two sides double-posts the seam. In the Bekenstein plan this is the LEG-A input that selects the additive $\kappa=4$ reading (Donnelly–Freidel–Geiller–Wall edge modes; RS T0 double-entry at the cut) over the joint $\kappa\to 1$ alternative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.