orientedPolygonToPolygon
plain-language theorem explainer
Projects a Phase-38 oriented polygon-gluing component onto its underlying Phase-36 polygon component by discarding face-orientation audit fields. Anyone reducing an oriented gluing witness to the unoriented polygon-gluing bridge cites this forgetful map. The body is the structure field projection onto the embedded polygon record.
Claim. Given an oriented polygon-gluing component $C$ (a Phase-36 polygon component together with face-assignment count and orientation-contradiction count), return the underlying polygon-gluing component of $C$, forgetting the orientability audit.
background
This module builds the algebraic bridge from cubical positive-excursion topology to a desingularized regular-neighborhood boundary. After raw singular edges appear (Phase 25), the readout switches to the boundary of a regular neighborhood; later phases supply finite combinatorial certificates that the corrected surface genus equals the first Betti number $b_1$ of the region.
A PolygonGluingComponent (Phase 36) records quotient vertices, split edges, faces, Euler characteristic, and a local vertex-link audit (link count versus cyclic-link count). An OrientedPolygonGluingComponent (Phase 38) wraps that record with two orientation-solver integers: how many faces received a sign assignment, and how many sign contradictions remain. Phase 39's oriented gluing witness succeeds only when every face is assigned and contradictions vanish, then inherits the Phase-37 polygon-gluing genus theorem on the forgotten polygon data.
The present map is the single-component forgetful arrow used to strip that orientation layer before applying the unoriented assembly algebra.
proof idea
One-line definition: return the polygon field of the oriented component structure. No lemmas, tactics, or arithmetic; pure field projection from OrientedPolygonGluingComponent to PolygonGluingComponent.
why it matters
Phase 39 needs a clean reduction from oriented certificates to the Phase-37 polygon-gluing bridge. This projection is that reduction at component scale; the list map orientedPolygonsToPolygons is the bulk form.
Downstream, correctedComponentCount_orientedPolygons uses it to show forgetting preserves component count. The numeric closures horizonAnnulusHandle_orientedPolygonGluingCloses and dyadicSpongeR20_orientedPolygonGluingCloses unfold through it when they inherit Phase-37 gluing from a successful orientation solve. The surface-type classifiers for the horizon annulus (torus plus sphere) and the dyadic sponge (genus-125 surface plus 52 spheres) likewise route oriented data through this forgetful step.
It does not close the still-open geometric realization or homeomorphism to the true regular-neighborhood boundary; it only keeps the orientability gate from blocking the algebraic genus arithmetic already proved for unoriented polygon gluings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.