ClosedSurfaceClassification
plain-language theorem explainer
Classical closed-orientable-surface classification, packaged as a named hypothesis on a realization relation R. R(C,S) means the geometric realization of combinatorial component C is homeomorphic to the standard surface S of matching genus. Phase-47 conditional homeomorphism theorems (horizon annulus, dyadic sponge) take this as input. Pure Prop definition: no proof content, never promoted to an axiom.
Claim. For a relation $R$ between oriented polygon-gluing components and standard surface types, the closed-surface classification hypothesis asserts: whenever $C$ is a combinatorial closed orientable surface and the Euler characteristic of $C$ equals $2-2g$ for the standard surface $S$ of genus $g$, then $R(C,S)$ holds.
background
This module builds the algebraic bridge from cubical positive-excursion regions to desingularized regular-neighborhood boundaries (Phases 27–47). After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood of ${q>0}$. Algebraic identities force boundary genus equal to the region's first Betti number $b_1$, but geometric realization remains open.
An oriented polygon-gluing component packages a Phase-36 polygon cellulation with a Phase-38 face-orientation certificate (every face signed, zero contradictions). A standard surface type is just an integer genus $g$, with Euler characteristic $2-2g$. The combinatorial closed-orientable-surface predicate is the decidable stand-in for a closed surface: Euler data match, every quotient vertex link is a single cycle, orientation succeeds, and every edge is shared by exactly two faces.
proof idea
Definition only: no tactics, no lemmas. The body is the universal quantification that every oriented polygon component satisfying the combinatorial closed-orientable-surface predicate, whose polygon Euler characteristic equals the standard formula $2-2g$, is related by $R$ to the corresponding standard surface type. Downstream theorems treat an assumption of this Prop as the classical classification hypothesis.
why it matters
Phase-47 capstones are conditional on this hypothesis. The one-component wrapper realizesStandard_of_surface applies it directly; concreteObligations_realizeStandard lifts it to a whole paired obligation package; the horizon-annulus and dyadic-sponge theorems then conclude componentwise realization (torus plus sphere; one genus-125 surface plus 52 spheres).
Module status is explicit: PARTIAL through Phase 44, CONDITIONAL at Phase 47, zero sorry and zero new axioms. The classical classification is held as an external hypothesis, never internalized as an RS axiom. This keeps the arithmetic genus bridge and numeric certificates clean while marking the missing geometric homeomorphism theorem as the remaining open step (embedded digital-cubical collapse and regular-neighborhood realization).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.