componentPairingCloses_of_embeddedComponentMapObligationsClose
plain-language theorem explainer
If a finite package of embedded component-map obligations closes, the underlying component pairing between source polygon components and target standard surfaces closes. Cosmology bridge authors cite this when reducing Phase-44 embedded-map certificates to the Phase-43 pairing inventory. The proof is a one-line projection of the second conjunct of the closing predicate.
Claim. Let $B=(b_0,b_1,b_2)$ be a Betti triple, $M_s$ a list of embedded component-map obligations, and $h\in\mathbb{Z}$ a half-Euler value. If the embedded-map obligations close for $B$, $M_s$, and $h$ (every candidate map meets its local geometric obligations, and the underlying pairing closes), then the component pairing of the source oriented polygon-gluing components with the target standard surface types closes at the same half-Euler value.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti data to the genus of its regular-neighborhood boundary. A BettiTriple is integer Betti numbers $(b_0,b_1,b_2)$ so Euler algebra is literal: region Euler is $\chi=b_0-b_1+b_2$. The target readout is that the desingularized boundary has $b_0+b_2$ components, Euler $2\chi$, and total genus exactly $b_1$.
Phase 43 packages finite pairings of oriented polygon-gluing components with standard surface types. A pairing closes when surface-type classification closes, every local pair is valid, and inventory matches regular-boundary component count, Euler, and genus $b_1$.
Phase 44 lifts each candidate pair to an embedded-map obligation: source component, target surface type, plus four Prop fields (incidence, quotient-cell bijection, vertex-link preservation, orientation). Obligations close when every map is locally ok and the underlying Phase-43 pairing closes. Those four fields stay as propositions so this file cannot silently assert geometry.
proof idea
One-line term projection. By definition, embedded-map obligations close if and only if (i) every obligation in the list is locally ok and (ii) ComponentPairingCloses holds on the mapped source and target lists at the given half-Euler. The hypothesis is that conjunction; the goal is exactly conjunct (ii). The proof is h.2.
why it matters
Phase 44 reduction step in the regular-neighborhood boundary genus bridge (module Phases 27–47). It separates the combinatorial pairing certificate from the still-open embedded homeomorphism theorem: once geometry supplies the four local obligations per map, the pairing inventory (component count, Euler, genus $=b_1$) is already closed by definition.
No downstream consumers are wired yet in the graph. The parent narrative is the algebraic half of cosmogenesis foam desingularization used by the desingularized interface scripts: raw singular cubical boundaries are replaced by regular-neighborhood readout, then finite certificates force total boundary genus $b_1$. The doc-comment is explicit that the real embedded homeomorphism theorem must still prove the obligations from geometry; this lemma only peels the pairing conjunct off the obligation package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.