dyadicOrientedSmallSphereComponent
plain-language theorem explainer
Packages the dyadic six-face cube-sphere as an oriented Phase-38 polygon-gluing component: all six faces get signs and the orientation solver reports zero contradictions. Cosmology proofs that need a concrete closed orientable sphere cellulation cite this witness. The body is a structure literal over the existing unoriented six-face polygon component.
Claim. The oriented dyadic small-sphere component is the Phase-38 record whose underlying polygon is the six-face cube-sphere ($V=8$, $E=12$, $F=6$, $\chi=2$, eight cyclic vertex links), with all six faces assigned an orientation and with zero orientation contradictions.
background
This module builds the algebraic bridge from cubical positive-excursion sets to desingularized regular-neighborhood boundaries. After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood of ${q>0}$. Later phases supply finite combinatorial certificates (edge pairing, polygon gluing, orientability) that force boundary genus equal to the region's first Betti number $b_1$, without yet proving homeomorphism to the geometric regular neighborhood.
Phase 36 introduces polygon-gluing components: finite cell counts plus vertex-link cycle audits. The unoriented dyadic six-face sphere is the cube-sphere cellulation with eight vertices, twelve edges, six faces, Euler characteristic $2$, and eight cyclic vertex links. Phase 38 wraps each such component with a face-orientation solve: how many faces received a sign, and how many sign contradictions appeared.
An oriented polygon-gluing component is exactly that triple (polygon data, faces assigned, contradiction count). Success means every face is assigned and the contradiction count is zero.
proof idea
Definitional structure literal, not a proof. It sets the polygon field to the existing dyadic six-face cube-sphere component, sets faces assigned to $6$ (matching the face count), and sets orientation contradictions to $0$. No lemmas or tactics run; the values are the Phase-38 numeric certificate for this sphere.
why it matters
Phase 39's orientability gate needs concrete components on which the face-sign solver succeeds. This definition is the small-sphere witness: six faces fully oriented with no contradictions. Downstream, it is the subject of the theorem that the dyadic six-face sphere is a combinatorial closed orientable surface (discharged by native_decide on the oriented-component predicates). It also appears forty-eight times in the Phase-38 oriented dyadic sponge component list, so the bulk sphere budget of that assembly inherits this orientation certificate.
In the module arc this is still a finite combinatorial certificate, not the missing geometric realization or homeomorphism theorem for regular-neighborhood boundaries. It closes the orientability bookkeeping for the small spheres that dominate the dyadic sponge count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.