The module-category pullback conjecture for commutative semiring infinity-categories

Let $\mathcal{R}\in\operatorname{CAlg}_{\operatorname{Fin}}$ and let $\mathcal{L}$ be a cyclic commutative algebra over $\mathcal{R}$, meaning a commutative $\operatorname{Fin}$-algebra with essentially surjective map $\mathcal{R}\to\mathcal{L}$. Let $\operatorname{Mod}_{\mathcal{L}}(\operatorname{SymMon}_\infty^\otimes)$ and $\operatorname{Mod}_{\mathcal{R}}(\operatorname{SymMon}_\infty^\otimes)$ denote the corresponding infinity-categories of module objects, and similarly let $\operatorname{Mod}_{\operatorname{Mdl}(\mathcal{L})}(\operatorname{Pr}^{\operatorname{L},\otimes}_\infty)$ and $\operatorname{Mod}_{\operatorname{Mdl}(\mathcal{R})}(\operatorname{Pr}^{\operatorname{L},\otimes}_\infty)$ denote the presentable module categories. Module-category pullback conjecture. The square

\xymatrix{ \operatorname{Mod}_{\mathcal{L}}(\operatorname{SymMon}_\infty^\otimes)\ar[r]\ar[d] &\operatorname{Mod}_{\mathcal{R}}(\operatorname{SymMon}_\infty^\otimes)\ar[d] \\ \operatorname{Mod}_{\operatorname{Mdl}(\mathcal{L})}(\operatorname{Pr}^{\operatorname{L},\otimes}_\infty)\ar[r] &\operatorname{Mod}_{\operatorname{Mdl}(\mathcal{R})}(\operatorname{Pr}^{\operatorname{L},\otimes}_\infty). }

is a pullback square. This proposed extension concerns the full infinity-categories of modules and is described by the authors as harder to prove; the preceding proposition establishes the analogous equivalence on classifying spaces of coherent module structures, but no resolution of this stronger statement is supplied.