regionEuler
plain-language theorem explainer
Defines the integer Euler characteristic of a compact 3D region from its Betti triple as χ = b₀ − b₁ + b₂. Cosmology and digital-topology arguments cite it whenever the regular-neighborhood boundary genus bridge needs the halved interior Euler number. The body is a one-line arithmetic abbreviation on the three Betti integers.
Claim. Given Betti data $(b_0,b_1,b_2)\in\mathbb{Z}^3$ of a compact 3D region, the region Euler characteristic is $\chi(B):=b_0-b_1+b_2$.
background
This module builds the algebraic bridge between a compact cubical 3D region and the topology of the boundary of a regular neighborhood of its exact positive set. Phase 25 saw nonmanifold edges on the raw cubical boundary; Phase 26 switches to the desingularized regular-neighborhood readout used by the foam-interface scripts.
A BettiTriple packages the three Betti numbers $(b_0,b_1,b_2)$ as integers so Euler algebra stays literal (no rationals). In classical 3-manifold topology the Euler characteristic of a compact region is $\chi=b_0-b_1+b_2$. The module then predicts that the regular-neighborhood boundary has component count $b_0+b_2$, boundary Euler $2\chi$, and total genus $b_1$.
Upstream count and neighborhood machinery (polarized interface edges, rung coarsening, recognition-lattice neighborhoods) supply the discrete regions whose Betti data feed this formula; the formula itself is pure 3D Euler algebra.
proof idea
Pure definition: return the integer $B.b0 - B.b1 + B.b2$. No lemmas, tactics, or hypotheses. Downstream theorems unfold this abbreviation when they need the halved interior Euler number.
why it matters
This is the half-Euler quantity that closes the regular-neighborhood genus bridge. The module doc states that if boundary components equal $b_0+b_2$ and boundary Euler equals $2\chi(\mathrm{region})$, then total desingularized genus is exactly $b_1$. Downstream, components_minus_regionEuler_eq_b1 rewrites genus as components minus this value; ComponentAssemblyCloses requires halfEuler = regionEuler B; and the dyadic-sponge and horizon-annulus certificates (Phases 34–39) plug concrete Betti triples into it to force corrected-component Euler sums, polygon-gluing closure, oriented gluing, and surface-type classification.
It does not touch the T0–T8 forcing chain or RCL directly; it is the arithmetic spine of the cosmogenesis foam-interface desingularization (Phases 27–47). The embedded digital-cubical collapse and the homeomorphism of corrected cellulations to true regular-neighborhood components remain open; this definition only supplies the integer $\chi$ those certificates compare against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.