regularBoundaryGenus_eq_b1
plain-language theorem explainer
For any integer Betti triple of a compact 3D region, the total genus of the regular-neighborhood boundary equals the region's first Betti number. Cosmology certificates that desingularize cubical excursion-set boundaries cite this identity. The proof unfolds the genus, component, and Euler definitions and finishes by ring arithmetic.
Claim. Let $(b_0,b_1,b_2)$ be the Betti numbers of a compact 3D region. Define the region Euler characteristic $\chi = b_0 - b_1 + b_2$, the regular-neighborhood boundary component count $c = b_0 + b_2$, and the total desingularized boundary genus $g = c - \chi$. Then $g = b_1$.
background
This module supplies the algebraic bridge used by the desingularized foam-interface readout in Recognition cosmology. After raw cubical boundaries of positive excursion sets showed nonmanifold edges, the canonical object became the boundary of a regular neighborhood of the exact positive region.
A BettiTriple packages integer Betti data $(b_0,b_1,b_2)$ so Euler algebra is literal. The region Euler characteristic is $\chi = b_0 - b_1 + b_2$. Alexander-duality intuition predicts boundary components $b_0 + b_2$ and boundary Euler characteristic $2\chi$. Total genus is then defined as components minus region Euler: $g = (b_0+b_2) - \chi$.
The module status is a partial theorem through Phase 44 (conditional at Phase 47): it proves arithmetic bridges and numeric certificates, not the embedded digital-cubical homeomorphism to the geometric regular neighborhood.
proof idea
Term-mode proof by definitional expansion and ring. Unfold the three definitions: genus as components minus region Euler, components as $b_0+b_2$, and region Euler as $b_0-b_1+b_2$. The resulting integer identity $(b_0+b_2)-(b_0-b_1+b_2)=b_1$ is discharged by ring. No external lemmas are required.
why it matters
This is the core genus bridge of the regular-neighborhood boundary module: once components and Euler data match the Alexander-duality predictions, total desingularized boundary genus is forced to equal $b_1$. Downstream, components_minus_regionEuler_eq_b1 restates the same surface identity without naming genus, and genus_eq_b1_of_isRegularBoundaryOf lifts it to any boundary report satisfying the regular-neighborhood bridge predicate ("Any boundary report satisfying the regular-neighborhood bridge has genus $b_1$").
In the cosmogenesis pipeline this underwrites Phases 27–28 and the later algebraic wrappers (component assembly, polygon gluing, orientability): finite combinatorial certificates reduce to $g=b_1$ without yet proving homeomorphism of corrected cellulations to the geometric regular-neighborhood boundary. That geometric realization remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.