HalfVertexQuotientCloses
plain-language theorem explainer
The half-vertex quotient closes when the Phase-30 corrected edge-paired Euler characteristic equals the canonical Phase-28 regular-boundary CW Euler of a compact 3D region. Cosmologists on the desingularized foam-interface pipeline cite this predicate as the Phase-31 algebraic gate. It is a pure equality proposition on integer Euler data, not a geometric theorem. Downstream numeric certificates discharge it by `native_decide`.
Claim. For a Betti triple $B=(b_0,b_1,b_2)$ of a compact 3D region, an edge-only Euler integer $E$, and a list $C$ of singular-graph components (each a pair of vertex and edge counts after four-face edge pairing), the half-vertex quotient closes when $\chi_{\mathrm{corr}}(E,C)=\chi_{\mathrm{CW}}(B)$, where $\chi_{\mathrm{corr}}$ is $E$ plus the half-vertex delta of $C$, and $\chi_{\mathrm{CW}}$ is the canonical regular-boundary CW Euler characteristic built from $B$.
background
This module builds the algebraic genus bridge for the regular-neighborhood boundary of a compact 3D cubical region. After Phase 25 found nonmanifold edges on the raw positive-excursion surface, Phase 26 switched to the desingularized readout: the boundary of a regular neighborhood of the exact positive region. The Betti triple records integer Betti numbers $(b_0,b_1,b_2)$ so Euler algebra is literal; the region Euler is $\chi=b_0-b_1+b_2$, and the canonical regular-boundary CW Euler is assembled from the corresponding CW vertex, edge, and face counts.
Phase 29 pairs four-face singular edges. Each connected component of the resulting singular-edge graph is recorded only as cell counts (vertices and edges), not as an embedded geometric object. Phase 30 then applies a half-vertex quotient: one vertex lift per pair of singular vertices in each component. The corrected Euler is the edge-only Euler plus that half-vertex delta.
The local setting is explicitly partial: the file proves arithmetic bridges and numeric certificates for horizon and dyadic examples, not the embedded digital-cubical collapse or the final homeomorphism to the regular-neighborhood boundary.
proof idea
Definitional equality, not a tactic proof. The predicate is the proposition that the half-vertex-corrected Euler (edge-only Euler plus the singular-graph half-vertex delta) equals the canonical regular-boundary CW Euler of the given Betti triple. Downstream theorems either unfold the predicate and decide the integer equality, or reduce to it by showing the half-vertex delta equals a required missing-vertex budget and that the budgeted sum matches the CW Euler.
why it matters
This is the Phase-31 algebraic gate named in the module doc: once four-face edges are paired and the singular components supply a half-vertex quotient equal to the missing vertex budget, the corrected Euler matches the Phase-28 CW Euler. It is the target proposition of the general bridge theorem that, given a matching half-vertex delta and budget identity, concludes the quotient closes.
Two concrete certificates use it: the horizon-annulus handle and the dyadic-sponge R20 examples each assert the predicate on their recorded Betti data, edge-only Euler, and singular-component lists, discharging by native decision. Those certificates sit inside the broader regular-neighborhood genus program, whose end goal is that total desingularized boundary genus equals the region's first Betti number $b_1$. The geometric realization and homeomorphism steps remain open; this definition only packages the arithmetic closing condition those later steps will need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.