Let $\mathcal{O}^\otimes$ be an $\infty$-operad and $\mathcal{C}^\otimes$ a symmetric monoidal $\infty$-category, both in the sense of Lurie's Higher Algebra. By augmented $\mathcal{O}^\otimes$-algebras in $\mathcal{C}^\otimes$ I mean either of the following: $$ \mathrm{Alg}^{\rm aug}_{\mathcal{O}}(\mathcal{C}^\otimes) := \mathrm{Alg}_{\mathcal{O}}(\mathcal{C}^\otimes)_{/1} \simeq \mathrm{Alg}_\mathcal{O}(\mathcal{C}^\otimes_{/1}) $$ In the latter case $\mathcal{C}^\otimes_{/1}$ has the symmetric monoidal structure coming from the commtative algebra structure of $1$. I would like to find an "augmented envelope": a symmetric monoidal $\infty$-category $\mathrm{Env}_{\rm aug}^\otimes(\mathcal{O}^\otimes)$ such that: $$ \mathrm{Fun}^{\rm strong -\otimes}(\mathrm{Env}_{\rm aug}^\otimes(\mathcal{O}^\otimes), \mathcal{C}^\otimes) \simeq \mathrm{Alg}^{\rm aug}_{\mathcal{O}}(\mathcal{C}^\otimes) . $$
The usual envelope $\mathrm{Env}^\otimes(\mathcal{O}^\otimes)$ has a similar property for non-augmented algebras. It is a symmetric monoidal $\infty$-category whose underlying $\infty$-category is the subcategory $\mathcal{O}_{\rm act}^\otimes \subset \mathcal{O}^\otimes$ and the symmetric monoidal structure can be thought of as "concatenating sequences of colors". In HA.2.2.4.7 Lurie remarks that this symmetric monoidal structure can be extended to all of $\mathcal{O}^\otimes$, but that this won't be needed. I'm fairly convinced that this symmetric monoidal structure should be the augmented envelope I'm looking for: the inert maps should exactly give all the augmentations.
There is also a more category theoretic way of saying what I'm looking for. The envelope $\mathrm{Env}^\otimes$ is the left-adjoint to the forgetful functor $\mathrm{Op}_\infty \leftarrow \mathrm{Cat}_\infty^\otimes$ from symmetric monoidal $\infty$-categories to $\infty$-operads. Similarly, the augmented envelope should be the left-adjoint to the forgetful functor $$ \mathrm{Op}_\infty \longleftarrow \mathrm{Cat}_\infty^{\otimes, 1\rm -term} $$ where the $\mathrm{Cat}_\infty^{\otimes,1\rm -term} \subset \mathrm{Cat}_\infty^\otimes$ is the full subcategory on those $\mathcal{C}^\otimes$ such that $1 \in \mathcal{C}$ is terminal. I think this amounts to the same as above because sending $\mathcal{C}^\otimes$ to $\mathcal{C}^\otimes_{/1}$ should be a colocalisation onto the full subcategory $\mathrm{Cat}_\infty^{\otimes,1\rm -term} \subset \mathrm{Cat}_\infty^\otimes$.
Question: Has such an augmented envelope been constructed or has someone written something about this extended symmetric monoidal structure on $\mathcal{O}^\otimes$ that Lurie mentions?
