embeddedComponentMapPair
plain-language theorem explainer
Projects an embedded-map obligation down to the bare Phase-43 component pair (oriented polygon component, standard surface type) by discarding the four geometric Prop fields. Cosmology bridge proofs cite it when assembling pairings or checking local validity of candidate maps. The body is a one-line product constructor on source and target.
Claim. Given a candidate embedded map obligation $M$ from one corrected oriented polygon component to one standard regular-boundary surface type (with four unpaid geometric propositions: incidence preservation, quotient-cell bijectivity, vertex-link preservation, orientation preservation), return the underlying component pair $(M.\mathrm{source}, M.\mathrm{target})$.
background
This module builds the algebraic genus bridge for desingularized regular-neighborhood boundaries of positive excursion sets in cubical cosmology (Phases 27–47). After raw cubical boundaries showed nonmanifold edges, the readout switched to the boundary of a regular neighborhood of ${q>0}$. Algebraically, if a compact 3D region has Betti triple $(b_0,b_1,b_2)$, the desingularized boundary has $b_0+b_2$ components, Euler characteristic $2(b_0-b_1+b_2)$, and total genus $b_1$.
A component pair is simply an ordered product of one corrected oriented polygon-gluing component with one standard regular-boundary surface type. An embedded-map obligation packages such a pair together with four proposition fields (incidence-preserving, quotient-cell bijective, vertex-links preserved, orientation-preserving). Those fields stay as Prop so the file cannot silently assert the missing geometric embedding theorem.
Phase 43 works with abstract pairings; the later geometric theorem must replace them by genuine embedded maps. This definition is the forgetful step from obligation to pair.
proof idea
One-line definitional constructor: return the product $(M.\mathrm{source}, M.\mathrm{target})$. No lemmas, tactics, or arithmetic; pure field projection from the obligation structure onto the ComponentPair abbrev.
why it matters
Feeds three local parents: the list-level pairing of embedded obligations, the local-validity predicate that requires both a valid Phase-43 pair and all four geometric obligations, and the theorem equating the embedded-map pairing with the ordinary component pairing of source and target lists.
In the module narrative this is bookkeeping for Phase 43–44 of the regular-neighborhood boundary genus bridge. It keeps certificates honest: pairings used downstream are exactly the source/target data of candidate maps, while incidence, bijectivity, vertex links, and orientation remain unpaid geometric work. The embedded digital-cubical collapse and homeomorphism to regular-neighborhood components stay open; this definition only wires the algebraic side used by the foam-interface desingularization scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.