embeddedComponentMapInventory_matches_regularBoundary
plain-language theorem explainer
When a finite package of embedded-map obligations closes against a Betti triple, the paired standard surfaces inherit the regular-boundary Euler characteristic and total genus $b_1$. Cosmogenesis certificate authors cite this as the Phase-44 inventory readout linking embedded-map packages to the Phase-43 pairing ledger. The proof is a direct projection of the Euler and genus conjuncts already stored in the closing hypothesis.
Claim. Let $B=(b_0,b_1,b_2)$ be a Betti triple, $M_s$ a finite list of embedded-map obligations (each a candidate map from an oriented polygon-gluing component to a standard surface type, carrying four geometric obligation propositions), and $h\in\mathbb{Z}$ a half-Euler value. If the package closes (every obligation is locally ok, and the underlying Phase-43 component pairing of sources to targets closes at half-Euler $h$), then the total target Euler characteristic of that pairing equals the regular-boundary Euler of $B$, and the total target genus equals $b_1$.
background
This module builds the algebraic bridge for the desingularized readout of a compact 3D cubical positive region: the boundary of a regular neighborhood of ${q>0}$. A BettiTriple records integer Betti numbers $(b_0,b_1,b_2)$ so Euler algebra is literal; the region Euler is $\chi=b_0-b_1+b_2$. The regular-neighborhood boundary is required to have component count $b_0+b_2$, Euler $2\chi$, and total genus $b_1$.
Phase 43 packages oriented polygon-gluing components against standard surface types via an abstract componentPairing (zip of sources and targets). Totals componentPairingEulerTotal and componentPairingGenusTotal sum the target standard-surface Euler and genus over that pairing. Phase 44 lifts each pair to an EmbeddedComponentMapObligation: source, target, and four Prop fields (incidence, quotient-cell bijectivity, vertex-link preservation, orientation) kept as obligations so the file cannot silently assert geometry.
EmbeddedComponentMapObligationsClose is the conjunction of local obligation-ok for every map and ComponentPairingCloses on the projected source/target lists. Closing already encodes classification, local pair validity, component count, Euler match to the regular boundary, and genus match to $b_1$.
proof idea
One-line projection from the closing hypothesis. Destructure the second conjunct of EmbeddedComponentMapObligationsClose (the ComponentPairingCloses package) to obtain its five witnesses; discard classification, pair-validity, and count; return the remaining Euler and genus equalities as the two conjuncts of the goal. No new arithmetic is performed: the inventory identities are already part of the Phase-43 closing data that the embedded package reuses by definition.
why it matters
Phase-44 inventory readout in the regular-neighborhood boundary genus bridge (module Phases 27–47). It records that any closed embedded-map obligation package inherits, definitionally via source/target projection, the same regular-boundary Euler and genus ledger already forced at Phase 43. Downstream geometric work can therefore quote a single closed package and read off $\chi(\partial N)=\mathrm{regularBoundaryEuler}(B)$ and total genus $b_1$ without re-running the pairing algebra.
No used_by edges are registered yet; the declaration is the terminal inventory theorem of the embedded-map layer. The module status remains partial through Phase 44 and conditional at Phase 47: the arithmetic and certificate bridges are proved (0 sorry), but the embedded digital-cubical collapse and the homeomorphism of corrected component cellulations to actual regular-neighborhood boundary components stay open. This lemma does not close those geometric gaps; it only freezes the inventory once the obligation package is assumed closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.