regularBoundaryGenus
plain-language theorem explainer
Defines the total genus of the desingularized regular-neighborhood boundary of a compact 3D region from its Betti triple: boundary component count minus the region's Euler characteristic. Cosmology and topology workers on the Phase-28 foam-interface certificates cite it as the algebraic genus readout. The body is a one-line integer difference of two combinatorial counts, arranged so the doubled-boundary identity forces genus equal to the first Betti number.
Claim. For a compact 3D region with integer Betti triple $(b_0,b_1,b_2)$, the total genus of its regular-neighborhood boundary is $g := (b_0+b_2) - (b_0-b_1+b_2)$, that is, the predicted boundary component count minus the region's Euler characteristic $\chi = b_0-b_1+b_2$.
background
This module builds the algebraic bridge for the desingularized regular-neighborhood boundary of a compact cubical 3D region (Phases 27–28 and later wrappers). After Phase 25 found nonmanifold edges on the raw cubical boundary of ${q>0}$, Phase 26 switched to the boundary of a regular neighborhood of the exact positive region as the canonical readout.
A BettiTriple packages integer Betti numbers $(b_0,b_1,b_2)$ so Euler algebra is literal. The region's Euler characteristic is $\chi = b_0-b_1+b_2$. Alexander-duality intuition supplies the boundary component count $b_0+b_2$ and the doubled-boundary law $\chi(\partial)=2\chi(\mathrm{region})$. Genus is then read as components minus $\chi(\mathrm{region})$, matching the classical closed-surface formula once the doubling is built in.
The module proves only the arithmetic bridge and numeric certificates (horizon annulus, dyadic sponge). Geometric realization of the digital-cubical collapse remains open.
proof idea
Pure definition: subtract the region's Euler characteristic from the predicted regular-boundary component count. Unfolding gives $(b_0+b_2)-(b_0-b_1+b_2)$, which ring-simplifies to $b_1$ in the companion equality theorem. No tactics beyond the defining expression.
why it matters
This is the genus readout used throughout the regular-neighborhood bridge. The parent theorem states that once components and Euler data are identified with the canonical formulas, total desingularized boundary genus equals the region's first Betti number $b_1$. An equivalent form writes the same identity as components minus $\chi(\mathrm{region})$ without division.
Downstream, the geometry-facing predicate IsRegularBoundaryOf records a boundary report whose genus field is forced to match this definition. Concrete certificates evaluate it by native decision: the horizon-annulus handle has genus one, and the dyadic sponge at R20 has genus 125. Those numeric facts feed the Phase-28 CW cell-count model (one 0-cell and one 2-cell per component, $2b_1$ one-cells) behind the cosmogenesis foam-interface scripts.
In the broader RS cosmology stack this closes the algebraic half of the desingularized boundary story; homeomorphism of corrected cubical cellulations to the true regular-neighborhood boundary remains the open geometric step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.