correctedComponentCount
plain-language theorem explainer
Counts how many corrected boundary components appear in a finite list, returning that cardinality as an integer. Cosmology proofs that assemble desingularized regular-neighborhood boundaries cite it as the component inventory. The body is the list length, viewed in ℤ.
Claim. For a finite list $C_s$ of corrected boundary components (each recorded only by its Euler characteristic after edge pairing and local vertex-link collapse), the corrected component count is $\# C_s \in \mathbb{Z}$.
background
This module builds the algebraic bridge from a compact 3D cubical region's Betti triple $(b_0,b_1,b_2)$ to the topology of the boundary of a regular neighborhood of the positive excursion set. After Phase 25 found nonmanifold edges on the raw cubical boundary, the canonical readout became that desingularized surface: boundary components $b_0+b_2$, boundary Euler $2(b_0-b_1+b_2)$, and total genus $b_1$.
A CorrectedBoundaryComponent is one connected piece of the corrected boundary after edge pairing and local vertex-link collapse; it stores only an integer Euler characteristic. The count of such pieces is the inventory input to the Phase-35 component-assembly predicate and to the half-Euler genus formula (components minus half-Euler).
Sibling quantities include the total corrected Euler sum, genus-from-half-Euler, and the assembly-closure proposition that matches count and Euler data to the regular-neighborhood formulas for a given Betti triple.
proof idea
Definitional one-liner: the value is the length of the input list, returned at type $\mathbb{Z}$. No lemmas are applied; downstream theorems unfold this name and reduce with simp or native_decide against concrete component lists.
why it matters
This is the component-count leg of the Phase-35 assembly bridge. ComponentAssemblyCloses requires the count to equal regularBoundaryComponents of the region's Betti triple, together with Euler half-sum matching the region Euler. Genus is then read as count minus half-Euler, forcing total desingularized genus $b_1$ when the assembly data hold.
Downstream certificates for the dyadic sponge R20 and the horizon-annulus handle pin the count numerically (e.g. 53 components on the dyadic split). Oriented-polygon and polygon-gluing wrappers preserve list length when forgetting structure down to corrected components, so the same inventory feeds Phases 37 and 39.
The module still leaves open the embedded digital-cubical collapse and homeomorphism of corrected cellulations to true regular-neighborhood components; this definition only supplies the arithmetic headcount those certificates compare against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.