Isomorphisms Between Impossible and Hard Tasks

If no efficient proof shows that an unprovable arithmetic sentence '$x$ is Kolmogorov random' ('$x{\in}R$') lacks a length $t$ proof, an isomorphism associates for each $x$ impossible and hard tasks: ruling out any proof and length $t$ proofs respectively. This resembles Pudl\'ak's feasible incompleteness. This possible isomorphism implies widely-believed complexity theoretic conjectures hold -- in effect, translating theorems from noncomputability about proof speedup and average-case hardness directly to complexity. Formally, we conjecture: sentence "Peano arithmetic (PA) lacks any length $t$ proof of '$x{\in}R$'" lacks $t^{\mathcal{O}(1)}$ length proofs in any consistent extension $\mathcal{T}$ of PA if and only if $\mathcal{T}$ cannot prove '$x{\in}R$'. If so, tautologies encoding the sentence lack $t^{\mathcal{O}(1)}$ length proofs in any proof system $P$ for $x{\in}R$ sufficiently long (relative to the description of a program enumerating theorems of a theory $\mathcal{T}$ proving '$P$ is sound'). $R$'s density implies: $\texttt{TAUT}{\notin}\textbf{AvgP}$, Feige's hypothesis holds, and, a new conjecture, $P$'s nonoptimality has dense witnesses. If the isomorphism holds for any $\Pi^0$ sentence, $\textbf{PH}$ does not collapse, because the arithmetic hierarchy does not collapse.