regularBoundaryComponents
plain-language theorem explainer
For a compact 3D region with Betti numbers $(b_0,b_1,b_2)$, the predicted number of connected components of the regular-neighborhood boundary is $b_0+b_2$. Cosmology and digital-topology work cite this as the Alexander-duality component count feeding the desingularized genus bridge. The definition is a one-line sum of the zeroth and second Betti numbers.
Claim. Given Betti data $(b_0,b_1,b_2)\in\mathbb{Z}^3$ of a compact 3D region, the regular-neighborhood boundary component count is $b_0+b_2$.
background
This module builds the algebraic bridge between a compact 3D cubical region's Betti triple and the topology of the boundary of a regular neighborhood of the exact positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to that desingularized readout.
A BettiTriple packages integer Betti numbers $(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 for a compact region in 3-space predicts that the regular-neighborhood boundary has as many components as $b_0+b_2$, and doubled Euler characteristic $2\chi$.
The surrounding bridge then sets total boundary genus equal to components minus $\chi(\mathrm{region})$, which collapses to $b_1$. This definition is the component half of that dictionary, used by the foam-interface desingularization pipeline.
proof idea
Pure definition: return the sum of the zeroth and second integer Betti fields of the triple. No lemmas, tactics, or hypotheses.
why it matters
This is the component slot in the regular-neighborhood genus bridge: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, genus $=$ components $-\chi(\mathrm{region})$, hence total genus $b_1$. Downstream, components_minus_regionEuler_eq_b1 and the genus-equals-$b_1$ theorem use it directly; ComponentAssemblyCloses and ComponentPairingCloses require corrected or classified component counts to match it; Phase-42 inventory theorems and the dyadic sponge R20 certificates (corrected component count 53, componentwise surface inventory) pin numeric witnesses against this value.
It does not close the geometric homeomorphism from digital cubical collapse or polygon gluings to the actual regular-neighborhood boundary; those remain open geometric premises. In the Recognition cosmology stack it is bookkeeping for the desingularized foam interface, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.