dyadicSpongeR20OrientedPolygonComponents
plain-language theorem explainer
Phase-38 inventory of oriented polygon-gluing components for the dyadic sponge R20: one genus-125 surface, forty-eight six-face spheres, three twenty-two-face spheres, and one thirty-face sphere. Downstream genus, pairing, and surface-classification certificates cite this fixed roster as the concrete component list. The body is pure list concatenation of four already-oriented component definitions.
Claim. The oriented dyadic-sponge $R_{20}$ component list is the concatenation of one genus-$125$ oriented polygon component, forty-eight six-face sphere components, three twenty-two-face sphere components, and one thirty-face sphere component (each carrying a full face-orientation assignment with zero sign contradictions).
background
This module builds the algebraic bridge from a compact 3D 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 desingularization, boundary components equal $b_0+b_2$, boundary Euler equals $2(b_0-b_1+b_2)$, and total genus collapses to $b_1$.
Phase 36 supplies polygon-gluing components (cell and link audits). Phase 38 wraps each with a face-orientation solve: an oriented component records the underlying polygon plus facesAssigned and orientationContradictions. The four building blocks here are the oriented genus-125 piece (8988 faces assigned, zero contradictions) and the three sphere sizes (6, 22, and 30 faces assigned, all zero contradictions).
The list is the concrete Phase-38 witness for the dyadic sponge numeric certificate used by later pairing and surface-type theorems.
proof idea
Definition by list construction, not a proof. Concatenate a singleton genus-125 oriented component, then List.replicate 48 of the small six-face sphere, then three medium twenty-two-face spheres, then a singleton large thirty-face sphere. Each entry is an already-built OrientedPolygonGluingComponent with orientation contradictions set to zero.
why it matters
This roster is the Phase-38 input shared by the dyadic sponge certificate chain. Downstream it feeds: oriented polygon-gluing closure and glued genus 125; componentwise surface inventory and surface-type classification; component pairing closure; the universal combinatorial closed-orientable-surface check on every member; and the Phase-46 concrete embedded-obligation capstone.
In the module narrative it records the orientability gate without claiming the missing regular-neighborhood homeomorphism. The geometric realization and embedded digital-cubical collapse remain open; this definition only freezes the finite oriented component inventory those algebraic wrappers quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.