polygonComponentToCorrected
plain-language theorem explainer
Projects a Phase-36 polygon-glued surface component onto the Phase-35 corrected-boundary component by retaining only its Euler characteristic. Cosmology bridge proofs cite it when reducing polygon-gluing certificates to component-assembly algebra. The body is a one-field structure constructor.
Claim. Map a polygon-glued surface component $C$ (with recorded vertices, edges, faces, Euler number, and vertex-link audit) to the corrected boundary component whose sole datum is the Euler characteristic $\chi(C)$.
background
This module builds the algebraic bridge from raw cubical excursion-set boundaries to the desingularized regular-neighborhood boundary used in cosmogenesis foam readout. After Phase 25 found nonmanifold edges, Phase 26 switched to the regular-neighborhood boundary; later phases supply arithmetic certificates that the total desingularized genus equals the first Betti number $b_1$ of the compact 3D region.
A CorrectedBoundaryComponent is a connected component of the corrected boundary after edge pairing and local vertex-link collapse, represented only by its Euler characteristic. A PolygonGluingComponent is the richer Phase-36 witness: quotient vertex, split-edge, and face counts, the Euler number, and a local vertex-link audit (link count and cyclic-link count).
Phase 37 reduces a finite polygon-gluing certificate (binary edge gluing, cyclic quotient-vertex links, matching corrected Euler data) to the Phase-35 component-assembly theorem. That reduction needs a forgetful map from the polygon-level audit down to Euler-only corrected components.
proof idea
Definitional one-liner: construct the corrected component by copying the euler field of the polygon-glued component and discarding vertices, edges, faces, and vertex-link data. No lemmas or tactics.
why it matters
Phase 35 forces total genus $b_1$ once corrected components have the canonical count and Euler half-sum. Phase 37 needs this forgetful map so polygon-gluing witnesses feed that algebra without carrying cellulation detail.
Downstream, list-level forgetting and length preservation (correctedComponentCount_orientedPolygons, polygonComponentsToCorrected) rest on it. Concrete certificates use it: horizon-annulus and dyadic-sponge R20 polygon-gluing and oriented-polygon-gluing closures, plus the dyadic surface-type classification (genus-125 surface plus spheres).
It is combinatorial scaffolding only. The module still does not prove homeomorphism of corrected cellulations to regular-neighborhood boundary components; the embedded digital-cubical collapse remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.