orientedPolygonEulerList
plain-language theorem explainer
Extracts the ordered list of Euler characteristics from a list of oriented polygon-gluing components. Cosmology surface-inventory proofs cite it as the polygon-side signature that must match the standard-surface Euler list. The body is a one-line list map onto each component's polygon Euler number.
Claim. For a finite list $C_1,\ldots,C_n$ of oriented polygon-gluing components, the ordered Euler signature is the integer list $(\chi(C_1),\ldots,\chi(C_n))$, where $\chi(C_i)$ is the Euler characteristic of the underlying polygon-gluing cellulation of $C_i$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the desingularized regular-neighborhood boundary: component count $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$. Phase 26 replaced raw cubical boundaries (which can have nonmanifold edges) by the regular-neighborhood readout used in the cosmogenesis foam interface.
An OrientedPolygonGluingComponent is a Phase-38 package: a Phase-36 polygon-gluing component (cells, binary edge gluing, cyclic vertex-link audit) plus face-orientation assignment data and a contradiction count. The Euler number lives on the nested polygon field.
The ordered Euler list is the componentwise inventory half of Phase 42. Matching it against the Euler list of assigned standard closed orientable surfaces is the algebraic gate before aggregate totals and genus bookkeeping.
proof idea
Pure definition: map the list of oriented components to integers by reading C.polygon.euler on each entry. No lemmas, no tactics; the equality theorems that consume this list do the inductive work later.
why it matters
Phase 42 treats this list as the polygon-side ordered signature. Downstream, orientedPolygonEulerList_eq_surfaceTypeEulerList_of_zip and the classification-closure wrapper prove it equals the standard-surface Euler list when lengths match and each zipped pair carries the surface-type predicate. The aggregate orientedPolygonEulerTotal is just the sum of this list.
Parent inventory theorems use both halves: componentwiseSurfaceInventory_matches_regularBoundary_of_surfaceTypeClassificationCloses asserts list equality plus total Euler equal to regularBoundaryEuler B. Concrete certificates horizonAnnulusHandle_componentwiseSurfaceInventory and dyadicSpongeR20_componentwiseSurfaceInventory instantiate that bridge on the horizon-annulus handle and the dyadic sponge.
In the module arc this is still combinatorial bookkeeping, not the missing embedded homeomorphism from corrected polygon gluings to actual regular-neighborhood boundary components. It supports the genus bridge (total desingularized genus $= b_1$) without closing geometric realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.