surfaceTypeCount
plain-language theorem explainer
Counts how many standard closed orientable surfaces sit in a finite assignment list, returning that cardinality as an integer for Euler bookkeeping. Cosmology inventory lemmas cite it when matching surface-type lists to regular-neighborhood boundary components. The body is the list length, coerced to ℤ.
Claim. Given a finite list $S$ of standard closed orientable surfaces (each classified by an integer genus $g$), the surface-type count of $S$ is $\# 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, 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 the combinatorial stand-in for a closed orientable surface: a single integer genus $g$, with Euler characteristic $2-2g$. Finite lists of these types are the inventory side of the Phase-41/42 classification: each oriented polygon-gluing component is paired with one standard type.
The count is deliberately valued in $\mathbb{Z}$ so it sits in the same additive algebra as component counts, half-Euler sums, and genus totals used by the regular-boundary formulas.
proof idea
Pure definition: the value is the length of the input list of standard surface types, read as an integer. No lemmas, no tactics.
why it matters
Inventory gate for the surface-type classification package. SurfaceTypeClassificationCloses requires the type count to equal the corrected polygon-component count, and that every component carries a matching standard type with total genus $b_1$. From there, surfaceTypeCount_eq_regularBoundaryComponents_of_surfaceTypeClassificationCloses promotes the count to the regular-neighborhood component formula $b_0+b_2$.
Downstream, ComponentPairingCloses and the Phase-42 componentwise inventory theorems (including the horizon-annulus and dyadic-sponge certificates) reuse the same equality so ordered Euler signatures and aggregate genus match the regular boundary. The geometric homeomorphism of corrected cellulations to the true regular-neighborhood boundary remains open; this definition only supplies the integer cardinality used by those algebraic certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.