embeddedComponentMapPairing
plain-language theorem explainer
Maps a list of candidate embedded component-map obligations to the ordered list of abstract (source, target) component pairs they are meant to realize. Cosmology certificate authors cite it when lifting Phase-43 pairings from geometric obligation records. The body is a one-line list map through the single-obligation forgetful projection.
Claim. Given a finite list $M_s$ of candidate embedded maps (each pairing one corrected oriented polygon component with one standard regular-boundary surface type, together with four unpaid geometric propositions), return the ordered list of pairs $(\mathrm{source},\mathrm{target})$ obtained by forgetting those geometric obligations.
background
This module builds the algebraic bridge for the desingularized regular-neighborhood boundary of a compact 3D cubical positive region. After Phase 25 found nonmanifold edges on the raw cubical boundary, the readout switched to the boundary of a regular neighborhood; the target identities are boundary components $b_0+b_2$, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
A ComponentPair is just a product of one corrected oriented polygon-gluing component with one standard surface type: the abstract pairing used by current certificates until a true embedded map exists. An EmbeddedComponentMapObligation packages that pair together with four proposition fields (incidence preservation, quotient-cell bijectivity, vertex-link preservation, orientation preservation) kept as Prop so the file cannot silently assert them.
The single-item forgetful map sends each obligation to its $(source,target)$ pair. The present definition lifts that forgetful map to lists.
proof idea
One-line definitional wrapper: apply the list functor map to the forgetful projection that sends each embedded-map obligation to the component pair $(M.source, M.target)$. No tactics, no lemmas beyond that projection.
why it matters
Feeds the equality theorem that the obligation pairing is definitionally the component pairing of the projected source and target lists. That equality lets later certificate steps treat geometric obligation records and abstract Phase-43 pairings interchangeably at the list level.
In the module arc this sits inside the Phase-43/44 embedded-map layer: algebraic wrappers and numeric certificates are closed, but the embedded digital-cubical collapse and the homeomorphism of corrected cellulations to regular-neighborhood boundary components remain open. The definition keeps geometric work as unpaid propositions while still exposing the ordered pairing the genus bridge needs.
It does not touch the forcing chain (T0–T8), RCL, or the mass ladder; it is pure combinatorial bookkeeping for the cosmogenesis foam-interface desingularization path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.