surfaceTypeGenusTotal
plain-language theorem explainer
Sums the genera of a finite list of standard closed orientable surfaces. Cosmology inventory certificates cite it when matching polygon-gluing components to a regular-neighborhood boundary genus total. The body is the obvious map-then-sum definition over the genus field.
Claim. Given a finite list $S$ of standard closed orientable surfaces, each classified by an integer genus $g(s)$, the total genus is $\sum_{s \in S} g(s) \in \mathbb{Z}$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the topology of the boundary of a regular neighborhood of the positive excursion set. After desingularization, boundary components number $b_0+b_2$, boundary Euler characteristic is $2(b_0-b_1+b_2)$, and total boundary genus equals $b_1$.
A StandardSurfaceType is just a closed orientable surface labeled by its integer genus $g$, with Euler characteristic $2-2g$. Lists of such types are the target side of componentwise surface inventories: each oriented polygon-gluing component is paired with a standard surface, and aggregate genus must match the regular-boundary genus readout.
The definition sits beside sibling tallies (surface-type count, Euler list/total) used in Phase-42 classification-closure predicates.
proof idea
Definition only: project each list entry to its genus field, then take the integer list sum. No lemmas or tactics.
why it matters
Parent equalities identify component-pairing genus totals with this sum once source and target lists have equal length. Phase-42 inventory theorems require the sum (with Euler lists and counts) to match the regular-boundary genus forced by the Betti triple, still without proving homeomorphism of cellulations.
Concrete certificates evaluate it: the dyadic sponge R20 surface list totals genus $125$ (one genus-$125$ surface plus $52$ spheres); the horizon-annulus handle has an analogous closed inventory. Those numeric facts feed the foam-interface desingularized cosmogenesis pipeline. The geometric realization (embedded digital-cubical collapse to the true regular neighborhood) remains open; this is pure arithmetic bookkeeping on the classification side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.