dyadicSpongeR20CorrectedComponents
plain-language theorem explainer
Phase-34 data package for the dyadic sponge R20 probe: the corrected boundary after edge pairing is recorded as one closed orientable genus-125 surface together with 52 spheres. Cosmology and digital-topology auditors cite it when checking component count, Euler half-sum, and total genus against the regular-neighborhood bridge. The body is a literal list constructor, not a proof.
Claim. The Phase-34 corrected boundary of the dyadic sponge at resolution R20 is the finite list consisting of one component with Euler characteristic $\chi=-248$ (genus $125$ if closed and orientable) followed by fifty-two sphere components each with $\chi=2$.
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 Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to the desingularized readout; the bridge asserts boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus exactly $b_1$.
A corrected boundary component is represented only by its Euler characteristic after edge pairing and local vertex-link collapse. The sphere atom has $\chi=2$. The large dyadic atom has $\chi=-248$, which is genus $125$ for a closed orientable surface via $\chi=2-2g$. Phase 34 packages the numeric split used by later assembly certificates; Phase 35 then forces total genus from component count and Euler half-sum without yet proving homeomorphism to the geometric regular-neighborhood boundary.
proof idea
Definitional list, not a derived proof. It concatenates the singleton list of the genus-125 component ($\chi=-248$) with List.replicate 52 copies of the sphere component ($\chi=2$). Downstream theorems discharge count, Euler sum, and genus claims by native_decide against this concrete list.
why it matters
Feeds the four Phase-34/35 numeric certificates: corrected component count equals the regular-boundary component count from the dyadic Betti data (53); corrected Euler sum equals twice the region Euler half-sum ($-144=2\cdot(-72)$); the Phase-35 assembly predicate closes on half-Euler $-72$; and total corrected genus is $125$. Those certificates are the algebraic half of the cosmogenesis foam-interface desingularization pipeline.
In the module arc this is the dyadic sponge witness parallel to the horizon-annulus split. It does not close the still-open embedded digital-cubical collapse or the homeomorphism of corrected cellulations to regular-neighborhood components; Phase 37 only wraps polygon-gluing certificates that reduce to the same assembly arithmetic. Landmark contact is local (cubical foam topology), not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.