Extremal dense hard-sequence conjecture for coTHEOREMS

Let $\mathcal{T}$ be the theory used to define $H'$, and let $H'$ be the collection of dense sets of true $\mathcal{T}$-unprovable sentences described in the source. Given a nondeterministic Turing machine $M$ accepting $\texttt{coTHEOREMS}$, consider inputs $\langle\phi_i,1^t\rangle$ with $i$ in a dense subset $H'_M$ of $H'$. Extremal dense hard-sequence conjecture. There exists such a dense subset $H'_M$, and for every sufficiently large $|x|$ depending on $M$ and $\mathcal{T}$, $M$ requires $2^t$ steps for all $t$ on every input $\langle\phi_i,1^t\rangle$ with $i\in H'_M$. This is presented as a stronger form of the preceding conjecture, asserting an exponential lower bound at every parameter $t$ and strengthening the proposed explanation for the absence of optimal proof systems.