Does focused proof search ever have to backtrack across the choice of focus formula?
Yes, backtracking in focused proof search may be necessary due to a wrong choice of focus formula.  Consider the provable sequent
$$\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot.$$
Choosing to focus on $p\otimes q$ leads to a dead end, because however you &quot;split&quot; the context you end up with an atom ($p$ or $q$) without matching dual.  So $(p^\bot\mathrel{\wp} q^\bot)\otimes r$ must be decomposed first.

A side remark, not directly related to the question but which gives some  further context: the formula $p\otimes q$ above is known to proof net connoisseurs as a &quot;non-splitting tensor&quot;.  When showing that proof nets (in the sense of suitably labelled graphs satisfying certain connectivity and acyclicity conditions) correspond to sequent calculus proofs (the sequentialization theorem) one must at some point prove the non-trivial &quot;splitting lemma&quot;: if the conclusions of a proof net come only from axiom or tensor nodes, then there is one such tensor node which is &quot;splitting&quot;, in the sense that removing it decomposes the proof net into two connected components which are themselves proof nets (this allows sequentialization to be proved inductively).  One of course may wonder whether all tensors are always splitting, and the above is the minimal counterexample.
In terms of proof nets, focusing strengthens the splitting lemma by adding that there always exists a &quot;hereditarily splitting tensor&quot;, in the sense that there is a tensor node such that all tensor nodes directly above it have the splitting property.