Length bound for strong Gröbner bases over rings

Let $\mathcal{P}$ be the polynomial algebra under consideration, and let $\mathcal{G}\subset\mathcal{P}\setminus\{0\}$ be a finite set whose polynomials involve monomials of length at most $d\in\mathbb{N}$. Assume that no new polynomials are added to $\mathcal{G}$ while computing a strong Gröbner basis, with respect to a length-compatible monomial ordering, up to length $3d-1$, using the Buchberger algorithm. Length-bound conjecture. Then $\mathcal{G}$ is a finite strong Gröbner basis for the ideal $\langle\mathcal{G}\rangle$. The conjecture proposes a finite certification bound for strong Gröbner bases over rings, extending the familiar bound $2d-1$ from the non-commutative case over fields. Its proof was previously stated as a lemma, but the authors found problems with that proof; the claim remains open despite supporting examples, including an example with bound $3d-1$.