embeddedComponentMapObligationsClose_of_concrete
plain-language theorem explainer
If every oriented polygon component is a concrete closed orientable surface and the Phase-43 component pairing already closes against standard surface types, then the Phase-44 embedded-map obligation package built from those concrete witnesses closes with no placeholders. Cosmology bridge proofs cite this to promote list-level surface certificates into obligation packages. The proof splits the conjunction, discharges each local obligation via the surface-to-obligation lemma, and rewrites source/target maps back to the given pairing.
Claim. Let $B=(b_0,b_1,b_2)$ be Betti data of a compact 3D region, $C_s$ a list of oriented polygon-gluing components, and $S_s$ a list of standard closed orientable surfaces of equal length. Suppose every paired component is a combinatorial closed orientable surface (Euler match, cyclic vertex links, successful face-orientation solve, closed quadrangulation), and the component pairing closes for $B$ at half-Euler $h$. Then the concrete embedded-map obligation list built from $(C_s,S_s)$ closes in the Phase-44 sense at half-Euler $h$.
background
This module is the algebraic regular-neighborhood boundary genus bridge for cosmogenesis foam interfaces (Phases 27–47). After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood of the positive region. The core arithmetic claim is that if a compact 3D cubical region has Betti triple $(b_0,b_1,b_2)$, then the desingularized boundary has $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus exactly $b_1$.
A BettiTriple stores integer Betti numbers so Euler algebra is literal. An oriented polygon-gluing component carries Phase-36 cell/link audits plus face-orientation data. A standard surface type is classified by genus (Euler $2-2g$). CombinatorialClosedOrientableSurface packages the decidable replacements for opaque Phase-44 obligations: recorded Euler from cell counts, cyclic quotient-vertex links, successful orientation solve, and every edge shared by exactly two faces.
ComponentPairingCloses asserts standard-surface classification, local pair validity, and matching of component count, Euler total, and genus total to the regular-boundary inventory of $B$. EmbeddedComponentMapObligationsClose requires every candidate map to satisfy local geometric obligations and the underlying Phase-43 pairing to close. The upstream local bridge concreteObligationOk_of_surface turns one concrete surface witness plus target Euler match into a fully discharged Phase-44 obligation.
proof idea
Term-mode proof of a two-conjunct goal. First conjunct: every concrete obligation in the mapped list is locally OK. Unpack membership via List.mem_map, pull the surface witness from hSurf and the pair-OK fact from hPair, then apply concreteObligationOk_of_surface (Euler match comes from the pair).
Second conjunct: the underlying Phase-43 pairing of sources and targets closes. Rewrite source and target projections of concreteObligations by the length-preserving map lemmas concreteObligations_map_source and concreteObligations_map_target, then finish with the given ComponentPairingCloses hypothesis.
why it matters
Phase 46 list bridge: lifts per-component concrete closed-orientable-surface certificates to a full Phase-44 embedded obligation package with no placeholders. Downstream capstones apply it directly: horizonAnnulusHandle_concreteEmbeddedObligationsClose (torus-plus-sphere package) and dyadicSpongeR20_concreteEmbeddedObligationsClose (genus-125-plus-spheres package), both via apply plus native_decide on the finite hypotheses.
In the module arc this sits after Phase-43 pairing and Phase-44 obligation interfaces, replacing opaque props by decidable combinatorial surface witnesses. It does not finish the geometric story: both downstream docs stress that embedded homeomorphism still needs the classification of closed surfaces, and the module status remains partial through Phase 44 with the digital-cubical collapse open. Within Recognition cosmology this is bookkeeping that certifies desingularized boundary genus against Betti data for concrete foam interfaces, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.