dyadicPolygonLargeSphereComponent
plain-language theorem explainer
Concrete cell-count certificate for one large spherical surface piece in the Phase-36 dyadic polygon gluing: 30 faces, Euler characteristic 2. Cosmology readers assembling the desingularized foam-interface components cite it when building the full Phase-36 list. The body is a structure literal packing quotient vertices, split edges, faces, Euler data, and a full cyclic vertex-link audit.
Claim. The large-sphere component of the dyadic Phase-36 polygon gluing is the surface cellulation with $V=32$, $E=60$, $F=30$, Euler characteristic $\chi=V-E+F=2$, and a complete cyclic vertex-link audit ($32$ links, all $32$ cyclic).
background
This module builds the algebraic bridge from cubical positive-excursion sets to desingularized regular-neighborhood boundaries (Phases 27–47). After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood of ${q>0}$. The target identity is that total desingularized boundary genus equals the first Betti number $b_1$ of the region.
Phase 36 supplies a finite polygon-gluing witness: binary edge pairings, cyclic quotient-vertex links, and corrected component Euler data. A PolygonGluingComponent records one such surface piece: quotient vertex count, split-edge count, face count, Euler characteristic, and a local vertex-link audit (number of links versus number of cyclic links).
The present definition is the large-sphere entry in that witness. Euler $\chi=2$ with $F=30$ marks a spherical topology at the high end of the sphere sizes used in the dyadic sponge assembly.
proof idea
Definition by structure literal, not a proof. The six fields are filled with the fixed integers $(V,E,F,\chi,\mathrm{links},\mathrm{cycles})=(32,60,30,2,32,32)$. No lemmas are applied; consistency of $\chi=V-E+F$ is checked elsewhere by the component Euler predicate on PolygonGluingComponent.
why it matters
Feeds the Phase-36 component roster dyadicSpongeR20PolygonComponents, which concatenates one genus-125 piece, 48 small spheres, 3 medium spheres, and this single large sphere. That list is the combinatorial input to the Phase-37 polygon-gluing genus wrapper: if binary edge gluing, cyclic vertex links, and corrected Euler data hold, total genus reduces to the Phase-35 assembly theorem (forced equal to $b_1$).
Also seeds the Phase-38 orientability lift dyadicOrientedLargeSphereComponent, which attaches a full face-orientation assignment with zero contradictions. Together these close the finite certificate side of the regular-neighborhood genus bridge. They do not discharge the still-open geometric realization (homeomorphism of the glued cellulations to the actual regular-neighborhood boundary components).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.