correctedComponentGenus_eq_b1_of_componentAssemblyCloses
plain-language theorem explainer
Once a list of corrected boundary components has the canonical component count and Euler half-sum of a compact 3D region, the total component genus equals the region's first Betti number b₁. Cosmology and digital-topology workers cite this as the Phase-34 algebraic bridge between edge-paired face components and regular-neighborhood genus. The proof unpacks the assembly hypothesis and rewrites to the Euler-form surface identity components − χ(region) = b₁.
Claim. Let $B=(b_0,b_1,b_2)$ be the Betti triple of a compact 3D region, let $C_s$ be a finite list of corrected boundary components (each recorded by its Euler characteristic), and let $h\in\mathbb{Z}$ be a half-Euler value. If the corrected component count equals the regular-neighborhood component count $b_0+b_2$, the total corrected Euler characteristic equals $2h$, and $h$ equals the region Euler characteristic $\chi(B)=b_0-b_1+b_2$, then the corrected component genus $\#C_s - h$ equals $b_1$.
background
This module builds the algebraic bridge used by the desingularized foam-interface readout. 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. For a compact 3D cubical region with Betti triple $(b_0,b_1,b_2)$, that boundary is expected to have $b_0+b_2$ components and Euler characteristic $2(b_0-b_1+b_2)$, so genus computed as components minus region Euler is exactly $b_1$.
A BettiTriple stores integer Betti numbers so Euler algebra is literal; region Euler is $\chi=b_0-b_1+b_2$. Each CorrectedBoundaryComponent is a post edge-pairing, vertex-link-collapse piece recorded only by its Euler number. The predicate ComponentAssemblyCloses asserts three equalities: corrected component count matches the regular-neighborhood count, total corrected Euler equals twice a supplied half-Euler, and that half-Euler equals region Euler.
Upstream, components_minus_regionEuler_eq_b1 is the Euler-form surface identity: components minus $\chi(\mathrm{region})$ equals $b_1$, obtained from the doubled-boundary genus theorem without integer division. The genus readout correctedComponentGenusFromHalfEuler is simply component count minus the explicit half-Euler.
proof idea
Term-mode unpack of the assembly hypothesis. Destructure ComponentAssemblyCloses into the three conjuncts (component-count match, doubled-Euler match, and half-Euler equals region Euler). Unfold the genus definition correctedComponentGenusFromHalfEuler (count minus half-Euler). Rewrite by the count and half-Euler equalities, then apply components_minus_regionEuler_eq_b1, which states regularBoundaryComponents B - regionEuler B = B.b1.
why it matters
Phase 35 of the regular-neighborhood boundary program: the algebraic half of the Phase-34 component-assembly certificate. It forces total desingularized boundary genus to equal $b_1$ whenever corrected edge-paired face components carry the canonical count and Euler half-sum, without yet proving homeomorphism of those cellulations to the true regular-neighborhood components.
Downstream, polygonGluedGenus_eq_b1_of_polygonGluingCloses (Phase 36/37) reduces finite polygon gluing with binary edge pairing and cyclic vertex links to this theorem, so the polygon-gluing genus bridge inherits the same $b_1$ identity. Later orientability wrappers (Phase 39) sit on that chain. The geometric realization and embedded digital-cubical collapse remain open; this file only closes the arithmetic bridge and numeric certificates used by the cosmogenesis desingularization scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.