sum_spike
plain-language theorem explainer
Over GF(2), the rest-region spike that places a prescribed parity bit at the distinguished free vertex and zero elsewhere sums exactly to that bit. Completions of exterior, interior, and joint readings cite it to restore global ledger closure. The proof unfolds the spike and collapses the finite sum via the standard ite-sum identity.
Claim. For every $r\in\mathbb{N}$ and every $x\in\mathbb{Z}/2\mathbb{Z}$, if $\mathrm{spike}_{r,x}$ is the configuration on $\mathrm{Fin}(r+1)$ that equals $x$ at the distinguished free vertex and $0$ elsewhere, then $\sum_p \mathrm{spike}_{r,x}(p)=x$.
background
Module HorizonOneSidedCut discharges LEG-A of the Bekenstein master plan: a horizon is a one-sided causal cut, so each side's accessible reading is a trace over the hidden side. The model is exact linear algebra over $\mathbb{Z}/2\mathbb{Z}$ on a globally closed recognition ledger (one balanced-loop parity constraint).
Vertices split into exterior private region, seam (severed-edge endpoints), interior private region, and a nonempty rest $\mathrm{Fin}(r+1)$ embedding the horizon patch in a closed universe. A configuration is closed when the total sum of all vertex bits is zero.
The spike is the elementary rest-region assignment that deposits a single free parity bit at index $0$ and zeros elsewhere. Completions of one-sided readings use it to fix global parity on the rest while tracing the hidden side to zero.
proof idea
Term-style tactic proof. Unfold the definition of the spike (pointwise ite: value $x$ at $0$, else $0$). Rewrite the finite sum by Finset.sum_ite_eq' on Finset.univ at the point $0:\mathrm{Fin}(r+1)$, which isolates the single nonzero summand. A final simp closes the equality to $x$. No external RS lemmas are required; only Mathlib finite-sum API.
why it matters
This is the parity bookkeeping step that lets one-sided readings be completed to closed configs. Downstream, compA_closed, compB_closed, and compAB_closed each reduce cutSum of the corresponding completion to zero by simp with sum_spike and a ring over $\mathbb{Z}/2\mathbb{Z}$.
Those closures feed the LEG-A argument that each side's trace independently realizes every seam bit, so summing exterior and interior double-posts the seam (Donnelly–Freidel–Geiller–Wall edge modes; RS T0 double-entry at the cut). That forces the additive $\kappa=4$ per-pixel reading rather than the joint $\kappa\to 1$ marginal, the geometric input the Bekenstein quarter-count still needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.