The lower-bounds sharpening conjecture

Suppose $T$ is a theory containing $\mathrm{I}\Sigma_1$, $(c,i)\mapsto l_c(i)$ is nondecreasing, and $M_f$ is a computable function for every computable $f$, satisfying:

1. $T \nvdash \forall x\,\exists y\,M_{l_c^{-1}}(x)=y$ for every $c$.
2. If $f(i)\leq g(i)$ for all $i\leq M_g(x)$, then $M_f(x)\leq M_g(x)$.
3. $H$ eventually dominates every function provably total in $T$.

Lower-bounds sharpening conjecture. Then

$$T \nvdash \forall x\,\exists y\,M_h(x)=y,$$

where

$$h(i)=l_{H^{-1}(i)}^{-1}(i).$$

The conjecture seeks to make the lower-bound sharpening argument independent of the particular method used to prove independence of the corresponding identity-parameter statement. Its status is unclear from the supplied text.