Annihilation, Independence, and Residue: Sharp Matching Bounds for the Annihilation Gap and a TxGraffiti Application

Let $G$ be a finite simple graph. The annihilation number $a(G)$ is an efficiently computable upper bound on the independence number $\alpha(G)$. We develop a sharp matching-number theory for the gap $a(G)-\alpha(G)$. The strongest general theorem is the exact closed form $$a(G)-\alpha(G)\leq 2\mu(G)+1- \lceil \sqrt{6 \mu(G)} \rceil \qquad(\mu(G)\geq 1),$$ and the bound is attained for every prescribed matching number. We also prove sharp matching-dependent bounds for forests, bipartite graphs, and K\"onig-Egerv\'ary graphs, with equality constructions, equality certificates, and equality criteria. Finally, we treat a TxGraffiti output as a machine-conjecture case study. Using annihilating decompositions together with the classical Havel-Hakimi residue inequality $res(G)\leq \alpha(G)$, we give an independent proof of the TxGraffiti annihilation-residue inequality $$\alpha(G)\geq \frac{a(G)+res(G)}{\Delta(G)}$$ for every connected graph $G$ of order at least three, show that both hypotheses are necessary, and compare this proof with a recent Caro-Wei approach. We also refine the Caro-Wei annihilation estimate by an explicit nonnegative slack term, identify its equality cases in degree-sequence form, and combine the refinement with our exact matching-number bound to obtain a combined computable bracket for the independence number and a Gupta-residue bound for the annihilation gap.