projAB
plain-language theorem explainer
The joint-boundary projection of a cut configuration keeps only the exterior-private, seam, and interior-private GF(2) bit strings, discarding the rest-of-universe block. Anyone counting horizon marginals or proving the double-posting identity cites it as the map whose image is the joint (A∪B) support. The body is a three-component product projection from the four-block CutCfg tuple.
Claim. Given a cut configuration $c$ on sizes $(a,s,b,r)$ (exterior-private $a$, seam $s$, interior-private $b$, and nonempty rest $r+1$), the joint-boundary projection returns the triple of bit assignments $(c_A, c_S, c_B) \in (\mathbb{F}_2^a) \times (\mathbb{F}_2^s) \times (\mathbb{F}_2^b)$, dropping the rest-of-universe block.
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-pixel traced marginals ($\kappa = 4$) rather than the joint ($\kappa \to 1$). The model is exact linear algebra over $\mathbb{Z}/2\mathbb{Z}$ on a globally closed recognition ledger.
A configuration CutCfg a s b r is a 4-tuple of bit maps: exterior-private vertices $\mathrm{Fin},a$, seam $\mathrm{Fin},s$ (severed-edge endpoints shared by both sides), interior-private $\mathrm{Fin},b$, and the rest of the closed universe $\mathrm{Fin}(r+1)$ (nonempty). Regions are $A = a \sqcup s$ and $B = s \sqcup b$. The joint boundary is the three-block support $A \cup B = a \sqcup s \sqcup b$; this definition is the corresponding coordinate projection.
Upstream, the only structural dependency is the CutCfg abbreviation itself. The physical reading is the Donnelly–Freidel–Geiller–Wall edge-mode prescription, phrased in RS as T0 double-entry at the cut.
proof idea
Pure definitional projection. If $c = (g_A, g_S, g_B, g_R)$, the value is $(g_A, g_S, g_B)$. No lemmas, no tactics: a three-field product destructor on the nested product type of CutCfg.
why it matters
This map is the joint-boundary marginal used throughout LEG-A. Downstream, margAB_image_univ shows its image on the closed set is all of $\mathbb{F}_2^{a+s+b}$; margAB_card and margAB_bits then give cardinality $2^{a+s+b}$ and bit count $a+s+b$. Those feed seam_identity: bits$(A)+$bits$(B)=$bits$(A\cup B)+s$, the symbolic double-posting identity.
horizon_record_double_posts_seam rewrites the horizon record as the joint bit count plus $s$, and the package proposition horizon_carries_one_side bundles the full LEG-A claim (private seam copies on each side, double-posting, physical seam $=2$, $\kappa=4$). A sibling module uses it in horizonRecord_eq_joint_plus_seam. Without this projection there is no joint side of the $\kappa=4$ vs $\kappa\to 1$ fork.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.