What is the logical status of the sentence combining the ideas of Löb and Rosser, "this sentence is provable before any proof of its negation"? Logicians are familiar with the variety of self-referential sentences expressible in the language of arithmetic:

*

*The Gödel sentence, "this sentence is not provable", which indeed is not provable in whichever base theory that was used when formulating it and hence is true yet unprovable.


*The Rosser sentence, "for any proof of this sentence there is a smaller proof of its negation," which is also true and unprovable. This sentence offers a technical improvement on the Gödel sentence in that the independence of the Rosser sentence can be proved assuming only the consistency of the base theory, whereas Gödel has used $\omega$-consistency.


*The Löb sentence, "this sentence is provable," is indeed provable, remarkably, by Löb's theorem.
My question is about the sentence that we might form by combining the ideas of Rosser and Löb. Namely, by the usual fixed-point methods, we can form a sentence $\zeta$ that PA provably asserts:
$\qquad$"$\zeta$ is provable in PA by a proof that is smaller than any proof of $\neg\zeta$."
We mean "smaller" here, just as with the Rosser sentence, in the sense of the Gödel codes of the proof.
Question. What is the logical status of the combined Rosser-Löb sentence $\zeta$? Is it provable, independent, or what?
The usual arguments for the Rosser and Löb sentences don't seem to gain any traction on the combined sentence.
This question grew out of discussion on Twitter concerning the recent question of Henry Yuen on MathOverflow, Will this Turing machine find a proof of its halting? and several comments on my answer there.
Namely, one can formulate a version of the question above in the context of computability (and Akiva Weinberger did so in the Twitter thread), by considering the Turing machine program $z$ that searches for proofs that $z$ halts or does not halt, and if it finds a proof of halting before finding any proof of nonhalting, then it halts. Does $z$ halt?
 A: As Akiva Weinberger and Will Sawin have already pointed out, the answer does depend on the details of the of the formalisation of the notion of proof.
Let's fix some terminology: Given a proof predicate $\mathrm{Prf}_\tau(x,y)$, the corresponding provability predicate $\mathrm{Pr}_\tau(x)$ is defined as $\exists y \mathrm{Prf}_\tau(x,y)$, and the corresponding Rosser provability predicate as $\exists y (\mathrm{Prf}_\tau(x,y) \land \forall z \leq y \lnot \mathrm{Prf}_\tau(\lnot x,z))$. A provability predicate is standard if it agrees, provably in PA, with "the ordinary" provability predicate. A fixed point of a provability predicate $\mathrm{Pr}(x)$ is often called a Henkin sentence.
Now, Kurahashi (Henkin sentences and local reflection principles for Rosser provability, APAL 167(2):73-94, 2016) shows that there are standard proof predicates such that their corresponding Rosser provability predicates have provable and refutable Henkin sentences only (Theorem 4.2), and that there are other standard proof predicates such that their Rosser provability predicates have independent Henkin sentences (Corollary 4.1).
See also Question 7.2 of Halbach & Visser (Self-reference in arithmetic II, RSL 7(4):692-712, 2014) and the ensuing discussion, which seems to imply that the fixed point of a Rosser provability predicate, as obtained by the canonical Gödel diagonalisation, can not be independent.
A: As Akiva Weinberger conjectured, this depends on the implementation.
Indeed, $0=0$ is a sentence of this type, i.e. $0=0$ is equivalent to the claim that there is a proof of $0=0$ that is shorter than all proofs of its negation, since we can prove this and check, by enumeration, that the proof is shorter than all proofs of its negation, and two tautologies are equivalent.
Similarly, $0=1$ is equivalent to the claim that there is a proof of $0=1$ that is shorter than all proofs of its negation, since we can disprove this and check, by enumeration, that there is no shorter proof, and two contradictions are equivalent.
I concur with Akiva's conjecture that there also exist undecidable sentences of this type.
Even for Rosser sentences, while they are all undecidable, I don't know if there is reason to believe they are all equivalent to each other (as Gödel and Löb sentences are). I don't think Rosser-type operations have unique fixed points.
