regularBoundaryCWEuler_eq_regularBoundaryEuler
plain-language theorem explainer
For any integer Betti triple of a compact 3D region, the Euler characteristic built from the canonical CW cell counts of the regular-neighborhood boundary equals the abstract regular-boundary Euler characteristic. Foam-interface and desingularized-boundary arguments in the cosmogenesis pipeline cite it as the algebraic identification of the two Phase-28 readouts. The proof unfolds both expressions into Betti polynomials and closes by ring.
Claim. Let $(b_0,b_1,b_2)\in\mathbb{Z}^3$ be the Betti data of a compact 3D region. The Euler characteristic of the canonical CW model of its regular-neighborhood boundary equals the abstract regular-boundary Euler characteristic of that triple (both equal $2(b_0-b_1+b_2)$ once the sibling doubled-Euler law is applied).
background
This module is the algebraic bridge for the desingularized regular-neighborhood boundary of a positive cubical excursion set. After Phase 25 found nonmanifold edges on the raw cubical surface, Phase 26 switched to the boundary of a regular neighborhood; Phases 27–28 encode the predicted topology in integer Betti data.
A BettiTriple is simply $(b_0,b_1,b_2)\in\mathbb{Z}^3$. Region Euler is $\chi(\mathrm{region})=b_0-b_1+b_2$. Alexander-duality intuition supplies boundary component count $b_0+b_2$ and boundary Euler $2\chi(\mathrm{region})$. The canonical CW model assigns integer cell counts (vertices, edges $2b_1$, faces) whose alternating sum is the CW Euler characteristic.
The present statement identifies that CW alternating sum with the abstract regular-boundary Euler functional, before the next lemma expands the latter as $2\chi(\mathrm{region})$.
proof idea
Term-mode proof by definitional expansion. Unfold the CW Euler characteristic into its vertex, edge, and face counts; unfold the abstract regular-boundary Euler into components and region Euler; then apply ring on the resulting integer polynomial identity in $b_0,b_1,b_2$. No external lemmas are required beyond the local definitions.
why it matters
Closes the first half of the Phase-28 doubled-Euler law for the canonical CW boundary model. The immediate parent is regularBoundaryCWEuler_eq_two_regionEuler, whose doc-comment states the CW model has Euler characteristic $2\chi(\mathrm{region})$ in expanded form; that parent rewrites through this equality and the sibling regularBoundaryEuler_eq_two_regionEuler.
In the broader bridge, boundary components $b_0+b_2$, doubled Euler $2\chi(\mathrm{region})$, and genus $b_1$ are the arithmetic inputs to the foam-interface desingularization scripts. The module status remains partial through Phase 44 and conditional at Phase 47: this file proves the arithmetic bridge and numeric certificates, not the embedded digital-cubical collapse or the homeomorphism of corrected cellulations to the true regular-neighborhood boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.