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:
\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).