componentPairingEulerTotal_eq_surfaceTypeEulerTotal
plain-language theorem explainer
When an ordered list of oriented polygon-gluing components is paired with a same-length list of standard surface types, the total Euler characteristic of the pairing equals the total Euler characteristic of the surface list alone. Cosmology certificates that close a finite component pairing cite this equality. The proof is list induction on both sides, reducing to the definition of zip and sum.
Claim. Let $C$ be a finite list of oriented polygon-gluing components and $S$ a finite list of standard closed orientable surface types (each classified by genus). If $\mathrm{length}(C)=\mathrm{length}(S)$, then the total Euler characteristic of the ordered pairing $C\mathbin{\mathrm{zip}}S$ equals the total Euler characteristic of $S$, where each surface of genus $g$ contributes $\chi=2-2g$.
background
This module builds the algebraic bridge for the desingularized regular-neighborhood boundary of a compact cubical positive region in the cosmogenesis pipeline. After raw cubical boundaries show nonmanifold edges, the readout switches to the boundary of a regular neighborhood; the file proves arithmetic identities relating Betti numbers, component counts, Euler characteristics, and genus, not the embedded homeomorphism.
A standard surface type is a closed orientable surface classified by an integer genus $g$, with Euler characteristic $2-2g$. An oriented polygon-gluing component packages a Phase-36 polygon cell/link audit together with a face-orientation assignment and a contradiction count from Phase 38.
The ordered component pairing is the zip of the two lists into pairs. The pairing Euler total sums the standard-surface Euler values of the second components; the surface-type Euler total sums the same formula over the surface list alone. The later geometric theorem must replace this abstract pairing with an embedded map.
proof idea
Induct on the component list, generalizing over the surface list. The nil case forces the surface list to be nil by the length hypothesis (otherwise simp contradicts length equality) and both totals are zero by reflexivity. In the cons case the surface list must also be cons; injectivity of successor on lengths gives the tail length equality. Unfolding the pairing and both Euler totals yields an additive identity with the head surface Euler on both sides; the inductive hypothesis rewrites the tail sums and finishes.
why it matters
Phase 43 needs a closed finite component pairing from a closed standard-surface classification. The immediate parent is componentPairingCloses_of_surfaceTypeClassificationCloses, whose doc-comment states: a closed standard-surface classification gives a closed finite component pairing, still without constructing the embedded homeomorphism. This lemma discharges the Euler-total half of that bridge: once lengths match, the pairing's Euler inventory is exactly the classified surface Euler inventory.
In the broader regular-neighborhood genus program (Phases 27–47), the algebraic goal is that total desingularized boundary genus equals the first Betti number $b_1$. Pairing components to standard surfaces of matching Euler characteristic is a gate on that path. The geometric realization (embedded digital-cubical collapse and homeomorphism of corrected cellulations to regular-neighborhood components) remains open; this result is pure list arithmetic inside the certificate layer used by the foam-interface desingularization scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.