CorrectedBoundaryComponent
plain-language theorem explainer
A corrected boundary component is a single connected piece of the desingularized cubical boundary after edge pairing and vertex-link collapse, recorded solely by its Euler characteristic. Cosmology proofs that assemble Phase-34/35 component lists and force total genus equal to b₁ cite this carrier type. It is a one-field data structure, not a proved identity.
Claim. A corrected boundary component is a datum consisting of a single integer $\chi$, the Euler characteristic of one connected component of the corrected (edge-paired, vertex-link-collapsed) boundary surface of a compact cubical region.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the genus of the boundary of a regular neighborhood of the positive excursion set. Raw cubical boundaries can carry nonmanifold edges; the canonical readout is the desingularized regular-neighborhood boundary, whose component count is $b_0+b_2$ and whose Euler characteristic is $2(b_0-b_1+b_2)$, so total genus equals $b_1$.
Phase 31/34 work with a corrected surface obtained by pairing four-face singular edges and collapsing local vertex links. Each resulting connected piece is not stored as a full cell complex here: only its Euler characteristic is needed for the half-Euler and genus arithmetic. Sibling quantities include region Euler $\chi=b_0-b_1+b_2$, regular-boundary component count, and the doubled-boundary Euler identity.
proof idea
Definitional structure with a single integer field euler and derived Repr/DecidableEq. No proof obligations. Downstream code reads the field via list maps and sums when forming total corrected Euler and genus-from-half-Euler.
why it matters
Phase 35's component-assembly bridge needs a uniform carrier for corrected pieces so that count and total Euler can be matched to regular-neighborhood data. ComponentAssemblyCloses packages equality of corrected component count to $b_0+b_2$, total corrected Euler to $2\cdot\mathrm{halfEuler}$, and half-Euler to region Euler; the theorem correctedComponentGenus_eq_b1_of_componentAssemblyCloses then forces total genus equal to $b_1$. Concrete certificates (dyadicSpongeR20CorrectedComponents, genus125Component, horizon-annulus handles) are lists of this type. The geometric homeomorphism of corrected cellulations to true regular-neighborhood components remains open; this type only supports the arithmetic half of that program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.