Verified Attenuated Modus Ponens: A Depth-Bounded Safety Primitive for Contradiction-Tolerant AI Systems

Frontier AI systems increasingly act in settings of moral and regulatory contradiction, where classical reasoning explodes and existing mitigations provide no formal guarantee about behavior while the contradiction is unresolved. This is the regime where human oversight is hardest and audit primitives are most needed. We prove a depth-bounded safety theorem for AI systems reasoning paraconsistently. Formulas carry graded contradiction values $\alpha$ in a bilattice semantics; high-stakes action-licensing rules carry firing thresholds $\vartheta$; inference steps are governed by collapse classes with per-step contradiction tensions $T(H)$. We define VAMP (Verified Attenuated Modus Ponens), a calculus in which each inference step satisfies a local additive verification condition relating the contradiction grade of a conclusion to the grades of its premises and the tension of its governing class. The central result is a budget domination theorem: VAMP-valid proof objects admit a recursive contradiction budget $B(v)$ that bounds formula-level grades at every node. No high-stakes rule may fire at a node whose budget remains below the minimum threshold across the high-stakes rule set, with explicit bounds for chain and tree-shaped derivations. The verification regime is motivated by a structural impossibility: the natural max-form non-expansion desideratum for paraconsistent inference fails for action-licensing implication under any reasonable graded semantics. Rather than weaken the system, we recast the desideratum as a per-step additive side condition, locally checked at each inferential step. This converts a negative result into an audit primitive: contradiction becomes a quantity flowing through inference at a bounded rate, and reasoning safety becomes a budget in that flow. We specify VAMP as a linear-time audit procedure over finite proof objects, distinguishing descriptive nodes from action-licensing nodes, and illustrate the construction on cross-jurisdictional content moderation. We are explicit about scope: the theorem bounds derivability of high-stakes consequences at bounded depth, not real-world harm; collapse-class selection and threshold setting remain normative-design choices outside the formalism. The contribution is a verifiable safety primitive for contradiction-tolerant AI systems and a governance interface where normative commitments about contradiction tolerance become explicit, parameterized, and subject to oversight.