regularBoundaryCWEuler
plain-language theorem explainer
Euler characteristic of the canonical CW model for a desingularized regular-neighborhood boundary, read from a compact 3D region's Betti triple. Horizon-annulus and dyadic-sponge Phase-28 certificates cite it as the target χ value that half-vertex corrections must match. Pure cell-count formula: one vertex and face per boundary component, 2b₁ edges, then V−E+F.
Claim. For a compact 3D region with integer Betti numbers $(b_0,b_1,b_2)$, the Euler characteristic of the canonical regular-boundary CW model is $V-E+F$, where $V=F=b_0+b_2$ (one 0-cell and one 2-cell per boundary component) and $E=2b_1$.
background
Phase 25 measured the raw cubical boundary of the positive excursion set and found nonmanifold edges. The module therefore switches to the boundary of a regular neighborhood of the exact positive region. The algebraic bridge used by the foam-interface desingularization scripts asserts: components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus exactly $b_1$.
A Betti triple packages $(b_0,b_1,b_2)$ as integers so Euler algebra is literal. The sibling cell counts define a topological CW model: vertices and faces equal the component count; edges equal $2b_1$, carrying the total handle rank. Upstream docs stress this is the Phase-28 cell-count model, not an embedded cubical sheet-splitting construction.
proof idea
Definitional abbreviation composing three sibling cell-count defs: vertices minus edges plus faces. Vertices and faces both equal the regular-boundary component count $b_0+b_2$; edges equal $2b_1$. No tactics or lemmas; pure arithmetic of those three quantities.
why it matters
Supplies the Phase-28 target Euler that numeric certificates evaluate: horizon-annulus handle gives $\chi=2$; dyadic sponge R20 gives $\chi=-144=2(50-125+3)$. Downstream, the half-vertex quotient closes precisely when the corrected edge-paired Euler equals this CW value, and the algebraic bridge theorem discharges that predicate once the half-vertex delta matches the missing vertex budget.
Equality lemmas also identify this CW Euler with the plain regular-boundary Euler and with twice the region Euler $\chi=b_0-b_1+b_2$, feeding the genus bridge (total desingularized genus $=b_1$). The embedded digital-cubical collapse and homeomorphism to the geometric regular neighborhood remain open; this definition is only the arithmetic side of that bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.