TopoNeSy: Exact Lifetime-Space Verification for Graph-Topological Queries

Feature-space robustness verification can be conservative when candidate feature perturbations have no admissible input realization at the claimed distance. TopoNeSy studies this question for a fixed graph with independently perturbed edge-birth times, a one-dimensional preterminal filtration, and completion at time one. Our main theoretical result is an exact image-and-lift theorem: every clipped ${\ell }_{\infty }$ input ball maps exactly to the ordered ${\ell }_{\infty }$ ball of the same radius around the global $H_1$ lifetime vector, and every target has a constructive input preimage at its distance from the nominal lifetime vector. This strengthens forward stability from an enclosure to exact realizability. Consequently, any frozen lifetime-only query has the same exact flip radius in input and lifetime space. The reduction also permits exact elimination of unused lifetime coordinates. TopoNeSy instantiates the resulting verification interface with jointly trained affine predicates and Boolean DAGs under a no-bypass architecture, deployed with exact rational semantics. Controlled experiments validate reconstruction and computational reduction. On measured EEG connectivity graphs, a frozen full-$H_1$ DAG attains 76.11% balanced accuracy and 67.78% open-ball certified balanced accuracy at edge radius $0.01$, averaged over three seeds. All 720 model/window cases have verified radius intervals of width at most $10^{-5}$ after refinement, with actual graph counterexamples at their upper endpoints. The guarantees concern the stated stored-edge domain, not raw EEG perturbations. Code: https://anonymous.4open.science/r/toponesy-75FF/