surfaceTypeEulerTotal_eq_count_genus
plain-language theorem explainer
A finite list of standard closed orientable surfaces has total Euler characteristic equal to twice the component count minus twice the summed genus. Cosmology inventory proofs cite this when converting a surface-type classification into Euler data for the regular-neighborhood boundary. The argument is list induction: each head contributes χ = 2 − 2g, the inductive hypothesis handles the tail, and ring closes the algebra.
Claim. For any finite list of standard closed orientable surfaces with genera $g_1,\ldots,g_n$, writing $\chi_i = 2-2g_i$, one has $\sum_i \chi_i = 2n - 2\sum_i g_i$.
background
This module builds the algebraic bridge between a compact cubical 3-region with Betti triple $(b_0,b_1,b_2)$ and the topology of the boundary of a regular neighborhood of the positive excursion set. After desingularization one expects boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$. The geometric homeomorphism remains open; the file proves the arithmetic identities and certificate wrappers that the cosmogenesis scripts consume.
A standard surface type is a closed orientable surface classified solely by an integer genus $g$. Its Euler characteristic is the classical value $2-2g$. For a list of such types one forms three integer aggregates: the component count (list length), the total genus (sum of genera), and the total Euler characteristic (sum of the per-surface values $2-2g$).
The present identity is the pure bookkeeping step that relates those three aggregates before they are matched to the canonical regular-boundary Euler number.
proof idea
List induction on the surface-type inventory. The empty list unfolds all three aggregates to zero and is settled by norm_num. In the cons step the three aggregates are unfolded; simp rewrites the head Euler value via the definition $2-2g$ and inserts the inductive hypothesis on the tail; ring finishes the integer identity $$(2-2g)+\bigl(2|{\rm rest}|-2G_{\rm rest}\bigr)=2(1+|{\rm rest}|)-2(g+G_{\rm rest}).$$
why it matters
Downstream, the Phase-41 inventory bridge surfaceTypeEulerTotal_eq_regularBoundaryEuler_of_surfaceTypeClassificationCloses applies this identity once a surface-type classification certificate has already forced the component count and total genus to match the regular-neighborhood boundary data. That bridge is one link in the chain (Phases 35–41) that converts oriented polygon-gluing certificates into the statement that total desingularized boundary genus equals $b_1$.
The module status is partial through Phase 44 and conditional at Phase 47: arithmetic and certificate wrappers are proved with zero sorry, while the embedded digital-cubical collapse and the final regular-neighborhood homeomorphism remain open. This lemma is the elementary Euler half of that inventory algebra; without it the classification-closure hypothesis cannot be rewritten as equality of Euler totals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.