horizonAnnulusHandle_realizesStandard
plain-language theorem explainer
Under the classical classification of closed surfaces, the horizon regular-neighborhood boundary realizes componentwise as a standard torus and a standard sphere. Cosmologists tracing the desingularized foam-interface readout would cite this Phase-47 horizon capstone. The proof is a two-conjunct term that feeds each oriented component's combinatorial-surface certificate and Euler match into the classification hypothesis.
Claim. Let $R$ be a realization relation from oriented polygon-gluing components to standard surface types. Assume closed-surface classification for $R$: every closed orientable combinatorial surface $C$ whose Euler characteristic equals that of a standard surface $S$ satisfies $R(C,S)$. Then $R$ holds for the horizon torus component with the standard torus, and for the horizon sphere component with the standard sphere.
background
This module bridges Betti data of a compact 3D cubical region to the genus of its regular-neighborhood boundary. Phase 25 found nonmanifold edges on the raw cubical boundary of the positive excursion set ${q>0}$; the canonical readout is therefore the boundary of a regular neighborhood of the exact positive region. Algebraically one has boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus exactly $b_1$.
An oriented polygon-gluing component packages a Phase-36 polygon cell/link audit with a face-orientation solve (faces assigned, zero orientation contradictions). A standard surface type is classified by genus, with Euler characteristic $2-2g$. The closed-surface classification hypothesis states that any concrete closed orientable combinatorial surface whose Euler matches a standard surface is realized by it (homeomorphic); it is held as an explicit named hypothesis, never an axiom.
Upstream certificates prove the horizon torus and sphere oriented components are combinatorial closed orientable surfaces, by native decision on Euler, cyclic links, orientation success, and closed-quadrangulation predicates.
proof idea
Term-mode pair constructor. Apply the classification hypothesis to the horizon torus component, supplying the combinatorial-surface theorem and a native_decide proof that its polygon Euler equals the standard-torus Euler. Apply it again to the horizon sphere component with the matching sphere combinatorial-surface certificate and Euler check. The two resulting realization facts form the claimed conjunction.
why it matters
Phase-47 horizon capstone: under surface classification, the horizon regular-neighborhood boundary is realized component by component (torus by standard torus, sphere by standard sphere). Module status is PARTIAL through Phase 44 and CONDITIONAL at Phase 47, with zero sorry and zero new axioms. It sits in the cosmology desingularized foam-interface pipeline that feeds foam_interface_desingularized.py. The embedded digital-cubical collapse and the geometric homeomorphism of corrected cellulations to regular-neighborhood components remain open; this only discharges classification-conditional realization for the two horizon annulus-handle components. No downstream dependents are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.