horizonOrientedSphereComponent
plain-language theorem explainer
Packages the Phase-38 horizon sphere as an oriented polygon-gluing component: the Phase-36 sphere cellulation with every face signed and zero orientation contradictions. Cosmology auditors cite it when checking that the desingularized horizon boundary splits into an oriented sphere plus torus. The body is a structure literal over the prior sphere polygon witness.
Claim. The horizon sphere component is the oriented polygon-gluing datum whose underlying polygon is the Phase-36 horizon sphere cellulation ($V=2484$, $E=4964$, $F=2482$, $\chi=2$, all vertex links cyclic), with $2482$ faces assigned a sign and $0$ orientation contradictions.
background
This module bridges cubical positive-excursion topology to a desingularized regular-neighborhood boundary. After raw cubical boundaries showed nonmanifold edges (Phase 25), the readout became 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 desingularized boundary has $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
Phase 36 supplies finite polygon-gluing certificates (binary edge gluing, cyclic vertex links, corrected Euler data). Phase 38 adds orientability: each component carries a full face-orientation assignment and a contradiction count. An oriented polygon-gluing component is a structure with a polygon field plus facesAssigned and orientationContradictions.
The upstream sphere polygon already records a spherical cellulation (Euler $2$, every vertex link a cycle). The present definition only attaches the Phase-38 orientation witness to that sphere.
proof idea
Definition by structure literal, not a proof. It sets the polygon field to the Phase-36 horizon sphere polygon component and records facesAssigned $= 2482$ (one sign per face) with orientationContradictions $= 0$. No tactics or lemmas are invoked; downstream theorems discharge the oriented-component predicates by native_decide on these numeric fields.
why it matters
Phase 39 wraps Phase-38 orientability so that a fully oriented polygon component with zero contradictions inherits the Phase-37 genus theorem. This definition is the sphere half of that witness list: it appears in the two-element list of oriented horizon components (torus plus sphere) and is the subject of the combinatorial closed-orientable-surface certificate for the sphere.
The Phase-47 conditional capstone then uses closed-surface classification to realize the horizon regular-neighborhood boundary componentwise: the torus component as the standard torus and this sphere component as the standard sphere. The geometric homeomorphism to the true regular-neighborhood boundary remains open; only the finite combinatorial and orientation certificates are closed here. Framework context is the cosmology foam-interface desingularization pipeline, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.