correctedComponentEuler
plain-language theorem explainer
Sums the Euler characteristics of a finite list of corrected boundary components after edge pairing and local vertex-link collapse. Cosmology certificates cite it as the total corrected-boundary Euler input to component-assembly and polygon-gluing closure. The body is a one-line map-and-sum over the component Euler fields.
Claim. For a finite list $C_s$ of corrected boundary components (each carrying only an integer Euler characteristic), the total corrected-component Euler characteristic is $\sum_{C \in C_s} \chi(C)$.
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 exact positive excursion set. After raw cubical boundaries showed nonmanifold edges, the readout switched to a desingularized surface: edge-paired faces plus local vertex-link collapse.
A corrected boundary component is represented only by its integer Euler characteristic $\chi$. The companion count of such components is the list length. The module's target identities are that the desingularized boundary has $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
The half-Euler of the region, $b_0-b_1+b_2$, is kept explicit so that doubled-boundary arithmetic is never hidden behind integer division.
proof idea
Definitional one-liner: map each corrected component to its euler field and take the integer list sum. No lemmas or tactics; the value is exactly $\sum_i \chi(C_i)$.
why it matters
Phase 35's component-assembly predicate requires this total to equal twice a supplied half-Euler that matches the region's Euler characteristic, together with the canonical component count. That predicate is the algebraic half of forcing total desingularized genus to equal $b_1$.
Numeric certificates discharge it directly: the horizon-annulus handle sums to $2$ (twice region Euler $1$), and the dyadic sponge R20 sums to $-144$ (twice $-72$). Polygon-gluing, oriented-gluing, and surface-type classification wrappers unfold through the same sum when reducing to component assembly.
This is arithmetic scaffolding only. The module still leaves open the embedded digital-cubical collapse and homeomorphism of corrected cellulations to genuine regular-neighborhood boundary components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.