singularV4E3
plain-language theorem explainer
Named constant for a singular-edge graph component with four vertices and three edges after Phase-29 four-face edge pairing. Cosmology certificates cite it when assembling the dyadic-sponge singular graph (21 copies). The body is a one-line structure literal of cell counts, not a geometric embedding.
Claim. Let a singular-edge graph component be a pair of cell counts $(v,e)\in\mathbb{N}\times\mathbb{N}$. The constant $\mathrm{V4E3}$ is the component with $v=4$ and $e=3$.
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. After raw cubical boundaries showed nonmanifold edges, the readout switched to that desingularized surface; the target identity is that total desingularized boundary genus equals $b_1$.
SingularGraphComponent records one connected component of the singular-edge graph after the Phase-29 four-face edge pairing step. Only vertex and edge cell counts are stored; the structure is not an embedded geometric complex. Phase 30 then uses each such component's counts for a half-vertex quotient contribution (one vertex lift per pair of singular vertices).
The local setting is combinatorial arithmetic for foam-interface desingularization certificates, not a homeomorphism theorem for the corrected cellulations.
proof idea
Definition by structure literal: set vertices := 4 and edges := 3 on SingularGraphComponent. No lemmas, tactics, or proof obligations.
why it matters
Feeds dyadicSpongeR20SingularComponents, the Phase-30 singular-edge graph for the dyadic sponge: twenty-four V2E1 components and twenty-one copies of this V4E3 type. That list yields half-vertex quotient $24\cdot 1 + 21\cdot 2 = 66$, matching the Phase-30 vertex delta.
Phase 35 then uses corrected component counts and Euler half-sums to force total genus $b_1$; this constant is one of the concrete component types in those numeric certificates. It does not close the still-open embedded digital-cubical collapse or regular-neighborhood homeomorphism theorems flagged in the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.