PolygonGluingCloses
plain-language theorem explainer
A finite list of polygon-glued surface components closes against a region's Betti data when every component has correct cell Euler counts, every quotient vertex link is a single cycle, and the Euler-only projection satisfies the Phase-35 component-assembly predicate. Cosmology certificates for the horizon annulus and dyadic sponge cite this gate. It is a pure conjunction of three existing predicates, not a derived equality.
Claim. Given a Betti triple $B=(b_0,b_1,b_2)$, a finite list $C_s$ of polygon-glued components (each recording vertices, edges, faces, Euler number, and vertex-link audit counts), and an integer half-Euler $h$, the polygon-gluing witness closes when: (i) for every component, $V-E+F=\chi$; (ii) for every component, the number of cyclic vertex links equals the number of quotient vertices; (iii) forgetting the polygon audit to Euler-only corrected components yields the Phase-35 assembly data for $B$ at half-Euler $h$ (component count $b_0+b_2$, total Euler $2h$, and $h=b_0-b_1+b_2$).
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple to the genus of its regular-neighborhood boundary. After desingularization (Phase 26) and corrected edge-paired components (Phase 35), the total boundary genus is forced to equal $b_1$ once component count and Euler half-sum match the canonical formulas: boundary components $b_0+b_2$ and boundary Euler $2(b_0-b_1+b_2)$.
Phase 36 supplies a finer combinatorial witness: each surface component is a polygon gluing with explicit cell counts and a vertex-link audit. PolygonComponentEulerOk demands $V-E+F=\chi$ on those counts; PolygonComponentLinksCyclic demands every quotient vertex has exactly one cyclic link. The forgetful map polygonComponentsToCorrected drops the link audit and retains only the Euler data used by Phase 35.
ComponentAssemblyCloses is the Phase-35 gate: corrected component count equals the regular-boundary component count, total corrected Euler equals twice the half-Euler, and that half-Euler equals the region's Euler characteristic. The present definition packages the two polygon-level audits with that assembly predicate.
proof idea
Definitional conjunction only. The body is the meet of three propositions: universal Euler-ok on the polygon list, universal cyclic-link audit on the same list, and ComponentAssemblyCloses applied to the image of the list under the forgetful map to corrected boundary components, at the supplied half-Euler. No lemmas are invoked; downstream certificates discharge it by unfold plus native_decide on concrete numeric witnesses.
why it matters
Phase 37 of the regular-neighborhood boundary bridge: the algebraic wrapper that lets a finite polygon-gluing certificate inherit the Phase-35 total-genus theorem. Downstream, horizonAnnulusHandle_polygonGluingCloses and dyadicSpongeR20_polygonGluingCloses certify the two main numeric models; the oriented wrappers and surface-type classifications thread through this gate; polygonGluedGenus_eq_b1_of_polygonGluingCloses converts closure into the genus equals $b_1$ identity.
In the module's own words, this remains a finite combinatorial certificate, not the missing homeomorphism of corrected cellulations to the geometric regular-neighborhood boundary. It sits in the cosmology desingularized-foam pipeline (Phases 27–47), feeding the genus readout used by the foam-interface scripts. No forcing-chain landmark (T0–T8) is at stake here; the content is pure 3D cubical topology algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.