standardSurfaceType_unique_of_euler
plain-language theorem explainer
Two standard closed orientable surface types with the same Euler characteristic are identical. Cosmology bridge proofs cite this to force the classification target from χ alone rather than by free choice. The proof recovers genus equality from χ = 2−2g by linear arithmetic, then cases on the one-field structure.
Claim. Let $S$ and $S'$ be standard closed orientable surfaces, each classified by a single integer genus. If their Euler characteristics agree, $\chi(S)=\chi(S')$ where $\chi=2-2g$, then $S=S'$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the topology of the boundary of a regular neighborhood of the positive excursion set. After desingularization, boundary components equal $b_0+b_2$, boundary Euler equals $2(b_0-b_1+b_2)$, and total genus collapses to $b_1$.
StandardSurfaceType is the discrete classification target: a closed orientable surface labeled only by its genus $g\in\mathbb{Z}$. Its Euler characteristic is the classical formula $\chi=2-2g$ (standardSurfaceEuler). The surrounding Phase-44/46 material matches polygon-gluing and orientation certificates against this standard type; uniqueness of the type given $\chi$ is what makes the match a determination rather than a selection.
proof idea
From $\texttt{standardSurfaceEuler},S=\texttt{standardSurfaceEuler},S'$, unfold the definition to $2-2\cdot S.\mathrm{genus}=2-2\cdot S'.\mathrm{genus}$. Linear integer arithmetic (omega) yields $S.\mathrm{genus}=S'.\mathrm{genus}$. Case-split on both structure values (each is a single genus field) and finish by simplification: equal genera give equal inhabitants.
why it matters
Doc-comment states the point directly: the classification target is forced by Euler characteristic, not chosen. In the Phase-46 local bridge, a concrete closed-orientable-surface witness plus a target Euler match must discharge every Phase-44 obligation with no placeholder left; this uniqueness lemma is the algebraic half of that forcing.
It sits inside the regular-neighborhood genus bridge (Phases 27–47): once corrected component Euler data equal $2-2g$, the standard type is uniquely fixed, so genus certificates cannot drift between two different labels. No downstream Lean users are wired yet (used_by empty); the lemma is infrastructure for the cosmogenesis foam-interface scripts and later homeomorphism goals. It does not touch T0–T8 forcing, RCL, or the phi ladder; its role is purely the classical surface-classification step inside the cubical cosmology readout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.