dyadicSpongeR20_regularBoundaryComponents
plain-language theorem explainer
For the Phase-26 dyadic sponge probe at radius 20, with Betti numbers (b₀,b₁,b₂)=(50,125,3), the regular-neighborhood boundary has exactly 53 connected components. Cosmogenesis and foam-interface readers cite this as the numeric component certificate. The proof is a one-line native decision of the integer identity 50+3=53.
Claim. Let the Phase-26 dyadic sponge at $R=20$ have Betti triple $(b_0,b_1,b_2)=(50,125,3)$. Then the predicted regular-neighborhood boundary component count equals $b_0+b_2=53$.
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. Phase 25 found nonmanifold edges on the raw cubical boundary, so Phase 26 switched to the desingularized readout: boundary components $b_0+b_2$, boundary Euler characteristic $2(b_0-b_1+b_2)$, and total genus equal to $b_1$.
The helper regularBoundaryComponents is the Alexander-duality style count $b_0+b_2$. The input certificate dyadicSpongeR20Betti freezes the Phase-26 dyadic sponge probe at $R=20$ as the integer triple $(50,125,3)$. Sibling lemmas then relate Euler characteristic and genus of that same boundary to the region Betti numbers; this declaration only pins the component count.
proof idea
Unfold the definitions: components equal $b_0+b_2$, and the sponge Betti data supplies $b_0=50$, $b_2=3$. The goal reduces to the closed integer equation $50+3=53$, discharged by native_decide. No geometric lemmas are invoked.
why it matters
It is a horizon/dyadic numeric certificate in the regular-neighborhood genus bridge used by the cosmogenesis foam-interface desingularization pipeline. Together with the matching Euler and genus certificates for the same Betti triple, it locks the arithmetic side of Phases 26–35: components $b_0+b_2$, $\chi(\partial)=2\chi(\mathrm{region})$, total genus $b_1$.
The module status remains partial through Phase 44 and conditional at Phase 47: the embedded digital-cubical collapse and the homeomorphism of corrected cellulations to actual regular-neighborhood boundary components stay open. This theorem does not close those geometric gaps; it only certifies the component arithmetic for the $R=20$ sponge probe. No downstream Lean consumers are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.