singularGraphHalfVertexDelta
plain-language theorem explainer
Sums the Phase-30 half-vertex quotient over every singular-edge component after Phase-29 four-face pairing. Each component contributes floor of its vertex count over two; the total is the missing vertex budget that corrects the edge-only Euler count. Cosmology certificates for the horizon annulus and dyadic sponge cite it, and the half-vertex corrected Euler definition is built from it. The body is a one-line map-and-sum.
Claim. Given a finite list of singular-edge graph components (each recorded by vertex and edge cell counts after four-face edge pairing), the total half-vertex delta is $\sum_i \lfloor v_i/2\rfloor$, where $v_i$ is the vertex count of the $i$-th component.
background
This module builds the algebraic bridge for the regular-neighborhood boundary of a compact 3D cubical positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to the desingularized readout: the boundary of a regular neighborhood of ${q>0}$. The target identities are boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus exactly $b_1$.
A SingularGraphComponent is one connected component of the singular-edge graph after Phase-29 four-face edge pairing; only cell counts are stored, not an embedded geometry. The per-component Phase-30 contribution is the vertex-link half-quotient: one vertex lift per pair of singular vertices, written $v/2$ in natural numbers. The present definition aggregates those contributions over a list of components.
Phase 31 uses that total as the additive correction that turns an edge-only Euler count into a candidate for the canonical regular-boundary CW Euler characteristic.
proof idea
Definitional one-liner: map each component through the per-component half-vertex delta $v\mapsto v/2$, then sum the resulting natural numbers. No lemmas or tactics; the meaning is entirely the sum of the upstream component-wise quotients.
why it matters
This is the Phase-30 aggregate that feeds the corrected Euler characteristic: edge-only Euler plus this delta. Downstream, halfVertexCorrectedEuler is defined by that sum, and the algebraic bridge theorem states that if the delta equals the missing vertex budget, the corrected count matches the canonical CW Euler of the Betti triple.
Numeric certificates close the budget on concrete foams: the horizon-annulus handle supplies exactly 64, recovering CW Euler 2 from edge-only $-62$; the dyadic sponge R20 supplies 66, recovering $-144$ from $-210$. Those equalities are the arithmetic half of Phases 30–31.
The geometric realization (embedded digital-cubical collapse to the true regular-neighborhood boundary) remains open; this object only packages the vertex-budget arithmetic used by the cosmogenesis desingularized interface script.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.