horizonAnnulusHandlePolygonComponents
plain-language theorem explainer
Packages the two Phase-36 horizon polygon-glued surface components (a torus and a sphere at radius 20) as a single list of cell-count witnesses. Cosmology and foam-interface work cites it when feeding the algebraic genus and gluing-closure certificates. The body is a two-element list literal of the precomputed torus and sphere components.
Claim. The Phase-36 horizon annulus-handle polygon-gluing data is the two-element list consisting of the torus component (vertices $1632$, edges $3264$, faces $1632$, Euler characteristic $0$, fully cyclic vertex links) and the sphere component (vertices $2484$, edges $4964$, faces $2482$, Euler characteristic $2$, fully cyclic vertex links).
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the genus of the boundary of a regular neighborhood of the positive excursion set. After raw cubical boundaries showed nonmanifold edges, the readout switched to the desingularized regular-neighborhood boundary, whose total genus is forced to equal $b_1$ once component count and Euler data match the canonical formulae.
A PolygonGluingComponent records one Phase-36 polygon-glued surface: quotient vertex, split-edge, and face counts, the Euler characteristic, and a local vertex-link audit (number of links versus number of cyclic links). The two upstream witnesses fix the horizon $R=20$ torus ($\chi=0$) and sphere ($\chi=2$), each with every vertex link cyclic.
Phase 37 treats a finite polygon gluing with binary edge pairing and cyclic quotient-vertex links as a combinatorial certificate that reduces to the Phase-35 component-assembly theorem; this list is that certificate's component payload.
proof idea
Pure data definition: the value is the two-element list whose head is the precomputed torus component and whose tail is the precomputed sphere component. No tactics, no lemmas, no arithmetic at this site.
why it matters
Feeds the Phase-37 algebraic wrappers that close the horizon annulus-handle story. Downstream, horizonAnnulusHandle_polygonGluingCloses asserts that these components have the recorded Euler counts and cyclic vertex links and reduce to the Phase-35 horizon component assembly; horizonAnnulusHandle_polygonGluedGenus then reads total corrected genus one from the half-Euler assembly of the same list.
In the module arc this is the Phase-36 witness payload: finite combinatorial cell counts, not a homeomorphism to the geometric regular-neighborhood boundary. The embedded digital-cubical collapse and the final regular-neighborhood homeomorphism remain open; this definition only supplies the numeric certificate those later algebraic bridges decide by native_decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.