halfVertexCorrectedEuler
plain-language theorem explainer
Defines the Phase-30 corrected Euler characteristic of a singular cubical boundary: edge-only Euler plus the total half-vertex delta from singular-edge components. Cosmology bridge proofs cite it to match the canonical regular-neighborhood CW Euler. The body is a one-line integer sum.
Claim. Given an edge-only Euler characteristic $E_{\mathrm{edge}}\in\mathbb{Z}$ and a finite list $C$ of singular-edge graph components (each a pair of vertex and edge counts after Phase-29 four-face edge pairing), the half-vertex-corrected Euler characteristic is $E_{\mathrm{edge}}+\Delta_{1/2}(C)$, where $\Delta_{1/2}(C)$ is the sum of the Phase-30 half-vertex contributions over components of $C$.
background
This module builds the algebraic bridge from raw cubical excursion-set boundaries to the desingularized regular-neighborhood boundary used in cosmogenesis foam readout. Phase 25 saw nonmanifold edges on the raw horizon-annulus handle; Phase 26 switches to the boundary of a regular neighborhood of ${q>0}$. For a compact 3D cubical region with Betti triple $(b_0,b_1,b_2)$, the regular-neighborhood boundary is expected to have $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
A SingularGraphComponent records only cell counts (vertices, edges) of one connected component of the singular-edge graph after Phase-29 four-face edge pairing; it is not yet an embedded geometric object. The sibling singularGraphHalfVertexDelta sums the Phase-30 vertex-link half-quotient contribution over a list of such components (one vertex lift per pair of singular vertices in each component). The present definition packages the corrected raw-boundary Euler as edge-only Euler plus that total delta.
proof idea
Definitional one-liner: return the integer sum of the supplied edge-only Euler characteristic and singularGraphHalfVertexDelta applied to the component list. No lemmas or tactics; the arithmetic content lives in the half-vertex delta and in downstream equality certificates.
why it matters
Phase 31 needs a single corrected Euler object so that the half-vertex quotient can be stated as equality with the Phase-28 canonical regular-boundary CW Euler. Downstream, HalfVertexQuotientCloses is exactly that equality predicate, and halfVertexCorrectedEuler_eq_cw_of_delta_eq_required is the algebraic bridge: if the half-vertex delta equals the missing vertex budget and the budgeted sum matches the CW Euler of the Betti triple, the quotient closes.
Numeric certificates instantiate it: horizonAnnulusHandle_halfVertexCorrectedEuler shows $-62+64=2$ recovers the handle CW Euler; dyadicSpongeR20_halfVertexCorrectedEuler shows $-210+66=-144$ for the dyadic sponge. The module status remains partial through Phase 44: this is the arithmetic bridge and certificate layer, not the embedded digital-cubical collapse or homeomorphism to the regular-neighborhood boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.