embeddedComponentMapPairing_eq_componentPairing

This module builds the algebraic bridge for the desingularized regular-neighborhood boundary of a compact 3D cubical positive region. After raw cubical boundaries showed nonmanifold edges, 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$.

An embedded component-map obligation packages one corrected oriented polygon-gluing component, one standard regular-boundary surface type, and four proposition fields (incidence preservation, quotient-cell bijectivity, vertex-link preservation, orientation preservation). Those fields stay as Prop obligations so the file cannot silently assert the missing geometric homeomorphism.

Forgetting an obligation yields the Phase-43 component pair (source, target). The embedded pairing is the list of those forgotten pairs; the ordinary component pairing is the zip of a source list with a target list. The later geometric theorem must still replace this abstract pairing by a true embedded map.

List induction on the obligation list. The empty case is definitional reflexivity: both sides are the empty list of pairs. In the cons step, both sides unfold to the forgotten pair of the head obligation consed onto the pairing of the tail; the inductive hypothesis rewrites the tail, and the goal closes. No external lemmas are required beyond the definitions of the two pairings and the forgetful map from obligation to pair.

Phase 44 records that if embedded component-map obligations close, the underlying finite component pairing closes. This theorem is the definitional half of that reduction: the embedded pairing is literally the Phase-43 zip of sources and targets, so any certificate stated on embedded obligations transfers to the ordinary pairing used by earlier genus and Euler bridges.

The module status remains partial through Phase 44 and conditional at Phase 47: arithmetic and certificate wrappers are proved, but the embedded digital-cubical collapse and the real regular-neighborhood homeomorphism stay open. The four geometric fields on each obligation are exactly the work still owed. No downstream consumers are wired yet; the lemma is infrastructure for that Phase-44 closure path rather than a forcing-chain (T0–T8) step.