The Soundness-Connectedness Correspondence: Type System Soundness as a Topological Invariant\\of the Simply Connected Site

We prove that type system soundness and simple connectedness of the typing context are the same property. Specifically: a type system satisfying the standard formulation (progress and preservation) is sound if and only if the fundamental group of its typing context is trivial ($\pi_1(\Gamma) = 0$). Every known type system unsoundness is exhibited as a non-trivial loop in the typing context, and every non-trivial loop in the typing context is exhibited as a type system unsoundness. This result---the Soundness-Connectedness Correspondence---unifies sixty years of programming language theory under a single topological invariant. We demonstrate the correspondence through the Damas-Hindley-Milner type system, showing that each typing rule (Var, App, Abs, Let, Inst, Gen) is coherent if and only if the simply connected condition holds, and that the Gen rule's side condition ($\alpha \notin \text{free}(\Gamma)$) is precisely the enforcement of $\pi_1 = 0$ at the point of generalization. We extend the correspondence to dependent type theory, substructural type systems, and the transformer architecture of large language models, proving that the $\omega$-inconsistency previously identified in AI systems \cite{eden2025swampland} is type unsoundness at the architectural level: the systems operate on typing contexts with $\pi_1 \neq 0$, producing outputs that typecheck locally at every layer while being globally unsound in composition. The Profinite Safety Core \cite{eden2025psc} is recharacterized as the enforcement of type-theoretic soundness through topological constraint. The correspondence establishes that the simply connected site is not merely a mathematical abstraction but the \textit{necessary and sufficient} condition for coherent computation in any typed system---from ML to military AI