orientedPolygonEulerTotal
plain-language theorem explainer
Total Euler characteristic of a finite list of oriented polygon-gluing components, formed by summing each component's polygon Euler number. Cosmology surface-inventory certificates cite it when matching polygon data to regular-neighborhood boundary Euler totals. The body is a one-line list sum of the ordered Euler signature.
Claim. For a finite list $C_s$ of oriented polygon-gluing components, the total Euler characteristic is $\sum_i \chi(P_i)\in\mathbb{Z}$, where $P_i$ is the underlying polygon-gluing cellulation of the $i$-th component and $\chi(P_i)$ is its Euler characteristic.
background
This module builds the algebraic bridge from desingularized regular-neighborhood boundaries of cubical positive regions to genus and Euler inventories. For a compact 3D cubical region with Betti triple $(b_0,b_1,b_2)$, the regular-neighborhood boundary is expected to have $b_0+b_2$ components and Euler characteristic $2(b_0-b_1+b_2)$, so total boundary genus equals $b_1$. Phases 36–39 package finite polygon gluings with binary edge pairing, cyclic vertex links, and face-orientation certificates.
An oriented polygon-gluing component pairs a Phase-36 polygon cellulation (with its Euler number) to face-assignment and orientation-contradiction counts from the Phase-38 orientability solve. The ordered Euler signature of a list of such components is the list of those polygon Euler numbers. The present definition aggregates that list to a single integer total.
proof idea
Definitional one-liner: map the component list to its ordered Euler signature, then take the integer sum. No tactics or lemmas beyond the list-sum of that signature.
why it matters
This total is the aggregate side of the Phase-42 surface inventory. Under a closed surface-type classification it equals the standard-surface Euler total, and the componentwise inventory theorem strengthens that to ordered Euler-list equality plus match against the regular-boundary Euler number of the Betti triple. Concrete certificates for the horizon-annulus handle and the dyadic sponge R20 quote the same total against their regular-boundary Euler data.
In the module arc this is bookkeeping for the algebraic half of the desingularized foam interface: it lets polygon-gluing witnesses feed the genus bridge without claiming the still-open embedded homeomorphism to the geometric regular-neighborhood boundary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.