horizonAnnulusHandleOrientedPolygonComponents
plain-language theorem explainer
Names the ordered Phase-38 oriented polygon inventory for the horizon-annulus handle: one torus component and one sphere component, each carrying a full face-orientation assignment with zero sign contradictions. Cosmology certificates that need the concrete component list (genus, pairing, surface-type inventory, embedded obligations) cite this constant. The body is a two-element list literal of the prebuilt oriented torus and sphere records.
Claim. The Phase-38 oriented horizon polygon inventory is the ordered list consisting of the oriented torus component (1632 faces assigned, 0 orientation contradictions) followed by the oriented sphere component (2482 faces assigned, 0 orientation contradictions).
background
This module builds the algebraic bridge from a compact cubical region's Betti triple $(b_0,b_1,b_2)$ to the desingularized regular-neighborhood boundary: component count $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$. Phase 25 saw nonmanifold edges on the raw cubical boundary of ${q>0}$; Phase 26 switched to the regular-neighborhood readout. Later phases add arithmetic certificates (edge pairing, polygon gluing, orientability) without yet proving geometric homeomorphism.
An OrientedPolygonGluingComponent packages a Phase-36 polygon-gluing component (cells and link audit) with a face-sign solve: facesAssigned and orientationContradictions. Orientation succeeds when every face is assigned and contradictions are zero. The two upstream constants supply exactly that data for the horizon torus (1632 faces, 0 contradictions) and sphere (2482 faces, 0 contradictions).
proof idea
Pure definition: a two-element list literal. First entry is the oriented torus component; second is the oriented sphere component. No tactics, no lemmas, no computation beyond assembling the already-certified Phase-38 records.
why it matters
This list is the shared input for the Phase-38–46 horizon certificates. Downstream theorems use it to close oriented polygon gluing (horizonAnnulusHandle_orientedPolygonGluingCloses), read total glued genus one (horizonAnnulusHandle_orientedPolygonGluedGenus), match componentwise Euler inventory to the regular boundary (horizonAnnulusHandle_componentwiseSurfaceInventory), close torus/sphere pairing (horizonAnnulusHandle_componentPairingCloses), classify every entry as a combinatorial closed orientable surface (horizonAnnulusHandle_all_combinatorialSurface), and discharge the Phase-46 concrete embedded-obligation package (horizonAnnulusHandle_concreteEmbeddedObligationsClose).
In the module narrative it is the Phase-39 orientability gate's concrete witness list: full face orientations with zero contradictions, inheriting the Phase-37 polygon-gluing genus theorem. It does not close the still-open embedded digital-cubical collapse or the regular-neighborhood homeomorphism; those remain geometric, not algebraic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.