compA
plain-language theorem explainer
Completes any exterior-plus-seam bit assignment to a globally closed cut configuration by zeroing the interior and parking the residual GF(2) parity on a single free rest vertex. Horizon and Bekenstein-count arguments cite it as the canonical exterior completion. The body is a four-tuple constructor using the spike absorber.
Claim. Given exterior private bits $g_A:\mathrm{Fin}\,a\to\mathbb{Z}/2\mathbb{Z}$ and seam bits $g_S:\mathrm{Fin}\,s\to\mathbb{Z}/2\mathbb{Z}$, form the cut configuration $(g_A,g_S,0,\mathrm{spike}_r(-( \sum g_A+\sum g_S)))$: interior private bits are identically zero, and the rest-of-universe factor carries a single nonzero entry equal to the negated total exterior-plus-seam parity.
background
The module formalizes LEG-A of the Bekenstein master plan: a horizon is a one-sided causal cut, so an exterior observer only sees a trace over the hidden interior. Configurations live in CutCfg a s b r, the product of GF(2) assignments on 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 factor $\mathrm{Fin}(r+1)$.
Global ledger closure means the sum of all four blocks is $0$ in $\mathbb{Z}/2\mathbb{Z}$. The spike map places a prescribed value at index $0$ of the rest factor and zero elsewhere; because that factor is nonempty, it can always absorb whatever parity a partial reading demands. Sibling notions of face/domino closure in the pixel modules are the local special cases of the same even-parity loop condition.
proof idea
Pure data constructor, not a proof. Pack the given exterior and seam maps, the zero map on $\mathrm{Fin},b$, and spike r applied to the negation of $\sum g_A+\sum g_S$. Downstream compA_closed then reduces total cut sum via sum_spike and cancels by ring arithmetic in $\mathbb{Z}/2\mathbb{Z}$.
why it matters
This is the geometric completion that makes exterior marginals surjective onto all $2^{a+s}$ readings. It feeds compA_closed (closure), margA_image_univ ("every exterior-side reading extends to a closed configuration"), and seam_posted_by_A ("the exterior side posts a full private copy of the seam"). Those theorems force private duplicated edge records at the cut, hence the additive $\kappa=4$ per-pixel count rather than the joint $\kappa\to 1$ reading: T0 double-entry at a one-sided causal cut, not an optional convention.
LocalRecognitionHorizonCut.ofExteriorReading reuses the same constructor to build a closed local cut from any exterior-plus-seam reading in a horizon context. Together with the symmetric interior completion, this discharges the geometric premise behind PerPixelRecordAdditivity in the Bekenstein quarter plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.