orientedPolygonsToPolygons
plain-language theorem explainer
Projects a list of Phase-38 oriented polygon-gluing components to the underlying Phase-36 polygon components by discarding face-orientation audits. Cosmology certificates for horizon-annulus and dyadic-sponge genus and gluing closure cite it whenever they reduce oriented data to the Phase-37 polygon bridge. The body is a one-line list map of the single-component forgetful map.
Claim. Given a finite list of oriented polygon-gluing components (each a Phase-36 polygon component plus face-assignment count and orientation-contradiction count), return the list of underlying polygon-gluing components obtained by forgetting the orientation fields.
background
The module builds an algebraic bridge from cubical positive-excursion sets to desingularized regular-neighborhood boundary genus. After raw nonmanifold edges appear on the horizon-annulus handle, the readout switches to the boundary of a regular neighborhood of ${q>0}$. For Betti triple $(b_0,b_1,b_2)$ the target identities are: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$.
Phase 36 packages each surface piece as a PolygonGluingComponent: quotient vertices, split edges, faces, recorded Euler, and vertex-link cycle audit. Phase 38 wraps that data in an oriented component carrying facesAssigned and orientationContradictions. The single-component forgetful map keeps only the .polygon field; this definition lifts that forgetful step to lists so oriented certificates can reuse the Phase-37 polygon-gluing bridge.
proof idea
One-line definition: map the list with the single-component forgetful function that returns the embedded polygon field of each oriented component. No tactics, no lemmas beyond list map.
why it matters
Phase 39's orientability gate must drop orientation data before invoking Phase-37 polygon-gluing closure and the Phase-35 component-assembly genus theorem. Downstream theorems that unfold this map include oriented gluing closure and glued-genus certificates for the horizon-annulus handle (genus one) and the dyadic sponge R20 (genus 125), the integer length identity for corrected component count, the equality of oriented glued genus with $b_1$ under closure, and the surface-type classification closures. It is pure bookkeeping: it does not prove homeomorphism to the geometric regular-neighborhood boundary (still open per the module status through Phase 47).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.