EmbeddedComponentMapObligation
plain-language theorem explainer
Packages a candidate embedded map from one oriented polygon-gluing component to one standard closed orientable surface of fixed genus. Four proposition fields (incidence, quotient-cell bijection, vertex-link preservation, orientation) record geometric work still owed, kept as Props so the file cannot silently assert them true. Cosmology authors cite it when reducing Phase-44 embedded-map packages to Phase-43 component pairing. Pure structure definition; no proof body.
Claim. An embedded component-map obligation is a 6-tuple $(C,S,P_{\mathrm{inc}},P_{\mathrm{bij}},P_{\mathrm{vl}},P_{\mathrm{or}})$ where $C$ is an oriented polygon-gluing component (Phase-38 face-orientation data on a Phase-36 polygon gluing), $S$ is a standard closed orientable surface classified by genus $g\in\mathbb{Z}$, and the four fields are propositions asserting incidence preservation, quotient-cell bijectivity, vertex-link preservation, and orientation preservation for a candidate embedded map $C\to S$.
background
This module builds the algebraic genus bridge for the desingularized regular-neighborhood boundary of a compact cubical positive region ${q>0}$. After raw cubical boundaries showed nonmanifold edges (Phase 25), the canonical readout is the boundary of a regular neighborhood: component count $b_0+b_2$, Euler characteristic $2(b_0-b_1+b_2)$, and total genus forced to $b_1$. Status is partial through Phase 44 and conditional at Phase 47, with zero sorry and no new axioms; the embedded digital-cubical collapse remains open.
An oriented polygon-gluing component carries a Phase-36 polygon (cell and link audit) plus face-assignment count and orientation-contradiction count from the Phase-38 sign solve. A standard surface type is just a closed orientable surface classified by its genus $g$, with Euler characteristic $2-2g$. Phase 43 pairs such components to standard surfaces algebraically; Phase 44 lifts each pair to a candidate embedded map whose geometric content is still unpaid.
proof idea
Structure definition only: six fields, no constructors beyond the default, no proof tactics. Source and target are the Phase-43 pairing endpoints; the four Prop fields are deliberately not Bool, so nothing in this file can evaluate them to true by computation. Downstream code either forgets the obligation back to a component pair or instantiates the four Props with concrete closed-orientable-surface predicates via concreteObligation.
why it matters
Phase-44 interface object for the regular-neighborhood boundary genus bridge. Parent theorems include componentPairingCloses_of_embeddedComponentMapObligationsClose (if a list of these obligations closes, the underlying finite component pairing closes; "the real embedded homeomorphism theorem must still prove the obligations from geometry") and embeddedComponentMapInventory_matches_regularBoundary (closed obligation packages inherit regular-boundary Euler and genus inventory from the Phase-43 pairing).
concreteObligation / concreteObligations fill the four Props with closed-quadrangulation and related surface conditions; source/target recovery lemmas keep list maps honest. This sits on the path from polygon gluing (Phase 37) and orientability (Phase 39) toward the still-open geometric realization: homeomorphism of corrected component cellulations to regular-neighborhood boundary components. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is pure combinatorial topology scaffolding for the cosmogenesis foam interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.