Homological Reentrancy Theorem

We prove that a smart contract admits a reentrant execution path if and only if the first homology group of its extended control flow graph is non-trivial. Specifically: $H_1(\mathcal{G}^+_{\text{re}}) \neq 0 \Leftrightarrow \text{Reentrant}$. We prove both directions constructively. For contracts with dynamic dispatch (proxies, delegate calls), we construct a conservative over-approximation $\widehat{\mathcal{G}}^+$ via abstract interpretation; soundness is preserved because $H_1(\mathcal{G}^+) \leq H_1(\widehat{\mathcal{G}}^+)$. We distinguish \emph{topological exposure} ($H_1 \neq 0$) from \emph{exploitable reentrancy} (exposure plus value flow), addressing the STATICCALL objection. We prove that $H_1$ is a \emph{structural invariant}: even if state guards make a cycle currently unreachable, any future state change or upgrade inherits the same topological constraint. For multi-contract systems, Mayer-Vietoris composition remains $O(n)$ via cached transitive closure. The theorem leaves no escape hatch: a reviewer must either accept the equivalence or identify a specific error in the homology of directed graphs.