dyadicSpongeR20_componentAssemblyCloses
plain-language theorem explainer
The Phase-35 algebraic certificate for the R=20 dyadic sponge: its corrected boundary components (one genus-125 surface plus 52 spheres) match the regular-neighborhood assembly data for Betti triple (50,125,3) with half-Euler -72. Cosmologists citing the desingularized foam-interface genus bridge use this numeric lock. The proof unfolds the three equalities and discharges them by native decision.
Claim. For the dyadic sponge probe with Betti numbers $(b_0,b_1,b_2)=(50,125,3)$ and corrected boundary list consisting of one genus-$125$ component together with $52$ spheres, the component-assembly predicate holds at half-Euler $-72$: the corrected component count equals the regular-neighborhood count $b_0+b_2$, the corrected Euler sum equals $2\cdot(-72)$, and $-72$ equals the region Euler characteristic $b_0-b_1+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 bridge asserts boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus equal to $b_1$.
ComponentAssemblyCloses packages the Phase-35 arithmetic gate: a corrected component list has the right count, its Euler sum is twice a supplied half-Euler, and that half-Euler equals the region Euler $b_0-b_1+b_2$. The dyadic sponge at radius 20 is the concrete probe with Betti $(50,125,3)$ and corrected list one genus-125 component plus 52 spheres. Region Euler is $50-125+3=-72$; regular-neighborhood component count is $53$.
Phase 35 still does not prove homeomorphism of the corrected cellulations to the true regular-neighborhood boundary components; it only forces the genus arithmetic once count and Euler half-sum match.
proof idea
Term-mode proof that unfolds ComponentAssemblyCloses into its three conjuncts (corrected count equals regular-neighborhood components, corrected Euler equals twice the half-Euler, half-Euler equals region Euler) and closes all three by native_decide on the concrete numeric definitions of the dyadic sponge Betti triple, the corrected component list, and the integer $-72$. No intermediate lemmas are invoked beyond those definitions.
why it matters
Phase-35 lock for the dyadic sponge: once corrected edge-paired face components carry the canonical count and Euler half-sum, total genus is forced to $b_1=125$. The module doc states this algebraic half of the Phase-34 component assembly; later Phase-37 polygon-gluing and Phase-39 orientability wrappers reduce to the same assembly predicate. Downstream use count is presently zero in the graph, so the certificate stands as a numeric endpoint rather than an intermediate lemma.
It does not close the embedded digital-cubical collapse or the geometric realization theorem; those remain open. Within Recognition cosmology it supplies the concrete R=20 witness that the desingularized foam-interface genus readout matches the first Betti number of the positive region, consistent with the regular-neighborhood genus bridge used by the cosmogenesis foam-interface scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.