polygonComponentsToCorrected
plain-language theorem explainer
Maps a finite list of polygon-glued surface components to Euler-only corrected boundary components by discarding vertex, edge, face, and link-audit fields. Cosmology certificates for Phase-37/38 polygon gluing and orientability cite it whenever a polygon witness must reduce to the Phase-35 assembly algebra. The body is a one-line list map of the single-component forgetful map.
Claim. Given a finite list $C_s$ of polygon-glued surface components (each carrying quotient vertex, split-edge, face, Euler, and vertex-link audit data), return the list of corrected boundary components obtained by retaining only each component's Euler characteristic $\chi$.
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 edge pairing and local vertex-link collapse, each connected piece of the corrected boundary is recorded only by its Euler characteristic (a CorrectedBoundaryComponent).
Phase 36 upgrades that Euler stub to a PolygonGluingComponent: quotient vertices, split edges, faces, recorded Euler count, and a local vertex-link audit (total links vs cyclic links). The single-component forgetful map keeps only euler. The present definition lifts that forgetful map to lists, so a finite polygon-gluing witness can be fed into the Phase-35 component-assembly algebra.
Module status is partial through Phase 44 and conditional at Phase 47: arithmetic and numeric certificates are proved; the embedded digital-cubical homeomorphism to the true regular-neighborhood boundary remains open.
proof idea
One-line definition: apply the single-component forgetful map to every entry via List.map. That map sends a polygon-glued component $C$ to the corrected component whose sole field is $C.\mathrm{euler}$. No arithmetic, no hypotheses, no tactics.
why it matters
Phase 37's polygon-gluing wrapper reduces a finite binary edge-gluing witness with cyclic quotient-vertex links to the Phase-35 assembly theorem only after the polygon list is forgotten to Euler-only corrected components. This definition is that forgetful step on lists.
Downstream it appears in the dyadic-sponge R20 certificates: polygon-gluing closure, oriented polygon-gluing closure, glued genus $125$ from half-Euler data with region Euler $-72$, surface-type classification (one genus-$125$ surface plus $52$ spheres), and the analogous horizon-annulus handle statements. Length preservation under the oriented forgetful composite is also stated explicitly.
It does not touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure combinatorial bookkeeping inside the cosmogenesis desingularized-boundary pipeline. The open geometric gap remains: corrected cellulations are not yet proved homeomorphic to regular-neighborhood boundary components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.