The answer to your question depends on what you mean precisely when you say "invertibility proof". If I understand well, when you say "proof" you mean a derivation, that is, a (syntactical) proof in sequent calculus. I take this interpretation otherwise the attribute "without cuts" you are talking about would be meaningless.
Your definition of invertibility for an inference rule is standard and unambiguous. Note however that being invertible is a property in the metalanguage: to prove that an inference rule $\mathsf{r}$ is invertible, you assume that there is a derivation of the conclusion of $\mathsf{r}$, and you have to build a derivation of the premises of $\mathsf{r}$.
Summing up, when you speak of "invertibility proof" you mean that you want to internalize in the object language (i.e., the sequent calculus) the proof that an inference rule $\mathsf{r}$ is invertible. Said differently, you are looking for a derivation in the sequent calculus that shows that a rule is invertible. The only sensible way to do that, provided that the inference rule $\mathsf{r}$ has only one premise, is to build a derivation whose conclusion is the premise of $\mathsf{r}$ and that contains the conclusion of $\mathsf{r}$ inside.
In the casse the inference $\mathsf{r}$ is the "double negation", an "invertibility proof" in the sense explained above exists using cuts, see $(*)$ below. But this is not the end of the story, because you look for an "invertibility proof" without cuts, and this is impossible, as argued in the section just below.
If instead when you say "invertibility proof" wihtout cuts you simply mean that you are looking for a proof of the invertibility of the inference rule "double negation" in the metalnagauge such that all the derivations there are without cuts, then the answer is positive, see the section starting with "Anoter approach..." below.
Strictly speaking, the answer to your question is negative, provided that your question is formulated in the following way, which interprets "invertibility proof without cuts" as a proof in the object language (that is, in the sequent calculus):
If the sequent $\Gamma, (A \to B) \to B \vdash B$ is derivable, is there a cut-free derivation (that is, without cut rules) with conclusion $\Gamma, A \vdash B$ and containing the sequent $\Gamma, (A \to B) \to B \vdash B$?
Indeed, as correctly pointed out by Mauro Allegranza in his comments, a key property of the sequent calculus is that for every inference rule except the cut, every formula occurring in its premises is a subformula of the formulas occurring in its conclusion (you can check it yourself looking at the rules listed in the documentation for Slaney's prover). The cut rule breaks the subformula property because in $$\dfrac{\Gamma, C \vdash B \qquad \Delta \vdash C}{\Gamma, \Delta \vdash B}$$ the formula $C$ (called the cut formula) occurs in the premises $\Gamma, C \vdash B$ and $\Delta \vdash C$, but not in the conclusion $\Gamma, \Delta \vdash B$. Said differently, cut rule is the only inference rule in the sequent calculus that allows you to remove something from the premises.
Therefore, it is impossible to have a cut-free (that is, without cut rules) derivation of $\Gamma, A \vdash B$ that contains the sequent $\Gamma, (A \to B) \to B \vdash B$, even if $\Gamma, (A \to B) \to B \vdash B$ is derivable.
Of course, you can build an "invertibility proof" with cuts: indeed, the derivation below shows that, given a derivation $\pi$ of $\Gamma, (A \to B) \to B \vdash B$, there is a derivation $\pi'$ of $\Gamma, A \vdash B$ containing the sequent $\Gamma, (A \to B) \to B \vdash B$ and with cuts.
$$\tag{$*$} \pi' \ = \ \dfrac { \displaystyle{{} \atop \displaystyle{{\vdots \pi} \atop \Gamma, (A \to B) \to B \vdash B}} \qquad \dfrac {\dfrac{}{A\vdash A}ax \qquad \dfrac{}{B \vdash B}ax} {\dfrac{A, (A \to B) \vdash B}{A \vdash (A \to B \to B}\to_R} \to_L } {\Gamma, A \vdash B} cut $$
but there is a sort of trade-off: if you want $\pi'$ to contain the sequent $\Gamma, (A \to B) \to B \vdash B$ then at least one cut rule must occur.
A fundamental result in the sequent calculus is cut elimination or admissibility of cut: For every derivation of a sequent $\Gamma \vdash C$, there is a cut-free derivation of $\Gamma \vdash C$; moreover, there is an effective procedure to transform the former derivation into the latter. In particular, this result can be applied to the derivation $\pi'$ in $(*)$, so as to obtain a cut-free derivation $\pi''$ of $\Gamma, A \vdash B$. The "problem" is that $\pi''$ does not contain the sequent $\Gamma, (A \to B) \to B \vdash B$, for the reasons explained above. Such a $\pi''$ cannot be considered as an "invertibility proof" of the inference rule "double negation" $$\tag{$\circ$} \dfrac {\Gamma, A \vdash B} {\Gamma, (A \to B) \to B \vdash B} $$ because the sequent $\Gamma, (A \to B) \to B \vdash B$ will not even appear in $\pi''$.
For instance, take $(\circ)$ when $A = B$ and $\Gamma = \emptyset$, and let
$$\pi = \dfrac { \dfrac {\dfrac{}{B \vdash B}ax} {\vdash B \to B} \to_R \qquad \dfrac{}{B \vdash B}ax } {(B \to B) \to B \vdash B} \to_L $$ According to $(*)$, the "invertibility proof" with cuts of the inference rule $(\circ)$ when $A = B$ and $\Gamma = \emptyset$ is
$$ \pi' \ = \ \dfrac { \displaystyle{{} \atop \displaystyle{{\vdots \pi} \atop (B \to B) \to B \vdash B}} \qquad \dfrac {\dfrac{}{A\vdash A}ax \qquad \dfrac{}{B \vdash B}ax} {\dfrac{A, (A \to B) \vdash B}{A \vdash (A \to B \to B}\to_R} \to_L } {\Gamma, A \vdash B} cut $$ which reduces via the cut-elimination procedure to the cut-free derivation
$$ \pi'' \ = \ \dfrac{}{B \vdash B}ax $$
In $\pi''$ the sequent $(B \to B) \to B \vdash B$ never occurs, so by no means $\pi''$ can be seen as a (cut-free) "invertible proof" of the inference rule $(\circ)$ when $A = B$ and $\Gamma = \emptyset$.
Another approach to prove that an inference rule $\mathsf{r}$ is invertible is to take any derivation $\pi$ whose conclusion is the conclusion of $\mathsf{r}$ (you have such a $\pi$ by hypothesis), and show that you can build a derivation $\pi'$ whose conclusion is the premise of $\mathsf{r}$. Such a proof of the invertibility of $ \mathsf{r}$ is in the metalanguage and proceeds in by structural induction on the derivation $\pi$. This means that you have to consider any possible last rule of $\pi$ and then build $\pi'$. The advantage of this approach is that, thanks to cut elimination (see above), you can always yields a cut-free derivation $\pi'$. The problem of this approach is that it yields a proof of the invertibility of $\mathsf{r}$ in the metalanguage, no in the object language (the sequent calculus). If you look at $\pi'$ alone, you cannot conclude that $\pi'$ shows that $\mathsf{r}$ is invertible, for the same reason we have already seen in the previous section (about cut elimination): since $\pi'$ is cut-free, in $\pi'$ the sequent conclusion of $\mathsf{r}$ does not occur.
Concretely, let us apply this method when the inference rule $\mathsf{r}$ is the "double negation" $(\circ)$ seen above. Let $\pi$ be a derivation with conclusion $\Gamma, (A \to B) \to B \vdash B$. By cut elimination, we can suppose that $\pi$ is cut-free without loss of generalization. Our goal is to build a cut-free derivation $\pi'$ with conclusion $\Gamma, (A \to B) \to B \vdash B$. We want to proceed by structural induction on $\pi$. In order to get the right induction hypothesis, we actually prove the following stronger statement:
If there is a cut-free derivation $\pi$ of $\Gamma, (A \to B) \to B \vdash C$ where $C$ is a subformula of $B$, then there is a cut-free derivation $\pi'$ of $\Gamma, A \vdash C$.
We prove this statement by structural induction on $\pi$. Let us consider its last rule $\mathsf{r}_0$. Cases:
$\mathsf{r}_0$ is $\to_L$ introducing $(A \to B) \to B$, that is, $$ \pi = \dfrac { \displaystyle{{} \atop \displaystyle{{\vdots \pi_0} \atop \Gamma \vdash A \to B}} \qquad \displaystyle{{} \atop \displaystyle{{\vdots \pi_1} \atop B \vdash C}} } {\Gamma, (A \to B) \to B \vdash C} \to_L $$ Since the rule $\to_R$ is invertible, from the derivation $\pi_0$ of $\Gamma \vdash A \to B$ above, it follows that there is a derivation $\pi_0'$ with conclusion $\Gamma, A \vdash B$. Thanks to cut elimnation, there is a cut-free derivation $\pi'$ with conclusion $\Gamma, A \vdash B$.
$\mathsf{r}_0$ is an axiom rule, then $$ \pi = \dfrac{}{\Gamma, (A \to B) \to B \vdash C} ax $$ Since $C \neq (A \to B) \to B$ (because $C$ is a subformula of $B$), then $C$ is a formula in $\Gamma$. Hence, the derivation $\pi'$ below concludes this case. $$ \pi' = \dfrac{}{\Gamma, A \vdash C} ax $$
$\mathsf{r}_0$ is a left rule introducing a formula in $\Gamma$ (for simplicity, I only consider the case where $\mathsf{r}_0$ has ony one premise; the case where $\mathsf{r}_0$ is similar), and so $$ \pi = \dfrac {\displaystyle{{} \atop \displaystyle{{\vdots \pi_0} \atop \Gamma_0, (A \to B) \to B \vdash C}}} {\Gamma, (A \to B) \to B \vdash C} \mathsf{r}_0 $$ Since $\pi_0$ is a cut-free derivation smaller than $\pi$ with conclusion $\Gamma_0, (A \to B) \to B \vdash C$, by induction hypothesis there is a cut-free derivation $\pi_0'$ of $\Gamma_0, A \vdash C$. By applying rule $\mathsf{r}_0$ to $\pi_0'$, we get a cut-free derivation $\pi'$ with conclusion $\Gamma, A \vdash C$.
$\mathsf{r}_0$ is a right rule introducing the formula $C$ (for simplicity, I only consider the case where $\mathsf{r}_0$ has ony one premise; the case where $\mathsf{r}_0$ is similar), and so $$ \pi = \dfrac {\displaystyle{{} \atop \displaystyle{{\vdots \pi_0} \atop \Gamma, (A \to B) \to B \vdash C_0}}} {\Gamma, (A \to B) \to B \vdash C} \mathsf{r}_0 $$ Since $\pi_0$ is a cut-free derivation smaller than $\pi$ with conclusion $\Gamma, (A \to B) \to B \vdash C_0$ where $C_0$ is a subformula of $B$, by induction hypothesis there is a cut-free derivation $\pi_0'$ of $\Gamma, A \vdash C_0$. By applying rule $\mathsf{r}_0$ to $\pi_0'$, we get a cut-free derivation $\pi'$ with conclusion $\Gamma, A \vdash C$. $\qquad\qquad \square$
The last case is the one that requires the stronger statement to get the right induction hypothesis, because when $\mathsf{r}_0$ is a right rule the formula on the right of $\vdash$ changes: in the premise of $\mathsf{r}_0$ it is a subformula of the one in the conclusion of $\mathsf{r}_0$.
What you are trying to do at the end of your post to build by induction a cut-free "invertibility proof" of $(\circ)$ does not lead anywhere. I point out some problems in your attempt.
It is not clear on what you are doing the induction. You shuold proceed by structural induction on any derivation $\pi$ with conclusion $\Gamma, (A \to B) \to B \vdash B$, this means that you have to consider any possible last rule of $\pi$ and then build a derivation with conclusion $\Gamma, A \vdash B$. In your attempt you are not doing that.
It seems that you are only considering the case where there is exactly one formula in $\Gamma$; but how would you proceed if in $\Gamma$ there are no formulas, or two formulas, or ten formulas?
There is no reason why you can restrict yourself to "sequent-conclusions that are provable with no weakening on the left"; you have to prove invertibility in the general case, when $\Gamma$ is whatever finite set of formulas.
In Points 2-4 of your attempt, the inference rule you are applying is not a rule of the sequent calculus, according to the definition given in the documentation you refer to for Slaney's prover. By definition, derivations in the sequent calculus are only made of instances of inference rules of the sequent calculus.
