embeddedComponentMapObligationOk_of_embeddedComponentMapObligationsClose
plain-language theorem explainer
From a closed package of embedded component-map obligations, every listed candidate map is locally valid: incidence, quotient-cell bijection, vertex-link, and orientation obligations all hold. Phase-44 auditors of the desingularized regular-neighborhood boundary inventory cite this readout. The proof is a one-line projection of the universal conjunct in the closure predicate.
Claim. Let $B=(b_0,b_1,b_2)$ be a Betti triple, $M_s$ a finite list of candidate embedded maps from oriented polygon-gluing components to standard regular-boundary surfaces, and $h\in\mathbb{Z}$ a half-Euler datum. If the package closes (every map is locally valid and the underlying Phase-43 component pairing closes at half-Euler $h$), then each $M\in M_s$ is locally valid: its Phase-43 pair is valid and the four geometric obligations (incidence preservation, quotient-cell bijection, vertex-link preservation, orientation preservation) hold.
background
This module builds the algebraic bridge for the regular-neighborhood boundary of a compact 3D cubical region. After Phase 25 found nonmanifold edges on the raw positive excursion set, the canonical readout became the boundary of a regular neighborhood of ${q>0}$. A Betti triple $(b_0,b_1,b_2)$ records the region's homology in integers so Euler algebra is literal; the target identities are boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total desingularized genus exactly $b_1$.
An embedded component-map obligation packages one corrected oriented polygon component against one standard surface type, together with four proposition fields (incidence, quotient-cell bijection, vertex links, orientation). Those fields stay as Prop obligations so the file cannot silently assert geometry. Local validity means the underlying Phase-43 component pair is ok and all four obligations hold. Package closure is the conjunction of universal local validity with Phase-43 component-pairing closure at a given half-Euler.
proof idea
One-line term proof. Package closure is definitionally a conjunction whose first factor is $\forall M\in M_s,,\mathrm{Ok}(M)$. Project that conjunct and apply it to the membership hypothesis $M\in M_s$. No further lemmas are needed.
why it matters
Phase 44's local inventory readout: once an embedded-map obligation package closes, every candidate component map carries the full local geometric certificate (incidence, bijection, links, orientation) on top of the Phase-43 pairing. That is the algebraic gate before any claim that corrected polygon components realize regular-neighborhood boundary components.
The module status remains partial through Phase 44 and conditional at Phase 47: arithmetic bridges and numeric certificates are proved, but the embedded digital-cubical collapse and the final regular-neighborhood homeomorphism stay open. No downstream consumers are wired yet; this lemma is the per-component extraction step those later geometric theorems would call. It does not touch the forcing chain (T0–T8), RCL, or the mass ladder; it sits entirely in the cosmogenesis foam-interface desingularization track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.