SingularGraphComponent
plain-language theorem explainer
Records one connected component of the singular-edge graph after Phase-29 four-face edge pairing, as a pair of natural-number cell counts (vertices, edges). Cosmology bridge proofs cite it when assembling Phase-30 half-vertex quotients for horizon-annulus and dyadic-sponge certificates. It is a pure data carrier: no geometric embedding, only arithmetic inputs to the corrected Euler characteristic.
Claim. A singular-graph component is a pair $(v,e)\in\mathbb{N}\times\mathbb{N}$ giving the vertex and edge cell counts of one connected component of the singular-edge graph obtained after the Phase-29 four-face edge pairing. Counts only; not an embedded complex.
background
The 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 exact positive set ${q>0}$. Phase 25 saw nonmanifold edges on the raw cubical boundary (horizon-annulus handle); Phase 26 switched to the desingularized regular-neighborhood readout. The target identity is that total desingularized boundary genus equals $b_1$.
Phase 29 pairs four-face edges on the raw singular boundary. What remains is a singular-edge graph whose connected components are the objects this structure packages. Phase 30 then applies a vertex-link half-quotient: each component contributes a half-vertex lift equal to half its vertex count, restoring the missing vertex budget so the corrected Euler characteristic matches the canonical CW Euler count of the regular boundary.
Upstream edge lists (diamond 4-neighbour adjacency) and the eight-tick phase space sit in the broader Recognition forcing chain ($D=3$, period 8), but this declaration itself only stores discrete cell counts for the post-pairing singular graph.
proof idea
No proof body: a two-field structure with vertices and edges as natural numbers, deriving Repr and DecidableEq. Downstream code treats instances as pure count carriers (e.g. half-vertex delta is integer division of the vertex field by two).
why it matters
Phase-30 arithmetic lives on lists of these components. halfVertexComponentDelta reads one component's contribution as vertices/2; singularGraphHalfVertexDelta and halfVertexCorrectedEuler sum over a list and add to the edge-only Euler characteristic. The closure predicate HalfVertexQuotientCloses and the bridge theorem halfVertexCorrectedEuler_eq_cw_of_delta_eq_required then assert equality with the Phase-28 regular-boundary CW Euler number once the total delta matches the required vertex budget.
Concrete certificates instantiate the type: horizon-annulus handle uses 64 copies of the two-vertex one-edge component (delta 64); dyadic sponge R20 uses 24 of type V2E1 and 21 of type V4E3 (delta $24\cdot 1+21\cdot 2=66$). Those numeric matches feed the partial theorem through Phase 44 and the conditional Phase-47 story. The module still leaves the embedded digital-cubical collapse and homeomorphism to the true regular-neighborhood boundary open; this structure only supplies the cell-count interface those algebraic bridges need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.