Polynomial consistency-speedup conjecture for bounded-arithmetic theories

Let $S$ be a sound theory whose axioms are definable by a $\Delta^b_1(S^1_2)$ formula, and let $l\in\omega$. A sound theory $T$ whose axioms are definable by a $\Delta^b_1(S^1_2)$ formula should exist such that

$$\left\|\operatorname{Con}_T(\underline{x})\right\|_S>x^l.$$

Polynomial consistency-speedup conjecture. For every sound $\Delta^b_1(S^1_2)$ theory $S$ and every $l\in\omega$, there exists a sound $\Delta^b_1(S^1_2)$ theory $T$ such that

$$\left\|\operatorname{Con}_T(\underline{x})\right\|_S>x^l.$$

This conjecture proposes that arbitrarily large polynomial lower bounds for the $S$-length of consistency statements can still be obtained while both theories have bounded-arithmetic definable axiom sets. The preceding discussion explains why the analogous unrestricted lower-bound theorem does not immediately extend to polynomial-time theories, leaving this bounded-arithmetic formulation as a speculative possibility.