surfaceTypeEulerTotal
plain-language theorem explainer
Sums the Euler characteristics of a finite list of standard closed orientable surfaces, each contributing 2−2g for its genus g. Cosmology proofs that classify regular-neighborhood boundary components as standard surfaces cite this total as the inventory-side Euler number. The body is a one-line map-and-sum over the per-surface Euler formula.
Claim. For a finite list $S_1,\ldots,S_n$ of standard closed orientable surfaces with genera $g_1,\ldots,g_n$, the total Euler characteristic is $\sum_{i=1}^n (2-2g_i)$.
background
This module builds the algebraic bridge between a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ and the topology of the boundary of a regular neighborhood of the exact positive region ${q>0}$. After desingularization, that boundary is expected to have $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
A StandardSurfaceType is a closed orientable surface classified solely by an integer genus $g$. Its Euler characteristic is the classical formula $2-2g$ (via standardSurfaceEuler). The present definition aggregates those values over a finite inventory list: the assigned surface types for oriented polygon components after classification closes.
Sibling quantities include component count, total genus, and the canonical regular-boundary Euler number derived from the Betti triple. Equality theorems later identify this sum with those geometric readouts under a closed surface-type classification.
proof idea
Pure definition: map each list entry through the per-surface Euler formula $2-2g$, then take the integer sum. No lemmas or tactics; the arithmetic identity with $2\cdot#\mathrm{components}-2\cdot\mathrm{total\ genus}$ is proved separately by induction on the list.
why it matters
This is the inventory-side Euler total in the Phase 41 surface-type classification bridge. Downstream, surfaceTypeEulerTotal_eq_count_genus rewrites it as $2\cdot\mathrm{count}-2\cdot\mathrm{genus\ total}$; orientedPolygonEulerTotal_eq_surfaceTypeEulerTotal_of_surfaceTypeClassificationCloses and componentPairingEulerTotal_eq_surfaceTypeEulerTotal equate polygon and pairing Euler sums to this total when lengths and classification close; and surfaceTypeEulerTotal_eq_regularBoundaryEuler_of_surfaceTypeClassificationCloses together with surfaceTypeInventory_matches_regularBoundary_of_surfaceTypeClassificationCloses match the inventory to the canonical regular-neighborhood boundary Euler $2(b_0-b_1+b_2)$.
In the module's program, that match is the algebraic half of the desingularized foam-interface readout used by the cosmogenesis scripts. It does not close the still-open geometric homeomorphism from corrected cubical cellulations to the regular-neighborhood boundary; it only supplies the Euler number that those certificates compare.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.