halfVertexComponentDelta
plain-language theorem explainer
For one connected component of the singular-edge graph after four-face edge pairing, the Phase-30 vertex-link quotient contribution is half the component's vertex count: one vertex lift per pair of singular vertices. Cosmology and foam-interface work cites this when correcting Euler data after edge splitting. The definition is pure integer division of the recorded vertex cell count.
Claim. Given a singular-edge graph component $C$ (cell counts of vertices and edges after Phase-29 four-face edge pairing), the Phase-30 half-vertex contribution of $C$ is $\lfloor |V(C)|/2 \rfloor$ in $\mathbb{N}$, i.e. one vertex lift per pair of singular vertices in that component.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the genus of the boundary of a regular neighborhood of the exact positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to that desingularized readout; later phases supply arithmetic certificates (edge pairing, half-vertex quotient, component assembly) without yet proving geometric homeomorphism.
A SingularGraphComponent is one connected component of the singular-edge graph after the Phase-29 four-face edge pairing step. Only cell counts matter: natural numbers of vertices and edges, not an embedded geometric complex.
Phase 30's vertex-link half-quotient is the correction that pairs singular vertices so the corrected Euler characteristic can match the canonical CW Euler characteristic of the regular-neighborhood boundary.
proof idea
One-line definition: return the natural-number quotient of the component's vertex count by 2. No lemmas or tactics; integer division encodes "one vertex lift per pair of singular vertices."
why it matters
Feeds singularGraphHalfVertexDelta, which sums this contribution over a list of singular-edge components and is the total half-vertex delta used in the Phase-30 correction. The module doc states that if the raw singular boundary has already had four-face edges paired and the singular-edge components supply a half-vertex quotient equal to the missing vertex budget, then the corrected Euler characteristic equals the canonical CW Euler characteristic.
That arithmetic is part of the bridge used by the desingularized foam-interface pipeline: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus exactly $b_1$. The embedded digital-cubical collapse and regular-neighborhood homeomorphism remain open; this definition only supplies the per-component half-vertex count for those algebraic certificates (Phases 31+).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.