The slightly less bold conjecture on elementary entailment

Let $\Phi$ and $\Psi$ be linear data, and let $\gamma$ be a partial matching map as in the paper. Write $\Phi\vdash'^k_\gamma\Psi$ for entailment using the additional elementary elimination rule, and $\Phi\vdash^{k'}_\gamma\Psi$ for entailment using only the original Cauchy–Schwarz rules. Slightly less bold conjecture. If $\Phi\vdash'^k_\gamma\Psi$, then there exists some $k'\geq0$ such that $\Phi\vdash^{k'}_\gamma\Psi$. This asks whether every entailment obtained from an elementary functional-equation argument can be simulated by repeated Cauchy–Schwarz applications; the source gives no resolution and notes possible difficulties with eliminating non-trivial subexpressions.