ComponentAssemblyCloses
plain-language theorem explainer
Predicate asserting that a list of corrected boundary components matches the regular-neighborhood assembly data of a compact 3D region: same component count, total Euler equal to twice a half-Euler, and that half-Euler equal to the region's Euler characteristic. Cosmogenesis and foam-interface work cite it as the Phase-35 algebraic gate. It is a pure Prop packaging three integer equalities; no proof content beyond the conjunction.
Claim. A list $C$ of corrected boundary components (each carrying an Euler characteristic) has the regular-neighborhood component-assembly data for a compact 3D region with Betti triple $B=(b_0,b_1,b_2)$ and half-Euler $h\in\mathbb{Z}$ when: the length of $C$ equals the predicted regular-boundary component count of $B$; the sum of Euler characteristics over $C$ equals $2h$; and $h$ equals the region Euler $\chi(B)=b_0-b_1+b_2$.
background
This module builds the algebraic bridge from desingularized regular-neighborhood boundaries of positive cubical excursion sets to genus equal to $b_1$. After Phase 25 found nonmanifold edges on raw cubical boundaries, Phase 26 switched to the boundary of a regular neighborhood of the exact positive region. The target identities are: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$.
A BettiTriple stores integer Betti numbers $(b_0,b_1,b_2)$ so Euler algebra is literal; region Euler is $\chi=b_0-b_1+b_2$. A corrected boundary component is one connected piece after edge pairing and local vertex-link collapse, represented only by its Euler characteristic. Corrected component count is list length; corrected component Euler is the sum of those Euler values. The half-Euler is kept explicit to avoid hiding the doubled-boundary relation behind integer division.
Phase 35 packages the algebraic half of component assembly: if corrected edge-paired face components already carry the canonical count and Euler half-sum, their total genus is forced to $b_1$. Geometric homeomorphism of those cellulations to the true regular-neighborhood components remains open.
proof idea
Definitional Prop, not a proved theorem. The body is the conjunction of three equalities: corrected component count equals the regular-boundary component count of $B$; corrected component Euler equals twice the supplied half-Euler; and that half-Euler equals region Euler of $B$. Downstream theorems unfold this predicate and discharge the three limbs by native_decide on concrete certificates, or by rcases when deriving genus $=b_1$.
why it matters
Phase-35 gate in the regular-neighborhood genus bridge. The parent theorem correctedComponentGenus_eq_b1_of_componentAssemblyCloses states that once this predicate holds, total component genus from half-Euler equals $b_1$. Numeric certificates close it for the horizon-annulus handle (half-Euler $1$, genus one) and the dyadic sponge R20 (half-Euler $-72$, genus $125$).
Later phases wrap it: polygon-gluing (Phase 36/37), oriented polygon-gluing (Phase 38/39), and surface-type classification all reduce to this assembly predicate. Module status is partial through Phase 44 and conditional at Phase 47 (zero sorry, zero new axiom). It does not close the embedded digital-cubical collapse or the homeomorphism of corrected cellulations to regular-neighborhood components; those remain open geometric realization goals. Landmark contact is cosmological foam topology rather than the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.