PolygonComponentHasSurfaceType
plain-language theorem explainer
A finite oriented polygon-gluing component is assigned a standard closed orientable surface of genus g precisely when its face-orientation certificate succeeds and its Euler characteristic equals 2-2g. Cosmology certificates cite this predicate to classify desingularized boundary components (horizon annulus, dyadic sponge). The body is a two-conjunct Prop abbreviation, not a proved theorem.
Claim. An oriented polygon-gluing component $C$ has standard surface type $S$ (genus $g$) when the orientation solver assigns every face with zero sign contradictions and the component Euler characteristic equals the closed-orientable formula $\chi=2-2g$.
background
This module builds the algebraic bridge from cubical positive-excursion sets to desingularized regular-neighborhood boundary genus. After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood of ${q>0}$. The target arithmetic identity is that total desingularized boundary genus equals the region's first Betti number $b_1$.
An oriented polygon-gluing component packages a Phase-36 polygon cell/link audit together with a face-sign solve: number of faces assigned and count of orientation contradictions. The orientation certificate succeeds when every face is assigned and contradictions vanish. A standard surface type is just an integer genus $g$; its Euler number is the classical closed orientable value $2-2g$.
The local setting is combinatorial certificate algebra (Phases 37–39), not a geometric homeomorphism theorem: binary edge gluing, cyclic vertex links, and orientability gates reduce to component-assembly genus identities.
proof idea
Definitional abbreviation only. The predicate is the conjunction of the orientation-success proposition (faces assigned equal the polygon face count and orientation contradictions are zero) with equality of the component's recorded Euler characteristic to $2-2g$ for the chosen standard surface type. No tactics or lemmas fire at this declaration.
why it matters
This is the per-component matching gate inside standard-surface classification. SurfaceTypeClassificationCloses requires every zipped component/type pair to satisfy it, together with oriented polygon-gluing closure, matching component counts, and total type-genus equal to $b_1$. The list-level Euler comparison theorem uses it pointwise to equate ordered polygon Euler signatures with ordered standard-surface Euler signatures.
Concrete cosmology 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 numeric closures feed the regular-neighborhood genus bridge (total boundary genus $=b_1$) used by the foam-interface desingularization pipeline. The geometric realization/homeomorphism to the true regular-neighborhood boundary remains open; this only records the orientable Euler-type match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.