BettiTriple
plain-language theorem explainer
Integer triple $(b_0,b_1,b_2)$ packing the Betti numbers of a compact 3D region so Euler algebra stays exact in $\mathbb{Z}$. Cosmology bridge lemmas cite it as the algebraic carrier for regular-neighborhood boundary counts, Euler, and genus. Pure data structure: no proof obligations.
Claim. A Betti triple is an ordered triple of integers $(b_0, b_1, b_2)$ recording the Betti numbers of a compact three-dimensional region, so that the Euler characteristic is the literal integer $\chi = b_0 - b_1 + b_2$.
background
The module builds the algebraic bridge from a compact cubical 3D region to the topology of its regular-neighborhood boundary (the desingularized readout used after raw cubical boundaries showed nonmanifold edges). In that setting the region's homology is summarized by three integers: $b_0$ (components), $b_1$ (tunnels/handles), $b_2$ (voids).
Euler characteristic is then $\chi(\mathrm{region}) = b_0 - b_1 + b_2$, kept in $\mathbb{Z}$ so later identities (doubled boundary Euler, genus as components minus $\chi$) never leave integer arithmetic. Spatial dimension $D = 3$ is the ambient setting forced by the T8 forcing chain; the structure itself is dimension-agnostic data, but every consumer theorem in this file assumes the 3D regular-neighborhood story.
Downstream predicates such as component-assembly closure and component-pairing closure take a Betti triple as the region's topological fingerprint against which corrected boundary inventories are checked.
proof idea
No proof: a structure declaration with three integer fields and derived Repr / DecidableEq. It is the carrier type for all subsequent Euler and genus identities in the module.
why it matters
Every algebraic bridge in the regular-neighborhood genus program is parameterized by this triple. Parent results include the identity that boundary components minus region Euler equals $b_1$, the component-assembly and component-pairing closure predicates, and the Phase 42–44 reductions from surface-type classification and embedded component-map obligations.
The module goal is that total desingularized boundary genus equals $b_1$ once component count is $b_0+b_2$ and boundary Euler is $2\chi(\mathrm{region})$. Packing Betti data as a single value keeps those statements uniform and decidable. This is scaffolding for Phases 27–47 of the cosmogenesis foam-interface pipeline; the embedded homeomorphism from digital cubical geometry remains open, but the arithmetic carrier is fixed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.