Kolmogorov hardness conjecture for random-axiom extensions

Fix a universal Turing machine $U$, a constant $c_U$, and let $R$ be the set of strings $x$ satisfying $K_U(x)\geq |x|-c_U$, where $K_U(x)$ is the plain Kolmogorov complexity of $x$. Let $\mathcal S$ be the base theory, and let $Con_{\mathcal S+(x\in R)}(n)$ denote the bounded consistency statement for the extension by the axiom $x\in R$. Kolmogorov hardness. Whenever $x\in R$ in the standard model,

$$\mathcal S\centernot{\sststile{}{n^{O(1)}}}Con_{\mathcal S+(x\in R)}(n)$$

if and only if

$$EA+Con_{\mathcal S}{\not\vdash}x\in R.$$

Equivalently,

$$\mathcal S\sststile{}{n^{O(1)}}Con_{\mathcal S+(x\in R)}(n)$$

if and only if $EA+Con_{\mathcal S}\vdash x\in R$. This proposes an exact equivalence between efficient simulation and the base theory's ability, over elementary arithmetic plus its consistency, to prove the random axiom; the source explicitly presents it as a candidate information-theoretic hardness principle rather than a theorem.