dyadicSpongeR20SurfaceTypes
plain-language theorem explainer
Ordered inventory of closed orientable surface types for the dyadic-sponge regular-neighborhood boundary at R=20: one genus-125 surface and fifty-two spheres. Phase-42–47 cosmology certificates cite this list when matching oriented polygon components to standard surfaces and when totaling genus. Pure data definition: singleton concatenated with a 52-fold replicate.
Claim. The ordered list of standard closed orientable surface types for the dyadic-sponge polygon components at $R=20$ is one surface of genus $125$ followed by fifty-two spheres (genus $0$).
background
This module bridges cubical positive-excursion topology to a desingularized regular-neighborhood boundary readout. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to the boundary of a regular neighborhood of ${q>0}$. Algebraically, if a compact 3D cubical region has Betti triple $(b_0,b_1,b_2)$, the regular-neighborhood boundary has $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
A StandardSurfaceType is a closed orientable surface classified by an integer genus $g$, with Euler characteristic $2-2g$. The building blocks here are the standard genus-125 surface and the standard sphere (genus $0$). The dyadic sponge at $R=20$ is a numeric Phase-26/28/30 artifact whose oriented polygon components are later paired against this fixed type list.
proof idea
Definitional data, not a proof. The list is the singleton containing the standard genus-125 surface, concatenated with List.replicate 52 of the standard sphere. No lemmas or tactics; the value is the certificate payload consumed by later native_decide and classification wrappers.
why it matters
This list is the surface-type side of the Phase-42–47 dyadic certificates. Downstream, dyadicSpongeR20_surfaceTypeClassificationCloses asserts the oriented polygon components classify as one genus-125 surface plus 52 spheres; dyadicSpongeR20_surfaceTypeGenusTotal checks the genus sum is 125; dyadicSpongeR20_componentwiseSurfaceInventory matches ordered Euler signatures and aggregate inventory to the regular boundary; dyadicSpongeR20_componentPairingCloses closes the ordered pairing.
The Phase-46 capstone packages concrete closed-orientable obligations from this list (not placeholders). Phase 47 is conditional: under closed-surface classification, every dyadic component realizes its paired standard surface. The module still leaves the embedded digital-cubical homeomorphism open; this definition only fixes the combinatorial target inventory for the $R=20$ sponge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.