dyadicOrientedLargeSphereComponent
plain-language theorem explainer
Packages the dyadic thirty-face sphere as an oriented Phase-38 polygon-gluing component: full face assignment (30) and zero orientation contradictions on the Phase-36 cell audit. Cosmology proofs cite it when assembling the R20 sponge component list or certifying a closed orientable combinatorial surface. The body is a structure literal wrapping the unoriented large-sphere certificate.
Claim. The oriented dyadic large-sphere component is the Phase-38 record whose underlying polygon is the thirty-face dyadic sphere ($V=32$, $E=60$, $F=30$, $\chi=2$, cyclic vertex links), with all $30$ faces orientation-assigned and $0$ orientation contradictions.
background
This module builds the algebraic bridge from cubical positive-excursion topology to desingularized regular-neighborhood boundary genus. After Phase 25 found nonmanifold edges on the raw cubical boundary, Phase 26 switched to the regular-neighborhood readout; later phases supply finite combinatorial certificates (edge pairing, polygon gluing, orientability) that force total boundary genus equal to $b_1$, without yet proving homeomorphism to the geometric regular neighborhood.
Phase 36 supplies PolygonGluingComponent cell and link audits. The upstream dyadic large-sphere component is the thirty-face sphere certificate: $32$ vertices, $60$ edges, $30$ faces, Euler characteristic $2$, and $32$ cyclic vertex links. Phase 38 wraps each such component in an oriented record: the polygon audit plus facesAssigned and orientationContradictions from the face-sign constraint solve. Success means every face gets a sign and no contradiction appears.
proof idea
Definition by structure literal, not a proof. It sets polygon to the Phase-36 dyadic thirty-face sphere component, facesAssigned to $30$ (one per face), and orientationContradictions to $0$. No tactics or lemmas are invoked; the values are the numeric Phase-38 orientability witness for that sphere.
why it matters
Phase 39's module doc states that if every polygon component has a full face-orientation assignment with zero contradictions, the oriented certificate inherits the Phase-37 polygon-gluing genus theorem. This definition is that witness for the large sphere in the dyadic R20 sponge assembly.
Downstream, dyadicSpongeR20OrientedPolygonComponents includes it once beside the genus-$125$ component, $48$ small spheres, and $3$ medium spheres. The theorem dyadicOrientedLargeSphere_combinatorialSurface then proves it is a concrete closed orientable surface by native_decide on the combinatorial surface predicates. It records the orientability gate only; the embedded digital-cubical collapse and regular-neighborhood homeomorphism remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.