PolygonComponentEulerOk
plain-language theorem explainer
A polygon-glued surface component is Euler-consistent when its recorded Euler number equals V − E + F from the quotient cell counts. Cosmology certificates cite this as the first gate on a closed orientable combinatorial surface. The body is a one-line equality of integer fields on the Phase-36 component structure.
Claim. For a polygon-glued surface component $C$ with integer cell counts $V$, $E$, $F$ and recorded Euler number $\chi$, the predicate holds precisely when $V - E + F = \chi$.
background
This module bridges regular-neighborhood boundary genus for the positive excursion set in the cosmogenesis pipeline. After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood; algebraically one wants boundary components $b_0+b_2$, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
Phase 36 packages one glued surface piece as a structure holding quotient vertex count, split-edge count, face count, a stored Euler integer, and local vertex-link audit counts. The present predicate is the arithmetic consistency check on those cell fields: the classical Euler combination of vertices, edges, and faces must match the recorded $\chi$.
It sits upstream of the Phase-37 polygon-gluing wrapper and the Phase-39 orientability gate. Those wrappers still certify finite combinatorial data, not the missing geometric homeomorphism to the regular-neighborhood boundary.
proof idea
Definitional, not a proof. The predicate is the bare equality vertices - edges + faces = euler on the integer fields of a polygon-gluing component. Downstream theorems discharge it by unfold plus native_decide on concrete numeric witnesses.
why it matters
First conjunct in the concrete closed-orientable-surface witness: cell counts must recover the recorded Euler characteristic, every quotient vertex link is a single cycle, face orientations solve without contradiction, and every edge is shared by exactly two faces. That bundle replaces opaque Phase-44 obligation propositions and feeds concreteObligation.
Numeric parents include the dyadic genus-125 component and the small, medium, and large dyadic sphere components, each proved by decision procedure after unfolding this gate. It also appears in oriented and unoriented dyadic sponge R20 gluing-closure certificates.
Within the module arc (Phases 27–47) this is pure arithmetic scaffolding for the genus bridge toward total desingularized boundary genus $b_1$. The embedded digital-cubical collapse and regular-neighborhood homeomorphism remain open; this only locks the Euler bookkeeping half of the polygon-gluing certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.