In Hrubeš' Algebraic Monotone Calculus AMC a DNF tautology $A$ is proved by a monotone arithmetic circuit computing $\chi(A)-\epsilon\cdot\chi(1)$ for some $\epsilon>0$, where $\chi(A)$ is the set-multilinear polynomial whose coefficient at $\mathbf x^{\sigma}$ counts the terms of $A$ satisfied by $\sigma$, and $\chi(1)=\prod_{i\le n}(x_i^0+x_i^1)$. Proof size is circuit size, and $\epsilon$ is existentially quantified, so a lower bound must hold at arbitrarily small $\epsilon$. We prove such bounds for bounded-depth fragments by two nonnegative rank measures of $\chi(A)-\epsilon\cdot\chi(1)$: its monotone tensor rank, and the nonnegative rank of a flattening of its coefficient tensor.
At depth three, a proof decomposes the coefficient tensor into nonnegative rank-one tensors. Restricting the summands to nonnegative multiples of subcube indicator tensors yields conical juntas and a system polynomially equivalent to Sherali–Adams when size counts conjunctions over the twin variables $x_i,\bar x_i$. For arbitrary nonnegative rank-one summands, we adapt Rothvoß' hyperplane separation method to monotone tensor rank and prove that Tseitin formulas on constant-degree expanders of sufficiently large girth require proofs of size $2^{\Omega(\epsilon n)}$ for $\epsilon\in(0,1]$ with $\epsilon=\omega(\log n/n)$. This cannot reach every $\epsilon>0$: at shift $2^{-\Theta(n\log n)}$ Tseitin acquires polynomial-size depth-three proofs, which separates the general depth-three fragment from the subcube one exponentially. We compose Tseitin formulas with a constant-size index gadget to obtain lower bounds for every $\epsilon\ge2^{-\Omega(n)}$, converting a Sherali–Adams *degree* bound into a depth-three *size* bound. Depth three is essential to all of this: we also show that Tseitin has monotone proofs of size $O(n^3)$ and depth $O(\log n)$ at *every* $\epsilon\in(0,1]$.
Beyond depth three, we bound the nonnegative rank of a flattening by $L^{2^t}$ for a monotone formula with $L$ leaves and *mixed-product depth* $t$. Here $t$ is the maximum number, along a root-to-leaf path, of product gates whose two inputs each involve both sides of the bipartition; the Tseitin proofs just mentioned have $t=0$ for every bipartition, so this bound is empty for Tseitin. We give two constructions turning hard matrices into hard DNFs. Approximate extension complexity yields bounds for perfect matching and odd factor instances. Linear programming integrality gaps for planted constraint satisfaction yield an explicit family of planted Tseitin DNFs hard at inverse-polynomial shift.
