standardSurfaceEuler
plain-language theorem explainer
Assigns to each standard closed orientable surface of genus g the classical Euler characteristic 2-2g. Cosmology proofs that match polygon-component Euler data to target surfaces cite this as the numeric target. The body is the one-line classical formula on the genus field.
Claim. For a standard closed orientable surface classified by genus $g\in\mathbb{Z}$, the Euler characteristic is $\chi=2-2g$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the desingularized regular-neighborhood boundary: component count $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$. Phases 35–39 reduce polygon-gluing and orientability certificates to that arithmetic, without yet proving homeomorphism to the geometric regular neighborhood.
StandardSurfaceType is the discrete label of a closed orientable surface by a single integer genus. The classical formula $\chi(\Sigma_g)=2-2g$ is the matching target used whenever a combinatorial polygon component is checked against a named surface type.
proof idea
Pure definition: read the integer genus field of the surface type and return $2-2g$. No lemmas, no tactics.
why it matters
Numeric spine of the Phase-35/37/39 component-assembly path. Downstream, ComponentPairOk requires polygon Euler equal to this value; componentPairingEulerTotal sums it over pairings; ClosedSurfaceClassification is the named hypothesis that Euler match plus combinatorial closed-orientable data implies realization by the standard surface; concreteObligationOk_of_surface discharges Phase-44 embedded-map obligations from the same equality. Horizon-annulus and dyadic-sponge certificates close surface-type classification through this formula. It does not touch T0–T8 forcing; it is local topology for the cosmogenesis foam interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.