Safety Composes, but Its Proof Does Not: Exponential Proof-Observability Gaps for Agent Contracts

Can a system be globally safe and computationally easy, yet exponentially hard to certify compositionally? We formalize \emph{proof observability}---the joint state visible to a proof architecture---and show that it can change proof size exponentially without changing behavior. We define a sound, complete, polynomially checkable positive analytic calculus for polarized agent contracts: local provers may be arbitrarily strong, but cross-component reasoning uses only original public variables. We prove linear monotone feasible interpolation, mapping proofs of size $s$ and depth $d$ to public separators of size at most $2s$ and depth at most $2d$. For Delegated Matching, a uniform family of safe deterministic finite-state agent networks of size $O(n^3)$, the exact public safety boundary is bipartite perfect matching and has polynomial unrestricted circuit complexity. Nevertheless, every analytic DAG proof has size $2^{n^{1/3-o(1)}}$, every tree-like proof has size $2^{\Omega(n)}$, and every proof has depth $\Omega(n)$, uniformly over private encodings and owner-local kernels. A behaviorally inert broker exposing $n^2+n$ mixed certificate bits yields an $O(n^3\log n)$ proof under the same kernel while preserving the original trace language exactly; every interface-preserving analytic elimination into the base calculus is again exponentially large. Thus compositional certifiability is governed not only by safety or computation, but by what the proof is allowed to observe.