projA
plain-language theorem explainer
Projects a globally closed cut configuration onto the exterior-side accessible bits: the exterior-private vertices together with the seam. Anyone counting exterior marginal capacity or proving double-posting of severed edges cites this map. The body is the product projection that discards interior-private and remainder coordinates.
Claim. Given a cut configuration $c$ on exterior-private size $a$, seam size $s$, interior-private size $b$, and nonempty remainder $r+1$, the exterior accessible marginal $\mathrm{proj}_A(c)$ is the pair of bit-strings consisting of the exterior-private coordinates and the seam coordinates (values in $\mathbb{Z}/2\mathbb{Z}$), discarding the interior-private and remainder coordinates.
background
The module formalizes LEG-A of the Bekenstein master plan: a horizon as a one-sided causal cut forces privately duplicated edge records, so per-pixel entropy sums rather than joints and yields $\kappa=4$. Configurations live in exact GF(2) linear algebra on a globally closed recognition ledger.
A cut configuration splits the vertex set into four blocks: exterior-private $\mathrm{Fin},a$, seam $\mathrm{Fin},s$ (severed-edge endpoints shared by both sides), interior-private $\mathrm{Fin},b$, and a nonempty remainder $\mathrm{Fin}(r+1)$. Region $A$ is exterior-private plus seam; region $B$ is seam plus interior-private. The exterior observer cannot condition on the causally hidden interior, so the accessible reading is the trace over interior and remainder.
This projection is that exterior reading: keep exterior-private and seam bits, drop the rest. Downstream cardinality and bit-count theorems treat the image of the closed-configuration set under this map as the exterior-side support.
proof idea
Definitional one-liner. A cut configuration is a 4-fold product of bit-string spaces; the map returns the first factor paired with the first component of the remaining triple, i.e. exterior-private $\times$ seam. No lemmas or tactics.
why it matters
This is the exterior half of the one-sided-cut bookkeeping that forces LEG-A. Downstream, the image of the closed set under this projection has full capacity $2^{a+s}$ (margA_card, margA_bits), so at the physical domino face ($a=s=2$) one gets $\kappa=4$ bits per pixel (kappa_per_pixel_is_four, domino_face_capacity).
It enters the one-sided-cut premise HorizonSumsPerSide (horizon record equals sum of exterior and interior accessible bit counts) and the bundled certificate horizon_carries_one_side, which packages full seam realization on each side, the seam double-posting identity, and $\kappa=4$. Together with the interior projection and seam_identity, summing the two sides exceeds the joint marginal by exactly the seam bit count: the additive Donnelly–Freidel–Geiller–Wall / T0 double-entry reading, forced by causal one-sidedness rather than postulated as PerPixelRecordAdditivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.