SETH-K-Finite conjecture on finite random-axiom consistency proofs

Fix a base theory $\mathcal S$ and let $R$ be the set of Kolmogorov-random strings defined using the fixed universal machine and additive constant. Let $N_R^{\mathcal S}$ be the maximum of the three thresholds specified in the source: the least length of a valid $\mathcal S$-proof string, a semantic threshold beyond which $\mathcal S$ proves no sentence of the form $x\in R$, and a syntactic threshold beyond which a proof of length at most $n$ can mention the added axiom $x\in R$. SETH-K-Finite. For every $\epsilon>0$, every $n>N_R^{\mathcal S}$, and every string $x\in\{0,1\}^n$,

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

if and only if

$$\mathcal S\vdash x\in R.$$

The easy implication from provability of the added axiom is established in the surrounding text; the conjecture asserts the converse at the stated subexponential proof-size bound. Its status is not resolved in the supplied material.