SurfaceTypeClassificationCloses
plain-language theorem explainer
Standard-surface classification closes when oriented polygon gluing already closes, each component is paired to a matching closed orientable surface type, the type count equals the corrected component count, and the total assigned genus equals the region's first Betti number $b_1$. Phase-40–43 cosmology bridge proofs cite this Prop as the algebraic gate before inventory matching and component pairing. It is a four-conjunct definition, not a proved theorem.
Claim. Given a Betti triple $B=(b_0,b_1,b_2)$, a list $C_s$ of oriented polygon-gluing components, a list $S_s$ of standard closed orientable surface types, and a half-Euler integer $h$, the standard-surface classification closes when: the oriented polygon-gluing certificate closes for $B$, $C_s$, and $h$; the number of surface types equals the corrected count of the underlying polygon components; every zipped pair assigns a matching surface type to its component; and the total genus of $S_s$ equals $b_1$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti data to the genus of its regular-neighborhood boundary. A BettiTriple stores integers $(b_0,b_1,b_2)$ so Euler arithmetic is literal: region Euler is $\chi=b_0-b_1+b_2$. The target identity is that total desingularized boundary genus equals $b_1$, with boundary components $b_0+b_2$ and boundary Euler $2\chi$.
Earlier phases supply finite combinatorial certificates: corrected edge-paired face components (Phase 35), polygon gluing with binary edges and cyclic vertex links (Phase 37), and face-orientation solves with zero contradictions (Phase 38). An oriented polygon-gluing component packages a polygon cell/link audit plus face-assignment and contradiction counts. A standard surface type is just a closed orientable surface classified by its genus $g$, with Euler $2-2g$.
OrientedPolygonGluingCloses already requires every orientation solve to succeed and the forgotten polygon list to close the Phase-37 gluing bridge. The present definition sits one layer above that gate.
proof idea
Pure definition: a Prop that is the conjunction of four conditions. No tactics, no lemmas applied at this site. The first conjunct reuses the oriented polygon-gluing closure predicate. The second equates surface-type list length to the corrected component count after forgetting orientations and mapping polygons to corrected boundary components. The third is a pointwise zip predicate that each oriented component carries its assigned standard surface type. The fourth equates total assigned genus to $B.b_1$. Downstream theorems unfold this conjunction and discharge each arm separately.
why it matters
Phase-40 algebraic gate in the regular-neighborhood boundary genus bridge. Once components are classified by standard surface type with genus total $b_1$, later phases obtain ordered Euler-list equality, aggregate Euler matching the regular-boundary Euler, and component-count equality with the regular-boundary inventory (Phase 42). It is the first hypothesis of ComponentPairingCloses and of the Phase-43 pairing bridge theorem that turns a closed classification into a closed finite component pairing.
Concrete numeric certificates discharge it: the horizon-annulus handle classifies as torus plus sphere, and the dyadic sponge R20 classifies as one genus-125 surface plus 52 spheres. Those certificates feed the cosmogenesis desingularized foam-interface readout.
Framework role is local to the cosmology boundary-genus chain (Phases 27–47). It does not touch T0–T8 forcing, RCL, or the phi ladder. The embedded digital-cubical homeomorphism to the true regular-neighborhood boundary remains open; this only records the combinatorial surface-type layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.