horizonAnnulusHandleCorrectedComponents
plain-language theorem explainer
Lists the Phase-34 corrected boundary components of the horizon-annulus handle as one torus and one sphere. Cosmology certificates that check component count, Euler sum, and genus against the regular-neighborhood bridge cite this list. The body is a two-element literal built from the standard sphere and torus component constructors.
Claim. The corrected boundary of the horizon-annulus handle, after edge pairing and local vertex-link collapse, is the two-component list consisting of one torus ($\chi=0$) and one sphere ($\chi=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 positive excursion set. After desingularization, the boundary has $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
A corrected boundary component is recorded only by its Euler characteristic. The sphere constructor is the component with $\chi=2$; the torus constructor is the component with $\chi=0$. Phase 34 supplies concrete component lists for numeric targets (horizon annulus and dyadic sponge) so that Phase-35 assembly theorems can check count, Euler half-sum, and genus by pure arithmetic.
proof idea
Definitional literal: the list is exactly the torus component followed by the sphere component. No proof obligations; the constructors already fix $\chi=0$ and $\chi=2$.
why it matters
Feeds the four Phase-34/35 horizon certificates: component count equals the regular-boundary component count from the Betti data; total corrected Euler equals twice the region Euler; the component-assembly predicate closes; and the half-Euler genus formula returns total genus one. Those theorems are the algebraic half of the horizon-annulus handle story in the cosmogenesis foam interface. They do not yet prove homeomorphism of the corrected cellulations to the geometric regular-neighborhood boundary; that geometric realization remains open per the module status through Phase 47.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.