EmbeddedComponentMapObligationsClose
plain-language theorem explainer
Packages the Phase-44 closing condition for a finite list of candidate embedded maps from corrected oriented polygon components onto standard regular-boundary surfaces. Every map must meet its local geometric obligations, and the induced source/target pairing must close in the Phase-43 sense against the region's Betti data and a half-Euler budget. Cosmology bridge proofs cite it as the single Prop that feeds inventory readout and the concrete horizon/dyadic capstones. The body is a two-conjunct definitional abbreviation.
Claim. Given Betti data $B=(b_0,b_1,b_2)$ of a compact 3D region, a finite list $M_s$ of candidate embedded component maps (each from a corrected oriented polygon component to a standard surface type, carrying four geometric obligation propositions), and an integer half-Euler budget $h$, the package closes when every candidate is locally valid and the induced source/target lists form a closed Phase-43 component pairing for $B$ with budget $h$.
background
This module builds the algebraic bridge from a compact cubical 3D region's Betti triple to the genus of its regular-neighborhood boundary. After desingularizing the raw positive-excursion surface, the target inventory is forced: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus exactly $b_1$. Phases 35–43 assemble corrected oriented polygon components and pair them to standard closed surfaces; the embedded digital-cubical homeomorphism remains open.
A BettiTriple is integer Betti data $(b_0,b_1,b_2)$ so Euler algebra is literal. An embedded-map obligation is a candidate map from one corrected oriented polygon component to one standard regular-boundary surface type, with four proposition fields (incidence preservation, quotient-cell bijectivity, vertex-link preservation, orientation preservation) kept as obligations rather than booleans. Local validity means the underlying Phase-43 component pair is valid and all four geometric fields hold. Component pairing closes when the lists come from the standard-surface classification, every pair is locally valid, and the regular-boundary inventory matches component count, Euler, and genus.
proof idea
Definitional abbreviation, not a proved theorem. The predicate is the conjunction of two clauses: universal local validity of every obligation in the list (via the local-ok predicate), and Phase-43 component-pairing closure on the projected source and target lists with the supplied half-Euler integer. No tactics or lemmas fire at the definition site; downstream theorems project either conjunct or rebuild the package from concrete closed-orientable data.
why it matters
Phase-44 gate in the regular-neighborhood boundary genus bridge. It is the single Prop that lets the module treat a list of still-unproved geometric map obligations as a closed algebraic package without silently asserting the missing homeomorphism.
Downstream, the reduction theorem extracts Phase-43 pairing closure from any closed package; the local readout theorem recovers every incidence, bijection, link, and orientation obligation; the inventory theorem inherits regular-boundary Euler and genus from the underlying pairing. Phase-46 then builds concrete packages (no placeholders) for the horizon-annulus handle and the dyadic sponge R20, and proves those packages close. The module status remains partial through Phase 44 and conditional at Phase 47: arithmetic and numeric certificates are in, the embedded geometric realization theorem is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.