correctedComponentCount_orientedPolygons
plain-language theorem explainer
Forgetting a list of oriented polygon-gluing components down to corrected boundary components preserves cardinality: the corrected-component count equals the original list length. Cosmology inventory algebra and surface-type classification cite this when matching type counts to components. The proof is pure definitional unfolding plus simplification through the forgetful maps.
Claim. For any finite list $C_s$ of oriented polygon-gluing components, the corrected-component count of the image of $C_s$ under the composite forgetful map (oriented polygons $\to$ polygon-gluing components $\to$ corrected boundary components) equals the length of $C_s$ as an integer.
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 its regular-neighborhood boundary. After desingularization, boundary components number $b_0+b_2$, boundary Euler is $2(b_0-b_1+b_2)$, and total genus equals $b_1$. Later phases add combinatorial certificates (edge pairing, polygon gluing, orientability) that still stop short of a homeomorphism theorem.
An oriented polygon-gluing component packages a Phase-36 polygon component with face-orientation audit data (facesAssigned, orientationContradictions). Two forgetful maps strip that structure: first drop orientation to a plain polygon-gluing component, then retain only the Euler number as a corrected boundary component. The corrected-component count is simply the length of that final list, valued in $\mathbb{Z}$ for the inventory algebra.
proof idea
Unfold the five definitions in the composite: correctedComponentCount (list length as $\mathbb{Z}$), polygonComponentsToCorrected and orientedPolygonsToPolygons (both List.map), and the two pointwise forgetters polygonComponentToCorrected and orientedPolygonToPolygon. After unfolding, simp discharges the equality because mapping preserves length and casting Nat length to $\mathbb{Z}$ is definitional. No external lemmas are required beyond the in-module defs.
why it matters
Phase 39 records the orientability gate on polygon components without claiming the missing regular-neighborhood homeomorphism. Length preservation is the inventory step that lets a closed standard-surface classification match its assigned surface-type list to the oriented-component list: the downstream theorem surfaceType_length_eq_orientedPolygon_length_of_surfaceTypeClassificationCloses invokes this equality when the classification closes (type count equals component count and type-genus totals $b_1$).
Within the broader RS cosmology stack this is bookkeeping, not a forcing-chain landmark, but it keeps the Phase-35/37/39 genus bridge coherent so that desingularized boundary genus remains forced to $b_1$ once the combinatorial certificates close. The geometric realization and embedded digital-cubical collapse stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.