CombinatorialClosedOrientableSurface
plain-language theorem explainer
A finite combinatorial certificate that one oriented polygon-gluing component is a closed orientable surface: Euler counts match the recorded χ, every quotient vertex link is a single cycle, the face-orientation solve has no contradictions, and every edge is shared by exactly two faces. Cosmology and foam-interface work cites it as the decidable Phase-44 surface witness. The body is a four-way conjunction of already-defined component audits.
Claim. An oriented polygon-gluing component $C$ is a combinatorial closed orientable surface when (i) its cell counts satisfy $V-E+F=\chi$ as recorded, (ii) every quotient vertex link is a single cycle, (iii) the face-orientation assignment covers every face with zero sign contradictions, and (iv) the gluing is a closed quadrangulation ($E=2F$, each edge shared by exactly two faces).
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 raw cubical boundaries showed nonmanifold edges, the readout switched to the desingularized regular-neighborhood boundary; later phases add polygon-gluing and orientability certificates without yet proving homeomorphism to that geometric boundary.
An oriented polygon-gluing component packages a Phase-36 polygon component (cell counts, Euler data, vertex-link audit) with a Phase-38 face-orientation solve (facesAssigned, orientationContradictions). The four conjuncts are the standard finite checks: Euler identity $V-E+F=\chi$; cyclic links (vertexLinkCycles = vertexLinks); orientation success (every face assigned, zero contradictions); and closed quadrangulation $E=2F$ ("combinatorial no-boundary").
These replace opaque Phase-44 obligation propositions by decidable arithmetic on the component fields.
proof idea
Definition only: the predicate is the conjunction of four existing component audits on $C$ and $C$.polygon. No tactics or lemmas are applied. Downstream certificates typically unfold the name and discharge the four equalities by native_decide on concrete numeric components.
why it matters
Phase 44 needs a concrete closed-orientable-surface witness so embedded-map obligations are not placeholders. This definition is that witness. It feeds concreteObligationOk_of_surface (Phase-46 local bridge: surface plus target Euler match fills every Phase-44 obligation) and the conditional package concreteObligations_realizeStandard under ClosedSurfaceClassification (classical closed-surface classification held as a named hypothesis, never an axiom).
Numeric dyadic certificates (dyadicOrientedGenus125_combinatorialSurface, the small/medium/large sphere components, sponge $R_{20}$) prove the predicate on concrete components. In the broader RS cosmology stack this is the finite combinatorial gate on the regular-neighborhood boundary genus bridge (total desingularized genus $=b_1$), still short of the open geometric realization/homeomorphism theorem flagged in the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.