horizonAnnulusHandle_regularBoundaryComponents
plain-language theorem explainer
The desingularized horizon-annulus handle boundary has exactly two connected components. Cosmology readers tracking the Phase-26 regular-neighborhood readout of the positive excursion set cite this numeric certificate. The proof is a one-line native decision of the arithmetic identity components = b0 + b2 on the fixed Betti triple (2,1,0).
Claim. For the horizon-annulus handle with Betti numbers $(b_0,b_1,b_2)=(2,1,0)$, the regular-neighborhood boundary component count $b_0+b_2$ equals $2$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the topology of the boundary of a regular neighborhood of the exact positive region ${q>0}$. Phase 25 saw nonmanifold edges on the raw cubical boundary of the horizon-annulus handle; Phase 26 switches to the desingularized readout.
regularBoundaryComponents is the Alexander-duality style prediction $b_0+b_2$. The horizon-annulus handle at the certified radii is frozen as the Betti triple $(2,1,0)$: two components, one tunnel, no void. Sibling formulas then give boundary Euler characteristic $2(b_0-b_1+b_2)$ and total genus equal to $b_1$.
The file proves arithmetic and numeric certificates used by the foam-interface desingularization pipeline, not the geometric realization or homeomorphism theorems (those remain open).
proof idea
Term-mode one-liner: native_decide evaluates the closed definition regularBoundaryComponents B := B.b0 + B.b2 on the concrete triple {b0 := 2, b1 := 1, b2 := 0}, reducing $2+0=2$ in the integers. No lemmas beyond the two local definitions are required.
why it matters
This is the component half of the Phase-26 horizon-annulus numeric certificate in the regular-neighborhood genus bridge (Phases 27–47). Together with the sibling Euler and genus identities, it pins the desingularized boundary as having two components and total genus one (since genus tracks $b_1=1$).
Downstream use is currently empty in the graph, but the module doc places it as input to the algebraic half of the cosmogenesis foam-interface desingularization script. It does not close the embedded digital-cubical collapse or the regular-neighborhood homeomorphism; those stay open while the arithmetic bridge and horizon/dyadic certificates are sealed with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.