dyadicSpongeR20PolygonComponents
plain-language theorem explainer
assembles the Phase-36 dyadic sponge (R20) polygon-gluing witness as an explicit list: one genus-125 surface, forty-eight six-face spheres, three twenty-two-face spheres, and one thirty-face sphere. Cosmology proofs that certify the desingularized boundary genus cite this list as the combinatorial input. The body is a pure list concatenation of four named component records.
Claim. The Phase-36 dyadic polygon-gluing certificate is the finite list consisting of one genus-$125$ component, forty-eight cube-sphere components (Euler characteristic $2$), three medium sphere components (Euler characteristic $2$), and one large sphere component (Euler characteristic $2$).
background
This module builds the algebraic bridge from a compact cubical region's Betti triple $(b_0,b_1,b_2)$ to the genus of the boundary of a regular neighborhood of the positive excursion set. After raw cubical boundaries showed nonmanifold edges, the readout switched to desingularized regular-neighborhood boundaries; later phases supply finite combinatorial certificates rather than a full homeomorphism theorem.
A PolygonGluingComponent records quotient vertices, split edges, faces, Euler characteristic, and a local vertex-link audit (link count versus cyclic-link count). The four upstream component defs fix the numeric cells: the large handle has Euler $-248$ (genus $125$), while the small, medium, and large spheres each have Euler $2$ with fully cyclic vertex links.
Phase 37 treats a finite polygon gluing with binary edge pairing and cyclic quotient-vertex links as an algebraic reduction to the Phase-35 component-assembly theorem. This list is exactly that Phase-36 witness for the dyadic sponge at resolution R20.
proof idea
Pure definitional assembly, not a proof. The value is the concatenation
[genus-125] ++ replicate 48 (small sphere) ++ replicate 3 (medium sphere) ++ [large sphere],
each summand a previously defined PolygonGluingComponent record with fixed integer cell counts and matching vertex-link audits. No tactics or lemmas are invoked.
why it matters
Feeds the two Phase-36/37 numeric certificates: dyadicSpongeR20_polygonGluingCloses (components have the recorded Euler data and cyclic links, and reduce to the Phase-35 assembly) and dyadicSpongeR20_polygonGluedGenus (corrected half-Euler genus equals $125$). Those theorems close the algebraic half of the dyadic sponge genus bridge used by the cosmogenesis foam-interface scripts.
In the module arc this is the concrete witness Phase 37 wraps and Phase 39 later orients. It does not settle the still-open geometric realization: homeomorphism of the corrected cellulations to the true regular-neighborhood boundary remains outside the proved arithmetic bridge. Framework role is local to the cosmology desingularization chain, not the T0–T8 forcing spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.