projSeam
plain-language theorem explainer
Extracts the seam bit-string from a cut configuration: the GF(2) assignment on the s shared endpoints of severed edges. Holography proofs cite it whenever they image closed ledgers onto seam readings. The body is a one-field product projection.
Claim. Given a cut configuration $c$ on private exterior size $a$, seam size $s$, private interior size $b$, and residual closed universe size $r+1$, write $\mathrm{proj}_{\mathrm{seam}}(c)$ for the middle factor of $c$, a map $\mathrm{Fin}\, s \to \mathbb{Z}/2\mathbb{Z}$ recording the parity bits on the severed-edge endpoints.
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 marginal ($\kappa\to 1$).
A cut configuration is a four-factor product of GF(2) assignments: exterior private vertices $\mathrm{Fin},a$, the seam $\mathrm{Fin},s$ (shared severed-edge endpoints), interior private vertices $\mathrm{Fin},b$, and a nonempty residual closed universe $\mathrm{Fin}(r+1)$. Global closure is a single balanced-loop parity constraint on the whole product. Regions $A=a\sqcup s$ and $B=s\sqcup b$ are the two sides that share the seam.
The seam projection isolates only the shared factor. Downstream statements compare images of the closed set under this map to the full function space $\mathrm{Fin},s\to\mathbb{Z}/2\mathbb{Z}$, which has cardinality $2^s$.
proof idea
Definitional one-liner: unpack the nested product type of a cut configuration and return the second factor (the seam map). No lemmas, no tactics.
why it matters
This is the projection that makes LEG-A statements speak about seam bits alone. Theorems seam_posted_by_A and seam_posted_by_B prove that the image of the closed set under this map is the full universe of seam readings, so each side privately realizes every severed-edge record. seam_card then reads off cardinality $2^s$. The package horizon_carries_one_side packages those facts into the geometric mechanism forcing double-posting of the seam (T0 double-entry at the cut) and the additive $\kappa=4$ per-pixel count in the Donnelly–Freidel–Geiller–Wall edge-mode reading.
Without a named seam projection, the double-posting identity (bits $A$ + bits $B$ = bits$(A\cup B)$ + $s$) cannot be stated as an image-cardinality comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.