Your notation is a bit confusing because usually in linear logic and related systems $\top$ denotes the unit of additive conjuction (i.e., categorically, the terminal object), but then when you formulate your question in categorical terms you clearly say that by $\top$ you mean the monoidal unit, which instead is traditionally denoted by $1$ (this is the notation used by Melliès, for instance in his habilitation thesis, see p.83-84).

So, the answer depends on what is $\top$. If it is the terminal object, then $\lnot(\lnot\top\otimes\lnot\top)$ is indeed provable; if it is the monoidal unit (which I am going to denote by $1$ here), then $\lnot(\lnot 1\otimes\lnot 1)$ is not provable.

In the former case, here's a proof: $$ \begin{array}{rcl} \lnot\top & \vdash & \top \\ \hline \lnot\top,\lnot\top & \vdash & \bot \\ \hline \lnot\top\otimes\lnot\top & \vdash & \bot \\ \hline & \vdash & \lnot(\lnot\top\otimes\lnot\top) \\ \end{array} $$

In the latter case, non-provability comes from the non-provability of $1⅋1$ in linear logic without mix. If you want to see it directly in tensorial logic, simply observe that, by cut-elimination (which holds in tensorial logic) and reversibility of the $\lnot$-right and $\otimes$-left rules, derivability of $\vdash\lnot(\lnot 1\otimes\lnot 1)$ is equivalent to derivability of $\lnot 1,\lnot 1\vdash\bot$, which may only come from a proof of $\lnot 1\vdash 1$, which is unprovable because no rule (except cut) admits such a sequent as its conclusion, as shown by a straightforward inspection of the various rules (cf. for instance p.84 of Melliès habilitation thesis).

The formula $\lnot(\lnot 1\otimes\lnot 1)$ is not provable. This is similar to the non-provability of $1⅋1$ in linear logic without mix.

If you want to see it directly in tensorial logic, simply observe that, by cut-elimination (which holds in tensorial logic) and reversibility of the $\lnot$-right and $\otimes$-left rules, derivability of $\vdash\lnot(\lnot 1\otimes\lnot 1)$ is equivalent to derivability of $\lnot 1,\lnot 1\vdash\bot$, which may only come from a proof of $\lnot 1\vdash 1$, which is unprovable because no rule (except cut) admits such a sequent as its conclusion, as shown by a straightforward inspection of the various rules (cf. for instance p.84 of Melliès habilitation thesis).

Your notation is a bit confusing because usually in linear logic and related systems $\top$ denotes the unit of additive conjuction (i.e., categorically, the terminal object), but then when you formulate your question in categorical terms you clearly say that by $\top$ you mean the monoidal unit, which instead is traditionally denoted by $1$ (this is the notation used by Melliès, for instance in his habilitation thesis, see p.83-84).

So, the answer depends on what is $\top$. If it is the terminal object, then $\lnot(\lnot\top\otimes\lnot\top)$ is indeed provable; if it is the monoidal unit (which I am going to denote by $1$ here), then $\lnot(\lnot 1\otimes\lnot 1)$ is not provable.

In the former case, here's a proof (apologies for the formatting, I am using nested \frac's because I don't know if there are any commands for typesetting derivation trees available here on Stack Exchange): $$ \frac{\frac{\frac{\frac{}{\lnot\top\vdash\top}}{\lnot\top,\lnot\top\vdash\bot}}{\lnot\top\otimes\lnot\top\vdash\bot}}{\vdash \lnot(\lnot\top\otimes\lnot\top)} $$

In the latter case, non-provability comes from the non-provability of $1⅋1$ in linear logic without mix. If you want to see it directly in tensorial logic, simply observe that, by cut-elimination (which holds in tensorial logic) and reversibility of the $\lnot$-right and $\otimes$-left rules, derivability of $\vdash\lnot(\lnot 1\otimes\lnot 1)$ is equivalent to derivability of $\lnot 1,\lnot 1\vdash\bot$, which may only come from a proof of $\lnot 1\vdash 1$, which is unprovable because no rule (except cut) admits such a sequent as its conclusion, as shown by a straightforward inspection of the various rules (cf. for instance p.84 of Melliès habilitation thesis).

Your notation is a bit confusing because usually in linear logic and related systems $\top$ denotes the unit of additive conjuction (i.e., categorically, the terminal object), but then when you formulate your question in categorical terms you clearly say that by $\top$ you mean the monoidal unit, which instead is traditionally denoted by $1$ (this is the notation used by Melliès, for instance in his habilitation thesis, see p.83-84).

So, the answer depends on what is $\top$. If it is the terminal object, then $\lnot(\lnot\top\otimes\lnot\top)$ is indeed provable; if it is the monoidal unit (which I am going to denote by $1$ here), then $\lnot(\lnot 1\otimes\lnot 1)$ is not provable.

In the former case, here's a proof: $$ \begin{array}{rcl} \lnot\top & \vdash & \top \\ \hline \lnot\top,\lnot\top & \vdash & \bot \\ \hline \lnot\top\otimes\lnot\top & \vdash & \bot \\ \hline & \vdash & \lnot(\lnot\top\otimes\lnot\top) \\ \end{array} $$

In the latter case, non-provability comes from the non-provability of $1⅋1$ in linear logic without mix. If you want to see it directly in tensorial logic, simply observe that, by cut-elimination (which holds in tensorial logic) and reversibility of the $\lnot$-right and $\otimes$-left rules, derivability of $\vdash\lnot(\lnot 1\otimes\lnot 1)$ is equivalent to derivability of $\lnot 1,\lnot 1\vdash\bot$, which may only come from a proof of $\lnot 1\vdash 1$, which is unprovable because no rule (except cut) admits such a sequent as its conclusion, as shown by a straightforward inspection of the various rules (cf. for instance p.84 of Melliès habilitation thesis).