correctedComponentGenusFromHalfEuler
plain-language theorem explainer
Total desingularized boundary genus is the corrected component count minus a supplied half-Euler integer. Cosmology certificates for horizon-annulus and dyadic-sponge readouts cite this as the genus readout. The body is pure arithmetic: length of the component list minus halfEuler, keeping the doubled-boundary factor explicit.
Claim. Given a finite list $C$ of corrected boundary components (each carrying only an Euler characteristic) and an integer half-Euler value $h$, the total genus is $|C| - h$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the genus of the boundary of a regular neighborhood of the positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, the canonical readout became that desingularized surface: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and genus equal to components minus the region's Euler characteristic, forcing total genus $b_1$.
A corrected boundary component is one connected piece after edge pairing and local vertex-link collapse, stored only by its Euler number. The component count is just the list length. The half-Euler argument is the Euler half-sum kept as an explicit integer so the doubled-boundary identity is never buried in integer division.
proof idea
Definitional one-liner: return correctedComponentCount Cs - halfEuler, i.e. list length minus the supplied half-Euler integer. No lemmas, no tactics.
why it matters
Phase 35's algebraic bridge theorem correctedComponentGenus_eq_b1_of_componentAssemblyCloses unfolds this definition: once component count and Euler half-sum match regular-neighborhood data, the genus equals $b_1$. The same readout feeds the Phase 36/37 polygon-gluing and Phase 38/39 orientability wrappers, plus numeric certificates: horizon-annulus handle genus $1$, dyadic sponge R20 genus $125$ (raw, polygon-glued, and oriented).
It sits in the cosmogenesis desingularized foam interface path. It does not close the still-open geometric realization or homeomorphism of corrected cellulations to true regular-neighborhood boundary components; it only supplies the arithmetic genus total those certificates and bridges share.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.