Proof Circuits

Many of the deepest theorems in mathematics were not proved within a single domain but by transferring the problem through a sequence of domains, applying tools native to each, and returning. We observe that these are instances of a single phenomenon and formalize it.

We define the proof category \(\mathbf{Spec}\), whose objects are spectral domains — triples \(\mathcal{D} = (V, L, \sigma)\) consisting of a Hilbert space, a self-adjoint operator, and a polarity function classifying spectral components as convolutive or correlative. Morphisms are spectral transfers: bounded linear maps preserving spectral structure that may change polarity. Each morphism carries a decorrelation gain \(\delta(\Phi) \in [0,1]\), measuring the fraction of correlative spectral energy converted to convolutive.

We prove that \(\mathbf{Spec}\) is a dagger category enriched over \(([0,1], \geq, \cdot)\) with a symmetric monoidal product. The enrichment yields a composition law: \(\delta(\Phi_2 \circ \Phi_1) \geq 1 - (1-\delta_1)(1-\delta_2)\). A proof circuit is a loop in \(\mathbf{Spec}\) whose total decorrelation gain exceeds a problem-dependent threshold \(\delta^\). We compute \(\delta\) for the principal known transfers (Fourier, analytic continuation, Feynman-Kac, Cholesky, the probabilistic method, Langlands functoriality), draw the explicit transfer graph, classify historical proofs as circuits, characterize the density increment paradigm as iterated circuit composition, identify the missing edges, and prove a residual-based obstruction: in the tight multiplicative regime of the composition proof, no finite circuit of strictly partial steps attains \(\delta^ = 1\).

We implement the framework computationally. The MorphismDSL, built on the Lean 4, discovers cross-domain morphisms at three levels — exact type substitution (L1), structural skeleton similarity (L2), and semantic feature analysis (L3) — and executes theorem transport with 99.7% automatic success rate across 866 verified domain pairs spanning 46 mathematical domains. The kernel's connectivity graph reveals a hub-spoke topology that mirrors the theoretical transfer graph, with probability, topology, and complex analysis as universal connectors.

Keywords: proof circuits, spectral transfer, decorrelation gain, proof category, cross-domain transfer, Langlands program, automated theorem transport, morphism DSL, formal verification

MSC 2020: 18A05, 11-02, 42A85, 60F05, 18M05, 03B35, 68V15