PolygonComponentClosedQuadrangulation
plain-language theorem explainer
Closed quadrangulation on one polygon-glued surface component means the edge count equals twice the face count. That identity is the combinatorial no-boundary condition for quadrilateral faces: each edge is shared by exactly two faces. Cosmology certificates cite it as one of the four decidable gates for a concrete closed orientable surface witness. The body is a one-line equality on the component's integer cell counts.
Claim. For a polygon-glued surface component $C$ with integer edge count $E$ and face count $F$, the closed-quadrangulation predicate holds precisely when $E = 2F$. Equivalently, counting incidences two ways on a pure quadrangulation with no boundary gives $4F = 2E$.
background
The module builds the algebraic bridge from regular-neighborhood boundaries of positive excursion sets in cubical cosmology to genus equal to the region's first Betti number $b_1$. After raw cubical boundaries showed nonmanifold edges, the readout switched to desingularized regular-neighborhood boundaries; later phases supply finite polygon-gluing and orientability certificates rather than the missing homeomorphism theorem.
A PolygonGluingComponent is one Phase-36 glued surface piece: integer quotient vertices, edges, faces, recorded Euler characteristic, and a local vertex-link audit (link count versus cycle count). Faces are treated as quadrilaterals in the incidence arithmetic.
Closedness is the standard double-counting identity. Each face contributes four edge incidences, so $4F$ total; each interior edge is shared by two faces, so $2E$ incidences. Equality forces $E = 2F$ and rules out free boundary edges.
proof idea
Pure definition: the predicate is the proposition $C.edges = 2 \cdot C.faces$ on the integer fields of the component structure. No lemmas, tactics, or arithmetic reduction beyond that equality. Downstream certificates unfold the name and discharge it by native_decide on concrete numeric components.
why it matters
This is the decidable combinatorial stand-in for "no boundary" inside Phase-44 surface obligations. It is one of the four conjuncts of the concrete closed orientable surface witness (Euler match, cyclic vertex links, successful face-orientation solve, and this closed quadrangulation). concreteObligation wires it directly into the incidencePreserving field of an embedded-component map obligation, replacing opaque placeholders.
Numeric parents include the dyadic genus-125 component, the small/medium/large dyadic sphere components, and the horizon-oriented sphere and torus combinatorial-surface theorems; each unfolds this predicate and decides it. In the broader RS cosmology bridge the module still only certifies finite combinatorial data and Euler/genus arithmetic toward total boundary genus $b_1$; geometric realization of the regular-neighborhood homeomorphism remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.