torusComponent
plain-language theorem explainer
A corrected boundary component with Euler characteristic 0, the algebraic stand-in for a torus after edge pairing and vertex-link collapse. Cosmology certificates that assemble horizon-annulus handle topology cite it as the non-spherical piece. The body is a one-field structure literal.
Claim. The torus corrected-boundary component is the connected component whose Euler characteristic is $\chi = 0$ (genus $1$ when closed and orientable).
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 its regular-neighborhood boundary: component count $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus $b_1$. Phase 25 found nonmanifold edges on the raw cubical boundary of ${q>0}$; later phases switch to the desingularized readout and prove only the arithmetic certificates, not geometric homeomorphism.
A CorrectedBoundaryComponent is one connected piece of that corrected boundary after edge pairing and local vertex-link collapse. It is represented solely by an integer Euler characteristic. For a closed orientable surface, $\chi=2-2g$, so $\chi=0$ is the torus ($g=1$).
proof idea
Definitional constructor only: pack the integer field euler := 0 into the CorrectedBoundaryComponent structure. No lemmas or tactics.
why it matters
Feeds horizonAnnulusHandleCorrectedComponents, the Phase-34 list for the horizon-annulus target: one torus plus one sphere. That list is the corrected-component input to the Phase-35 assembly bridge, which forces total genus $b_1$ once component count and Euler half-sum match the canonical data.
In the cosmogenesis foam-interface pipeline this is the non-spherical handle piece of the desingularized horizon annulus. It does not close the still-open embedded digital-cubical collapse or regular-neighborhood homeomorphism theorems; it only supplies the Euler datum those algebraic wrappers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.