closedSet
plain-language theorem explainer
The closed-configuration set is the Finset of all cut-ledger assignments (exterior private, seam, interior private, rest-of-universe) whose total GF(2) parity is balanced. Every LEG-A marginal, capacity, and double-posting identity is computed by projecting this set. The body is a one-line filter of the universe by the closedness predicate.
Claim. For natural numbers $a,s,b,r$, write $\mathrm{CutCfg}(a,s,b,r)$ for the product of GF(2)-valued assignments on the exterior private vertices $\mathrm{Fin}\,a$, the seam $\mathrm{Fin}\,s$, the interior private vertices $\mathrm{Fin}\,b$, and the nonempty rest factor $\mathrm{Fin}(r+1)$. The closed-configuration set is the finite subset of those assignments that satisfy the global balanced-loop (closed) parity constraint.
background
Module HorizonOneSidedCut discharges LEG-A of the Bekenstein master plan: a one-sided causal cut forces private duplicated edge records, so horizon entropy is the sum of per-side traced marginals ($\kappa=4$) rather than the joint marginal ($\kappa\to 1$).
A configuration is a four-factor GF(2) ledger on vertices split by the cut: exterior private $a$, shared seam $s$, interior private $b$, and a nonempty rest-of-universe factor $r+1$ that can absorb parity. The two pixels are region $A=a\sqcup s$ and $B=s\sqcup b$. Closedness is the single global balanced-loop parity constraint on the whole product.
The closed-configuration set is the ambient sample space for every subsequent image, card, and log2-bit count (seam projections, side marginals, joint $AB$ marginal).
proof idea
Definitional one-liner: take the finite universe of all cut configurations and retain those satisfying the closedness predicate. No lemmas are applied; the filter is the entire content.
why it matters
This set is the carrier for the whole LEG-A argument. Downstream, HorizonSumsPerSide defines the one-sided-cut premise as equality of the horizon record with the sum of log2-cards of the two side images of this set; horizon_record_double_posts_seam then derives that the record exceeds the joint $AB$ marginal by exactly the seam bit count. The bundled target horizon_carries_one_side packages surjectivity onto the seam, the seam-identity, and the physical domino face ($a=s=b=2$) where each pixel marginal has 4 bits ($\kappa=4$) and face capacity $16$.
In RS terms this is T0 double-entry at the cut, matching the Donnelly–Freidel–Geiller–Wall edge-mode prescription: each side posts its own copy of the severed edges, forced by causal one-sidedness rather than assumed as PerPixelRecordAdditivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.