StandardSurfaceType
plain-language theorem explainer
A standard closed orientable surface is recorded by a single integer genus. Cosmology certificates that match corrected polygon components to regular-neighborhood boundary components cite this type as the target side of the pairing. The declaration is a one-field structure with decidable equality; no proof content.
Claim. A standard surface type is a closed orientable surface classified by an integer genus $g \in \mathbb{Z}$. Its 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 topology of the boundary of a regular neighborhood of the positive excursion set. After desingularization, that boundary is expected to be a disjoint union of closed orientable surfaces whose total genus equals $b_1$.
Classical surface theory classifies closed orientable surfaces up to homeomorphism by a single integer genus $g$, with Euler characteristic $2-2g$. The present type is the Lean carrier for that classical label: it holds only the genus, leaving geometric realization to later hypotheses.
Upstream holography notions of ledger-closed plaquettes and glued dominos supply the discrete face data that eventually feed polygon-gluing certificates; they do not define this surface type, but they motivate why a clean combinatorial target is needed once edges are paired and orientations are fixed.
proof idea
Definition only: a structure with one field genus : ℤ, deriving Repr and DecidableEq. No tactics, lemmas, or proof body. Companion definitions in the same module (Euler characteristic $2-2g$, totals over lists of surface types) read this field.
why it matters
Every Phase-43/44 pairing certificate treats this type as the right-hand side of component matching. ClosedSurfaceClassification is the named hypothesis that a corrected oriented polygon component with matching Euler data is realized by a standard surface of this type. ComponentPair and componentPairing zip polygon components against lists of these surfaces; ComponentPairingCloses demands that the inventory of standard surfaces reproduce regular-boundary component count, Euler total, and genus total.
Downstream equalities such as componentPairingEulerTotal_eq_surfaceTypeEulerTotal and the genus analogues reduce pairing bookkeeping to sums over this type. The module status remains partial through Phase 44 and conditional at Phase 47: the arithmetic bridge and certificates are proved, but the embedded homeomorphism from corrected cellulations to the actual regular-neighborhood boundary is still open. This definition is the classical target label those open geometric theorems would discharge against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.