horizonAnnulusHandle_correctedComponentCount
plain-language theorem explainer
The Phase-34 horizon-annulus handle has corrected boundary component count equal to the regular-neighborhood prediction b0+b2 from its Betti triple. Both sides equal 2: one torus plus one sphere versus (b0,b1,b2)=(2,1,0). Anyone auditing the desingularized foam-interface certificate for this handle cites this equality. The proof is a one-line native_decide on the finite list length and integer sum.
Claim. For the horizon-annulus handle, the number of corrected boundary components equals the regular-neighborhood component count $b_0+b_2$ of its Betti triple $(b_0,b_1,b_2)=(2,1,0)$. Explicitly both sides equal $2$ (one torus component and one sphere component).
background
This module builds the algebraic bridge between a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ 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 horizon surface, Phase 26 switched to that desingularized readout. The predicted boundary component count is $b_0+b_2$, the boundary Euler characteristic is $2(b_0-b_1+b_2)$, and the total desingularized genus collapses to $b_1$.
The horizon-annulus handle at the Phase-26 radii is certified with Betti data $(2,1,0)$: two components, one tunnel, no void. Phase-34 supplies the corrected edge-paired face components as an explicit list: one torus component and one sphere component. The corrected component count is simply the length of that list; the regular-neighborhood prediction is $b_0+b_2$.
Phase 35 then uses matching component count and Euler half-sum to force total genus $b_1$. This file still proves only the arithmetic certificates, not homeomorphism of the corrected cellulations to the true regular-neighborhood boundary.
proof idea
Both sides are closed integer expressions built from concrete definitions. The left-hand side is the length of the two-element list [torusComponent, sphereComponent]. The right-hand side is $2+0$ from the fixed Betti triple. native_decide evaluates the equality in the kernel; no lemmas are invoked beyond definitional unfolding of correctedComponentCount and regularBoundaryComponents.
why it matters
Phase 35's component-assembly bridge needs the corrected face components to carry the canonical component count before it can force total genus equal to $b_1$. This theorem discharges that count gate for the horizon-annulus handle: two corrected components match $b_0+b_2=2$. The module doc frames Phase 35 as the algebraic half of the Phase-34 assembly; the geometric realization (homeomorphism of corrected cellulations to regular-neighborhood components) remains open, as does the embedded digital-cubical collapse.
No downstream theorem currently depends on this declaration in the graph, so it sits as a numeric certificate inside the Phase-34/35 horizon package rather than a shared lemma. It is one of the finite combinatorial checks that keep the cosmogenesis foam-interface script's desingularized readout consistent with Alexander-duality intuition for this handle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.