HorizonSumsPerSide
plain-language theorem explainer
Encodes the sole physical premise of LEG-A: a horizon record equals the sum of the two one-sided accessible marginal bit-counts (exterior plus interior), not their joint. Anyone citing the κ=4 double-posting argument or the Bekenstein master-plan cut uses this predicate. It is a bare Prop definition equating the record to log₂ of the projected closed-set cardinalities on each side.
Claim. For $a,s,b,r,H\in\mathbb{N}$, the one-sided-cut premise holds when $H=\log_2|\pi_A(C)|+\log_2|\pi_B(C)|$, where $C$ is the set of globally closed ledger configurations on the cut $(a,s,b,r)$ and $\pi_A,\pi_B$ are the projections onto the exterior side $A=a\sqcup s$ and interior side $B=s\sqcup b$.
background
Module HorizonOneSidedCut discharges LEG-A of the Bekenstein quarter master plan: the geometric input that forces the additive κ=4 per-pixel count. A recognition ledger is split into exterior private vertices (size $a$), seam (size $s$), interior private vertices (size $b$), and a nonempty rest ($r+1$). Regions are $A=a\sqcup s$ and $B=s\sqcup b$. The closed configuration set is the kernel of the global balanced-loop parity constraint over $\mathbb{Z}/2\mathbb{Z}$.
A horizon is modeled as a one-sided causal cut: the exterior observer cannot condition on the hidden interior, so the accessible reading is a trace, not a joint. Each side therefore posts its own private record of the severed edges. The bit-count of a marginal is $\mathrm{Nat.log2}$ of the cardinality of the projected closed set. This definition packages that sum-of-marginals reading as a Prop on the horizon record $H$.
It is strictly weaker than per-pixel record additivity; additivity is derived later via the seam identity, not assumed here.
proof idea
Definitional Prop, not a proved theorem. The body is a single equality: the horizon record parameter equals the sum of $\mathrm{Nat.log2}$ of the image-cardinalities of the closed configuration set under the two side projections. No tactics, no lemmas applied; it names the physical input that downstream theorems consume.
why it matters
This is the named one-sided-cut premise that LEG-A isolates. Downstream, horizon_record_double_posts_seam rewrites through it and applies the seam identity to conclude $H=\log_2|\pi_{AB}(C)|+s$: the record exceeds the joint boundary marginal by exactly the seam bit count. That is the additive (κ=4) reading forced by causal one-sidedness rather than chosen.
It also appears as conjunct (4) inside the bundled LEG-A statement horizon_carries_one_side, which packages seam surjectivity, full private seam copies on each side, the double-posting identity, and the physical domino face (seam $=2$, each pixel marginal $=4$). LocalHorizonContext carries it as the oneSided field, joining the cut model to near-horizon rate data without thermality or curvature premises.
In RS terms this is T0 double-entry at the cut (Donnelly–Freidel–Geiller–Wall edge modes): shared edges are posted twice, once per side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.