dyadicSpongeR20_correctedComponentCount
plain-language theorem explainer
For the Phase-34 dyadic sponge at R=20, the corrected boundary-component list has length equal to the regular-neighborhood prediction b₀+b₂ from the Betti triple (50,125,3), both equal to 53. Cosmology and foam-interface work cites this as the numeric component-count certificate in the desingularized boundary bridge. The proof is a one-line native_decide on the concrete list length and Betti sum.
Claim. Let the Phase-26 dyadic sponge at $R=20$ have Betti numbers $(b_0,b_1,b_2)=(50,125,3)$, and let the Phase-34 corrected component list be one genus-$125$ surface together with $52$ spheres. Then the length of that corrected list equals the regular-neighborhood boundary component count $b_0+b_2$.
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 positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to that desingularized readout. The predicted boundary component count is $b_0+b_2$, the boundary Euler characteristic is $2(b_0-b_1+b_2)$, and the total desingularized genus is forced to $b_1$.
regularBoundaryComponents is exactly $b_0+b_2$. correctedComponentCount is the length of a finite list of corrected boundary components (edge-paired face assemblies from Phase 34). The dyadic sponge probe is fixed at Betti triple $(50,125,3)$; its corrected list is one genus-$125$ component plus $52$ spheres. Phase 35 uses matching component count and Euler half-sum to force total genus $b_1$, still without a homeomorphism theorem to the true regular-neighborhood boundary.
proof idea
Term-mode proof by native_decide. Both sides are closed integer expressions: left is List.length of a concrete list [genus125Component] ++ replicate 52 sphereComponent, hence $1+52=53$; right is $50+3=53$ from the fixed Betti triple. No lemmas are invoked beyond definitional unfolding of those four defs.
why it matters
Phase 34/35 of the regular-neighborhood boundary genus bridge needs a numeric certificate that the corrected component assembly for the dyadic sponge has the canonical component count $b_0+b_2=53$. The module doc states: if corrected edge-paired face components have the canonical component count and Euler half-sum, then total genus is forced to $b_1$. This theorem discharges the component-count half of that gate for the R=20 dyadic sponge probe used by the cosmogenesis foam-interface scripts.
No downstream Lean theorems currently depend on it (used_by is empty); it is a leaf numeric certificate. It does not close the still-open embedded digital-cubical collapse or the homeomorphism of corrected cellulations to regular-neighborhood components. It sits strictly inside the algebraic/combinatorial certificate layer (Phases 34–39), not the geometric realization theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.