genus125Component
plain-language theorem explainer
Named constant for the large corrected boundary component of the dyadic sponge probe: Euler characteristic −248, hence genus 125 if closed and orientable. Cosmology and foam-interface work cites it when assembling Phase-34 corrected component lists. The body is a one-field structure literal.
Claim. Let a corrected boundary component be a connected piece of the edge-paired, vertex-link-collapsed boundary, recorded only by its Euler characteristic $\chi\in\mathbb{Z}$. The dyadic probe's large component is the component with $\chi=-248$. For a closed orientable surface this is genus $g=125$, since $\chi=2-2g$.
background
This module builds the algebraic bridge between a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ and the topology of the boundary of a regular neighborhood of the exact positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to that desingularized readout. Corrected components further encode edge pairing and local vertex-link collapse; each is stored only as an integer Euler characteristic.
For a closed orientable surface, $\chi=2-2g$, so $\chi=-248$ forces genus $125$. The module proves arithmetic identities (boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, total desingularized genus equal to $b_1$) and numeric certificates for horizon/dyadic probes, not the geometric homeomorphism to the regular-neighborhood boundary.
proof idea
Definitional structure literal: inhabit CorrectedBoundaryComponent by setting the single field euler to $-248$. No lemmas or tactics; the genus reading $g=125$ is the classical closed-orientable relation $\chi=2-2g$, recorded in the doc-comment rather than proved here.
why it matters
Feeds dyadicSpongeR20CorrectedComponents, the Phase-34 list for the dyadic sponge: this genus-125 piece plus 52 sphere components. That list is the numeric certificate half of the Phase-35 component-assembly bridge: if corrected edge-paired face components have the canonical count and Euler half-sum, total genus is forced to $b_1$.
In the broader RS cosmology stack this is a concrete handle on the horizon-annulus / dyadic foam interface after desingularization. It does not close the still-open embedded digital-cubical collapse or the homeomorphism of corrected cellulations to regular-neighborhood boundary components; those remain geometric realization gaps beyond the arithmetic bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.