EmbeddedComponentMapObligationOk
plain-language theorem explainer
A candidate embedded map from a corrected oriented polygon component onto a standard regular-boundary surface is locally valid exactly when its Phase-43 component pair checks out and the four geometric map obligations (incidence, quotient-cell bijection, vertex links, orientation) all hold. Cosmology bridge proofs cite this as the Phase-44 local validity gate. The body is a five-way conjunction of those predicates, not a derived theorem.
Claim. For a candidate embedded map $M$ from a corrected oriented polygon component to a standard regular-boundary surface component, $M$ is locally valid if and only if the underlying Phase-43 component pair is valid (the oriented-polygon certificate succeeds and the polygon Euler characteristic equals the target standard-surface Euler characteristic) and the four geometric obligations hold: incidence preservation, quotient-cell bijectivity, vertex-link preservation, and orientation preservation.
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 identity is that the total desingularized boundary genus equals the first Betti number $b_1$ of the region.
An embedded-map obligation packages one corrected oriented polygon-gluing component together with a target standard surface type, plus four proposition fields (incidence preservation, quotient-cell bijectivity, vertex-link preservation, orientation preservation). Those fields stay as Prop obligations rather than booleans so the file cannot silently assert the missing geometric work. Forgetting the obligation yields the Phase-43 component pair (source, target).
Upstream, a component pair is valid when the oriented-polygon certificate succeeds and the polygon Euler characteristic equals the standard-surface Euler characteristic of the target. The present definition layers the four geometric map obligations on top of that pair check.
proof idea
Pure definitional unfolding: local validity is the conjunction of (i) validity of the forgotten Phase-43 component pair and (ii)–(v) the four geometric proposition fields carried by the obligation structure. No lemmas are applied; the body is the Prop that downstream package-closure and concrete-witness theorems inhabit.
why it matters
Phase 44 local gate for the embedded-component-map layer of the regular-neighborhood genus bridge. Package closure is defined as “every listed map is locally valid” conjoined with Phase-43 component-pairing closure, so this predicate is the per-map atom of that package. Downstream, the local readout theorem extracts local validity from a closed package; the Phase-46 concrete bridge builds a fully discharged obligation from a combinatorial closed-orientable-surface witness plus Euler match; the horizon-torus certificate specializes that bridge to the concrete horizon component. The module status remains partial through Phase 44 and conditional at Phase 47: arithmetic and certificate bridges are closed, while the embedded digital-cubical collapse and the final regular-neighborhood homeomorphism stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.