singularV2E1
plain-language theorem explainer
Names the elementary singular-edge graph component with two vertices and one edge after four-face edge pairing. Cosmology certificates for the horizon-annulus handle and dyadic sponge cite it as the atomic V2–E1 building block. The body is a one-line structure literal.
Claim. Let a singular graph component be a pair of natural numbers $(v,e)$ counting vertices and edges in one connected component of the singular-edge graph after four-face edge pairing. The standard two-vertex one-edge component is the pair $(v,e)=(2,1)$.
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. Phase 25 saw raw nonmanifold edges on the cubical boundary; Phase 26 switched to the desingularized regular-neighborhood readout. The target identity is that total desingularized boundary genus equals $b_1$.
A SingularGraphComponent records one connected component of the singular-edge graph after the Phase-29 four-face edge pairing step. Only cell counts matter: natural numbers of vertices and edges. It is not yet an embedded geometric object. Phase 30 uses these counts for a vertex-link half-quotient: one vertex lift per pair of singular vertices in the component.
The present constant is the smallest nontrivial such component: two vertices joined by one singular edge.
proof idea
Pure definition: the structure is inhabited by the pair vertices = 2, edges = 1. No lemmas, tactics, or arithmetic are involved.
why it matters
Feeds the Phase-30 singular-edge inventories for the two main numeric certificates in this file. The horizon-annulus handle list is sixty-four copies of this component, supplying exactly the missing sixty-four vertices in the half-vertex quotient. The dyadic sponge list is twenty-four copies of this type plus twenty-one of the four-vertex three-edge type, giving half-vertex quotient $24\cdot 1 + 21\cdot 2 = 66$, matching the Phase-30 vertex delta.
Those inventories sit inside the larger regular-neighborhood genus bridge (Phases 27–44 partial, Phase 47 conditional): corrected Euler data and component counts force total desingularized boundary genus equal to $b_1$. The geometric realization and homeomorphism to the true regular-neighborhood boundary remain open; this constant only supplies the combinatorial atom those certificates count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.