* [AL18] Albert Atserias and Massimo Lauria.  Circular (yet sound) proofs.  CoRR, abs/1802.05266, 2018.
  * [BBC08] James Brotherston, Richard Bornat, and Cristiano Calcagno.  Cyclic proofs of program termination in separation logic.  In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 101–112, 2008.
  * [BDP11] James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen.  Automated cyclic entailment proofs in separation logic.  In CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, pages 131–146, 2011.
  * [BDS16] David Baelde, Amina Doumane, and Alexis Saurin.  Infinitary proof theory: the multiplicative additive case.  In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, pages 42:1–42:17, 2016.
  * [BGP12] James Brotherston, Nikos Gorogiannis, and Rasmus L. Petersen.  A generic cyclic theorem prover.  In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, pages 350–367, 2012.
  * [Bro05] James Brotherston.  Cyclic proofs for first-order logic with inductive definitions.  In Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, pages 78–92, 2005.
  * [Bro06] James Brotherston.  Sequent calculus proof systems for inductive definitions.  PhD thesis, University of Edinburgh, 2006.
  * [BS07] James Brotherston and Alex Simpson.  Complete sequent calculi for induction and infinite descent.  In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 51–62, 2007.
  * [BS11] James Brotherston and Alex Simpson.  Sequent calculi for induction and infinite descent.  J. Log. Comput., 21(6):1177–1216, 2011.
  * [BT17a] Stefano Berardi and Makoto Tatsuta.  Classical system of Martin-Löf’s inductive definitions is not equivalent to cyclic proof system.  In Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, pages 301–317, 2017.
  * [BT17b] Stefano Berardi and Makoto Tatsuta.  Equivalence of inductive definitions and cyclic proofs under arithmetic.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12, 2017\.
  * [Bus95] Samuel R. Buss.  The witness function method and provably recursive functions of Peano arithmetic.  In Studies in Logic and the Foundations of Mathematics, volume 134, pages 29–68. Elsevier, 1995.
  * [Bus98] Samuel R. Buss, editor.  Handbook of Proof Theory.  Studies in Logic and the Foundations of Mathematics 137. Elsevier, 1998\.
  * [CK02] Peter Clote and Evangelos Kranakis.  Boolean Functions and Computation Models.  Texts in Theoretical Computer Science. An EATCS Series. Springer, 2002\.
  * [CN10] Stephen Cook and Phuong Nguyen.  Logical Foundations of Proof Complexity.  Cambridge University Press, New York, NY, USA, 1st edition, 2010.
  * [DBHS16] Amina Doumane, David Baelde, Lucca Hirschi, and Alexis Saurin.  Towards completeness via proof search in the linear time $\mu$-calculus: The case of Büchi inclusions.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 377–386, 2016.
  * [DHL06] Christian Dax, Martin Hofmann, and Martin Lange.  A proof system for the linear time $\mathrm{\mu}$-calculus.  In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, pages 273–284, 2006.
  * [Dou17] Amina Doumane.  Constructive completeness for the linear-time $\mu$-calculus.  In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12, 2017\.
  * [DP17] Anupam Das and Damien Pous.  A cut-free cyclic proof system for Kleene algebra.  In Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, pages 261–277, 2017.
  * [For14] Jérôme Fortier.  Puissance expressive des preuves circulaires. (Expressive Power of Circular Proofs).  PhD thesis, Aix-Marseille University, Aix-en-Provence, France, 2014.
  * [FS13] Jérôme Fortier and Luigi Santocanale.  Cuts for circular proofs: semantics and cut-elimination.  In Computer Science Logic 2013 (CSL 2013), September 2-5, 2013, Torino, Italy, pages 248–262, 2013.
  * [Hir14] Denis R. Hirschfeldt.  Slicing the truth: On the computable and reverse mathematics of combinatorial principles.  World Scientific, 2014.
  * [HP93] Petr Hájek and Pavel Pudlák.  Metamathematics of First-Order Arithmetic.  Perspectives in mathematical logic. Springer, 1993.
  * [Kay91] Richard Kaye.  Models of Peano Arithmetic.  Oxford Logic Guides 15. Oxford University Press, 1991.
  * [KMPS19] Leszek Kołodziejczyk, Henryk Michalewski, Pierre Pradic, and Michał Skrzypczak.  The logical strength of Büchi’s decidability theorem.  volume Volume 15, Issue 2, May 2019.
  * [KPW95] Jan Krajíček, Pavel Pudlák, and Alan Woods.  An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle.  Random Structures & Algorithms, 7(1):15–39, 1995.
  * [Kra95] Jan Krajíček.  Bounded arithmetic, propositional logic, and complexity theory.  Cambridge University Press, New York, NY, USA, 1995.
  * [McN66] Robert McNaughton.  Testing and generating infinite sequences by a finite automaton.  Information and Control, 9(5):521–530, 1966.
  * [ML71] Per Martin-Löf.  Hauptsatz for the intuitionistic theory of iterated inductive definitions.  In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179 – 216. Elsevier, 1971.
  * [NST18] Rémi Nollet, Alexis Saurin, and Christine Tasson.  Local validity for circular proofs in linear logic with fixed points.  In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 35:1–35:23, 2018.
  * [NW96] Damian Niwinski and Igor Walukiewicz.  Games for the $\mu$-calculus.  Theor. Comput. Sci., 163(1&2):99–116, 1996.
  * [Par71] Rohit Parikh.  Existence and feasibility in arithmetic.  J. Symb. Log., 36(3):494–508, 1971.
  * [Par72] Charles Parsons.  On n-quantifier induction.  The Journal of Symbolic Logic, 37(3):466–482, 1972.
  * [PBI93] Toniann Pitassi, Paul Beame, and Russell Impagliazzo.  Exponential lower bounds for the pigeonhole principle.  Computational Complexity, 3:97–140, 1993.  10.1007/BF01200117.
  * [PW81] Jeff B. Paris and Alex J. Wilkie.  $\Delta_{0}$ sets and induction.  Open Days in Model Theory and Set Theory, W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, eds, pages 237–248, 1981.
  * [RB17] Reuben N. S. Rowe and James Brotherston.  Automatic cyclic termination proofs for recursive procedures in separation logic.  In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 53–65, 2017.
  * [San02] Luigi Santocanale.  A calculus of circular proofs and its categorical semantics.  In Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002, Grenoble, France, April 8-12, 2002, Proceedings, pages 357–371, 2002.
  * [Sch77] Kurt Schütte.  Proof Theory.  Grundlehren der mathematischen Wissenschaften 225. Springer Berlin Heidelberg, 1977.  Translation of Beweistheorie, 1968.
  * [SD03] Christoph Sprenger and Mads Dam.  On the structure of inductive reasoning: Circular and tree-shaped proofs in the $\mathrm{\mu}$-calculus.  In Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pages 425–440, 2003.
  * [Sim09] Stephen G. Simpson.  Subsystems of second order arithmetic, volume 1.  Cambridge University Press, 2009.
  * [Sim17] Alex Simpson.  Cyclic arithmetic is equivalent to Peano arithmetic.  In Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Proceedings, pages 283–300, 2017\.
  * [Str17] Sorin Stratulat.  Cyclic proofs with ordering constraints.  In Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, pages 311–327, 2017.
  * [Tho97] Wolfgang Thomas.  Languages, automata, and logic.  In Handbook of formal languages, pages 389–455. Springer, 1997\.

##  Appendix A Case study: the relativised pigeonhole principle

In this section we will give an example of the translation from Sect. 4 in a
relativised setting. Simpson already gave an example of a separation between
$\mathrm{C}{\Sigma}_{1}$ and $\mathrm{I}{\Sigma}_{1}$ via the totality of the
Ackermann-Péter function [Sim17], a ${\Pi}_{2}$ sentence. Logically simpler
${\Pi}_{1}$ separations are obtainable in the form of consistency principles,
as we discussed in Sect. 8.

In this section we consider the well-known _pigeonhole principle_ , defined by
the following FO formula with an uninterpreted function symbol $f$:

$\mathsf{PHP}(f)\ :=\ \forall n.(\forall x\leq n.f(x)<n\ \supset\ \exists
x\leq n.\exists x^{\prime}<x.f(x)=f(x^{\prime}))$

It is well-known that $\mathrm{I}{\Delta}_{0}(f)$ does not prove
$\mathsf{PHP}(f)$, due to lower bounds on propositional proofs of bounded
depth [KPW95, PBI93]. On the other hand, by relativising the constructions in
Sect. 4, it is provable in $\mathrm{C}{\Delta}_{0}(f)$ thanks to the known
simple proofs in $\mathrm{I}{\Sigma}_{1}(f)$.

###  A.1. A simple proof of $\mathsf{PHP}(f)$ in $\mathrm{I}{\Sigma}_{1}(f)$

First we recall a simple well-known proof of $\mathsf{PHP}(f)$ in
$\mathrm{I}{\Sigma}_{1}(X)$. In fact, as in Sect. 4, we will work with
${\Pi}_{1}\text{-}\mathsf{IND}$ rather than
${\Sigma}_{1}\text{-}\mathsf{IND}$.

Temporarily, let us write $A,B$ for first-order variables that we interpret as
the codes of finite sets. For such codes we may use set-theoretic symbols such
as $\in$ and $\setminus$ with their usual interpretations, with the
understanding that their basic properties are provable in
$\mathrm{I}{\Delta}_{0}$.

######  Lemma 36.

$\mathrm{I}{\Sigma}_{1}(f)$ proves the following:

$\forall A,B.(|A|>|B|\supset(\forall x\in A.f(x)\in B\supset\exists
x,x^{\prime}\in A.(x\neq x^{\prime}\wedge f(x)=f(x^{\prime}))))$ (18)

######  Proof A.1.

Working in $\mathrm{I}{\Sigma}_{1}(f)$, we reason by induction on $|B|$. If
$B$ is empty and $|A|>|B|$ then $A$ is nonempty and so (18) is vacuously true
by falsity of the premiss.

Otherwise $B$ is nonempty, so let $b\in B$ and let $|A|>|B|$.

  * •

If $\exists x\in A.f(x)=b$ then, let $a\in A$ such that $f(a)=b$.

    * –

If $\exists x\in A.(x^{\prime}\neq a\wedge f(x^{\prime})=b)$ then we are done.

    * –

Otherwise suppose $\forall x\in A.(f(x)=b\supset x=a)$. Then we have $\forall
x\in A\setminus\\{a\\}.f(x)\in B\setminus\\{b\\}$. Since we still have that
$|A\setminus\\{a\\}|>|B\setminus\\{b\\}$ we may conclude by the inductive
hypothesis.

  * •

Otherwise $\forall x\in A.f(x)\neq b$, so in fact $\forall x\in A.f(x)\in
B\setminus\\{b\\}$ and still $|A|>|B\setminus\\{b\\}$. Hence we conclude by
the inductive hypothesis.

From here there is a simple proof of $\eqref{eqn:php-
ih}\supset\mathsf{PHP}(f)$ in $\mathrm{I}{\Delta}_{0}(f)$, by instantiating
$A$ and $B$ as $[0,n]$ and $[0,n)$ resp. Thus we have that
$\mathrm{I}{\Sigma}_{1}(f)\vdash\mathsf{PHP}(f)$.

###  A.2. A proof of $\mathsf{PHP}(f)$ in $\mathrm{C}{\Delta}_{0}(f)$

To show that $\mathrm{C}{\Delta}_{0}(f)\vdash\mathsf{PHP}(f)$ it suffices to
give $\mathrm{C}{\Delta}_{0}(f)$ proofs of Lemma 36. The remainder of the
argument may be carried out in $\mathrm{I}{\Delta}_{0}(f)$, and so also in
$\mathrm{C}{\Delta}_{0}(f)$ by Prop. 7,

######  Lemma 37.

$\mathrm{C}{\Delta}_{0}(f)\vdash\eqref{eqn:php-ih}$.

######  Proof A.2.

As abbreviations, let us write $f(A)\subseteq B$ for $\forall x\in A.f(x)\in
B$ and $\mathrm{Inj}_{f}(A)$ for $\forall x,x^{\prime}\in
A.(f(x)=f(x^{\prime})\supset x=x^{\prime})$. We give an appropriate derivation
in Fig. 2, mimicking the argument of Lemma 36 under Lemma 9, where $\pi_{0}$
is a $\mathrm{I}{\Delta}_{0}(f)$ proof of $B=\varnothing,|A|>|B|,f(A)\subseteq
B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ and $\pi_{1}$ is a proof of
$a^{\prime}\in A,a^{\prime}\neq a,f(a^{\prime})=b,a\in A,f(a)=b,b\in
B,|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$.

$\pi_{0}$ $\vdots$ $\;\bullet$ $|A|>|B|,f(A)\subseteq
B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ $\scriptstyle\mathit{sub}\;$
$|A\setminus\\{a\\}|>|B\setminus\\{b\\}|,f(A\setminus\\{a\\})\subseteq
B\setminus\\{b\\}\Rightarrow\neg\mathrm{Inj}_{f}(A\setminus\\{a\\})$ $\forall
x\in A.(f(x)=b\supset x=a),a\in A,f(a)=b,|A|>|B|,f(A)\subseteq
B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ $\pi_{1}$ $a\in A,f(a)=b,b\in
B,|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ $\vdots$
$\;\bullet$ $|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$
$\scriptstyle\mathit{sub}\;$ $|A|>|B\setminus\\{b\\}|,f(A)\subseteq
B\setminus\\{b\\}\Rightarrow\neg\mathrm{Inj}_{f}(A)$ $\forall x\in A.\neg
f(x)=b,b\in B,|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ $b\in
B,|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ $\;\bullet$
$|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$
$\scriptstyle\supset,\forall\;$ $\Rightarrow\forall
A,B.(|A|>|B|\supset(f(A)\subseteq B\supset\neg\mathrm{Inj}_{f}(A)))$ Figure 2.
A $\mathrm{C}{\Delta}_{0}(f)$ proof of $\mathsf{PHP}(f)$, where $\pi_{0}$ is a
$\mathrm{I}{\Delta}_{0}(f)$ proof of $B=\varnothing,|A|>|B|,f(A)\subseteq
B\Rightarrow\neg\mathrm{Inj}_{f}(A)$ and $\pi_{1}$ is a proof of
$a^{\prime}\in A,a^{\prime}\neq a,f(a^{\prime})=b,a\in
A,f(a)=b,|A|>|B|,f(A)\subseteq B\Rightarrow\neg\mathrm{Inj}_{f}(A)$.

##  Appendix B Non-uniform complementation of Büchi automata

In this section we give a self-contained proof of Prop. 21, which is only
implicit in [KMPS19]. One novel contribution here is a much simpler proof of
the (Nonuniform) Additive Ramsey Theorem. The remainder of the complementation
argument is standard and follows closely [KMPS19], though we present it here
with more structure and proof details.

###  B.1. Nonuniform Additive Ramsey Theorem in $\mathsf{RCA}_{0}$

Let us write $\binom{\mathbb{N}}{2}$ for the set of unordered pairs of natural
numbers. We in fact write its elements as ordered pairs $(i,j)$ where always
$i<j$.

Let $(S,\bullet)$ be a finite semigroup and consider a ‘colouring’
$C:\binom{\mathbb{N}}{2}\to S$. We may omit the group operation symbol
$\bullet$ when composing elements of $S$. We say that $C$ is _additive_ if,
whenever $i<j<k$, we have $C(i,j)C(j,k)=C(i,k)$. We say that
$I\subseteq\mathbb{N}$ is an _$a$ -clique_ (under $C$) if, $\forall i,j\in I$
we have $C(i,j)=a$.

######  Theorem 38 (Nonuniform Additive Ramsey Theorem).

Let $(S,\bullet)$ be a finite semigroup. Then:

$\mathsf{RCA}_{0}\vdash\forall C:\binom{\mathbb{N}}{2}\to S.(\text{``$C$ is
additive''}\supset\exists a\in S.\exists I\subseteq\mathbb{N}.\text{``$I$ is
an infinite $a$-clique''})$

Before we give the proof, we better state the following fact:

######  Fact 39 (Nonuniform Infinite Pigeonhole Principle).

Let $S$ be a finite set. Then:

$\mathsf{RCA}_{0}\vdash\forall f:\mathbb{N}\to S.\exists a\in S.\forall
m.\exists x>m.f(x)=a$

In particular:

$\mathsf{RCA}_{0}\vdash\forall f:\mathbb{N}\to S.\ \exists Y\text{infinite}.\
\forall x,y\in Y.\ f(x)=f(y)$

This result is well-known in reverse mathematics and can be proved by a
routine meta-level induction on the size of $S$. The second display follows
from the first part by ${\Delta}^{0}_{1}\text{-}\mathsf{CA}$.

We can now give a proof of the Nonuniform Additive Ramsey Theorem. This
argument differs from and is somewhat simpler than the analogous argument from
[KMPS19] (Prop. 4.1), which requires a detour via the Ordered Ramsey Theorem
and ‘Green’ theory. In particular, since we only care about nonuniform
provability here, we are not conerned about the quantifier complexity of the
inductive invariant, since this induction will take place at the meta-level.

######  Proof B.1 (Proof of Thm. 38).

We proceed by a meta-level induction on the size of $S$. If $S$ is empty the
statement is vacuously true, so we proceed to the inductive step.

If for some $a\in S$ there are only finitely many $i$ such that $C(i,j)=a$ for
some $j>i$. Then, letting $n$ be such that $C(i,j)\neq a$ for $i,j\geq n$, we
may simply apply the inductive hypothesis to the colouring
$C(\cdot+n,\cdot+n)$. Thus we may assume henceforth that:

$\forall a\in S.\exists^{\infty}i\in\mathbb{N}.\exists j>i.C(i,j)=a$ (19)

Now, suppose that for some $a\in S$ we have $aS\subsetneq S$. We will define,
assuming the above display, a certain ‘increasing’ enumeration of elements of
$\binom{\mathbb{N}}{2}$ that map to $a$. Consider the functions
$i:\mathbb{N}\to\mathbb{N}$ and $j:\mathbb{N}\to\mathbb{N}$ defined
simultaneously as follows:

$\begin{array}[]{rcl}i(0)&:=&\beta_{0}\mu k.(k=\langle
i^{\prime},j^{\prime}\rangle\wedge j^{\prime}>i^{\prime}\wedge
C(i^{\prime},j^{\prime})=a)\\\ i(n+1)&:=&\beta_{0}\mu k.(k=\langle
i^{\prime},j^{\prime}\rangle\wedge j^{\prime}>i^{\prime}>j(n)\wedge
C(i^{\prime},j^{\prime})=a)\\\ \vskip 6.0pt plus 2.0pt minus 2.0pt\cr
j(0)&:=&\mu j^{\prime}>i(0).C(i(0),j^{\prime})=a\\\ j(n+1)&:=&\mu
j^{\prime}>i(n+1).C(i(n+1),j^{\prime})=a\end{array}$

where we write $\mu x.\varphi(x)$ for the least $x$ such that $\varphi(x)$.
Notice that this definition is a form of simultaneous primitive recursion with
provably terminating blind searches, assuming Eqn. (19), so $i$ and $j$ are
provably recursive and their defining equations above are provable (in
$\mathsf{RCA}_{0}+\eqref{eqn:each-colour-occurs-inf-high}$). Thus we have that
for all $n\in\mathbb{N}$:

$\begin{array}[]{l}i(n)<j(n)<i(n+1)\\\ C(i(n),j(n))=a\end{array}$

But now, for $m<n$, notice that,

$\begin{array}[]{rcl}C(i(m),i(n))&=&C(i(m),j(m))C(j(m),i(n))\\\
&=&aC(j(m),i(n))\\\ &\in&aS\subsetneq S\end{array}$

by the additivity property and assumption. So from here we may apply the
inductive hypothesis to the colouring $C(i(\cdot),i(\cdot))$ and conclude.
Thus we may henceforth assume that:

$\forall a\in S.aS=S$ (20)

In other words, $a\bullet\cdot$ is a bijection on $S$, for any $a\in S$. Thus
we have the left cancellation property: if $ab=ac$ then $b=c$, and for any $a$
there is a unique $b\in S$ such that $ab=a$.

Now, $C(0,\cdot)$ must take some value $a\in S$ infinitely often, by the non-
uniform infinite pigeonhole principle, Fact 39. In this case we may simply set
$I=\\{i:C(0,i)=a\\}$. Notice that, for $i,j\in I$ with $i<j$, we have
$a=C(0,j)=C(0,i)C(i,j)=aC(i,j)$, and so indeed each $C(i,j)$ is identical, by
left-cancellation.

###  B.2. Characterising rejection via the Ramseyan factorisation of
$\omega$-words

For the remainder of this section let us fix an NBA
$\mathcal{A}=(A,Q,\delta,q_{0},F)$.

Since we deal with non-deterministic automata, it no longer makes sense to use
the notation $\sigma:q\underset{\delta}{\overset{*}{\rightarrow}}q^{\prime}$
from Sect. 9, since there may be several paths through $\delta$ from $q$ to
$q^{\prime}$ following $\sigma$. Instead, for $\sigma\in A^{*}$, we write:

$x:q\underset{\delta}{\overset{\sigma}{\rightarrow}}q^{\prime}\quad:=\quad\text{``$x$
is a path through $\delta$ from $q$ to $q^{\prime}$ following $\sigma$''}$

Now, for each finite word $\sigma\in A^{*}$ we may consider its _transition
matrix_ $\delta(\sigma)$, which is the graph whose nodes are those of $Q$ with
an edge from $q$ to $q^{\prime}$ if there exists some
$x:q\underset{\delta}{\overset{\sigma}{\rightarrow}}q^{\prime}$. The edge is
labelled with $\infty$ if there is such a path that hits an accepting state
(after $q$). We construe such graphs as functions of type $Q\times
Q\to\\{0,1,\infty\\}$ in the natural way. Let us call the set of all such
graphs $\delta(A^{*})$, which we note must be finite. Notice that
$\delta:A^{*}\to(Q\times Q\to\\{0,1,\infty\\})$ is provably recursive in
$\mathsf{RCA}_{0}$ by the following definition:

$\delta(\sigma)(q,q^{\prime})=\begin{cases}0&\nexists
x:q\underset{\delta}{\overset{\sigma}{\rightarrow}}q^{\prime}\\\
\infty&\exists
x:q\underset{\delta}{\overset{\sigma}{\rightarrow}}q^{\prime}.\exists
i<|x|.x(i)\in F\\\ 1&\text{otherwise}\end{cases}$

We may compose such graphs by a variation of the usual relational composition
accounting for the labelling in a natural way: for $\beta,\gamma:Q\times
Q\to\\{0,1,\infty\\}$, we define $\beta\gamma:Q\times Q\to\\{0,1,\infty\\}$
by:

$(\beta\gamma)(q,q^{\prime})=\max\limits_{p\in
Q}\left(\beta(q,p)\cdot\gamma(p,q^{\prime})\right)$

Here we define $\max$ and $\cdot$ as expected, in particular setting
$0\cdot\infty=0=\infty\cdot 0$. Intuitively, this is just the same as
relational composition, only recording if it is possible to hit a final state
en route. Under these operations we have that $\delta$ is in fact a
homomorphism $A^{*}\to(Q\times Q\to\\{0,1,\infty\\})$, provably in
$\mathsf{RCA}_{0}$:

######  Proposition 40.

$\mathsf{RCA}_{0}\vdash\forall\sigma,\tau\in
A^{*}.\delta(\sigma\tau)=\delta(\sigma)\delta(\tau)$.

The proof follows by a straightforward induction on the length of $\tau$. Only
the base case when $\tau$ is some $a\in A$ is interesting, with the inductive
case following by associativity of word composition.

Now, for $\beta,\gamma:Q\times Q\to\\{0,1,\infty\\}$, let us say that the pair
$(\beta,\gamma)$ is _rejecting_ if:

  1. (1)

$\beta\gamma=\beta$; and,

  2. (2)

$\gamma\gamma=\gamma$; and,

  3. (3)

$\forall q\in Q.(\beta(q_{0},q)>0\supset\gamma(q,q)<\infty)$

Again, the property of being rejecting pair is clearly $\Delta^{0}_{1}$, since
we have fixed $Q$ in advance so there are only finitely many cases to
consider. Let us adopt the interval notation $[i,j]$ for the set
$\\{i,i+1,\dots,j\\}$ and $[i,j)$ for the set $\\{i,i+1,\dots,j-1\\}$. For an
infinite sequence $X$ we also write $X[i,j]$ and $X[i,j)$ for the finite
subsequences $(X(i),X(i+1),\dots,X(j))$ and $(X(i),X(i+1),\dots,X(j-1))$
respectively.

######  Lemma 41 (Ramseyan factorisation (in $\mathsf{RCA}_{0}$)).

For any $X\in A^{\omega}$, there are $\beta,\gamma\in\delta(A^{*})$ and an
infinite set $I\subseteq\mathbb{N}$ such that:

  1. (1)

$\delta(X[0,i))=\beta$, for $i\in I$.

  2. (2)

$\delta(X[i,j))=\gamma$, for $i,j\in I$ with $i<j$.

Moreover, for any such $\beta,\gamma,I$ satisfiying (1) and (2) above, we have
that:

  1. (3)

$(\beta,\gamma)$ is a rejecting pair if and only if
$X\notin\mathcal{L}(\mathcal{A})$.

######  Proof B.2.

Working inside $\mathsf{RCA}_{0}$, let
$C:\binom{\mathbb{N}}{2}\to\delta(A^{*})$ by $C(i,j)=\delta(X[i,j))$. By Prop.
40 we have that $C$ is an additive colouring, and thus we may apply the
Nonuniform Additive Ramsey Theorem, Thm. 38, to obtain some infinite set
$I_{0}$ with $\gamma=C(i,j)$, for all $i,j\in I_{0}$ with $i<j$, yielding (2).
Now, for an arbitrary $i_{0}\in I_{0}$ we may set $I=\\{i\in
I_{0}:i>i_{0}\\}$. Notice that, now,
$C(0,i)=C(0,i_{0})C(i_{0},i)=C(0,i_{0})\gamma$, so we may set $\beta=C(0,i)$
for some/any $i\in I$, yielding (1).

For (3), first suppose $(\beta,\gamma)$ is a rejecting pair and let $Y\in
Q^{\omega}$ be a run of $\mathcal{A}$ on $X$. We will show that $Y$ cannot be
accepting. By the Non-Uniform Infinite Pigeonhole Principle, Fact 39, there is
some $q\in Q$ and some infinite subset $I^{\prime}\subseteq I$ such that
$Y(i)=q$ for each $i\in I^{\prime}$. We claim that, for any $i,j\in
I^{\prime}$ and $k\in\mathbb{N}$ such that $i<k<j$, we have that $q_{k}\notin
F$. For this notice that:

  * •

$\beta(q_{0},q)>0$ since
$Y[0,i]:q_{0}\underset{\delta}{\overset{X[0,i)}{\longrightarrow}}q$.

  * •

$\gamma(q,q)<\infty$ since $(\beta,\gamma)$ is a rejecting pair.

So, if $q_{k}$ lies on the path
$Y[i,j]:q\underset{\delta}{\overset{X[i,j)}{\longrightarrow}}q$, we must have
that $q_{k}\notin F$, appealing to Prop. 40. Thus, for any $i\in I^{\prime}$,
we have that $\forall k>i.Y(k)\notin F$, and so $Y$ is not an accepting run.

Now, suppose that $(\beta,\gamma)$ is not a rejecting pair and, by definition,
let $q$ be such that $\beta(q_{0},q)>0$ and $\gamma(q,q)=\infty$. We may
enumerate infinite sets in $\mathsf{RCA}_{0}$ so let
$I=(i_{j})_{j\in\mathbb{N}}$. We may now simply define an accepting run $Y$ of
$\mathcal{A}$ on $X$ by recursive comprehension by insisting that,

  * •

in the interval $[0,i_{0})$, $Y$ follows the ‘least’ path through $\delta$
from $q_{0}$ to $q$; and,

  * •

in the interval $[i_{j},i_{j+1})$, $Y$ follows the ‘least’ path through
$\delta$ from $q$ to $q$ hitting a final state.

Such paths must exist since $(\beta,\gamma)$ is not a rejecting pair, and the
set of all paths of bounded length may be enumerated in $\mathsf{RCA}_{0}$. By
construction, $Y$ is accepting.

###  B.3. The complement NBA and proof of correctness

Now we are ready to define the complement automaton of $\mathcal{A}$, which
simply guesses a rejecting Ramseyan factorisation of an input $\omega$-word:

We define the NBA ${\mathcal{A}^{c}}=(A,Q^{c},\delta^{c},q_{0}^{c},F^{c})$ as
follows:

  * •

$Q^{c}=\\{q_{0}\\}\cup\delta(A^{*})\cup\delta(A^{*})^{2}\cup\delta(A^{*})^{3}$.

  * •

$\delta^{c}$ consists of the following transitions:

    * –

$(q_{0},a,(\beta,\gamma,\delta(a))$, for each rejecting pair $(\beta,\gamma)$.

    * –

$((\beta,\gamma,\zeta),a,(\beta,\gamma,\zeta\delta(a)))$

    * –

$((\beta,\gamma,\zeta),a,\gamma)$ if $\zeta\delta(a)=\beta$.

    * –

$(\gamma,a,(\gamma,\delta(a)))$.

    * –

$((\gamma,\zeta),a,(\gamma,\zeta\delta(a)))$.

    * –

$((\gamma,\zeta),a,\gamma)$ if $\zeta\delta(a)=\gamma$.

    * –

$(\gamma,a,\gamma)$ if $\delta(a)=\gamma$.

  * •

$q_{0}^{c}=q_{0}$.

  * •

$F^{c}=\delta(A^{*})$.

Now we are ready to prove the non-uniform complementation result.

######  Proof B.3 (Proof of Prop. 21).

By Lemma 41, it suffices to show that $\mathcal{A}^{c}$ accepts an
$\omega$-word just if has a Ramseyan factorisation that is rejecting. Let us
proceed working inside $\mathsf{RCA}_{0}$.

First, suppose $X\in A^{\omega}$ with $X\notin\mathcal{L}(\mathcal{A})$ and
let $\beta,\gamma,I$ be obtained from Lemma 41. Again we may enumerate
$I=(i_{j})_{j\in\mathbb{N}}$. Define the run $Y$ of $X$ on $\mathcal{A}^{c}$
as follows:

  * •

$Y(0)=q_{0}$ and $Y(1)=(\beta,\gamma,\delta(X(0)))$;

  * •

in the interval $[1,i_{0})$, $Y$ follows the (unique) transitions of the form
$((\beta,\gamma,\zeta),a,(\beta,\gamma,\zeta\delta(a)))$;

  * •

$Y(i_{j})=\gamma$, for all $j\in\mathbb{N}$;

  * •

in an interval $(i_{j},i_{j+1})$, $Y$ follows the (unique) transitions of the
form $((\gamma,\zeta),a,(\gamma,\zeta\delta(a)))$.

$Y$ is clearly recursive and so is indeed definable by
${\Delta}^{0}_{1}\text{-}\mathsf{CA}$. Moreover, $Y$ hits the final state
$\gamma$ infinitely often (at each $i_{j}\in I$), so $Y$ is an accepting run
for $X$ on $\mathcal{A}^{c}$.

Conversely, suppose $X\in\mathcal{L}(\mathcal{A}^{c})$ and let $Y$ be an
accepting run with $Y(1)=(\beta,\gamma,\delta(X(0)))$. By a routine induction,
$Y$ must hit $\gamma$ infinitely often, since that is the only state in
$\delta(A^{*})$ that can ever be hit. Thus, by
${\Delta}^{0}_{1}\text{-}\mathsf{CA}$, we have an infinite set
$I=\\{i\in\mathbb{N}:Y(i)=\gamma\\}$, which we again enumerate
$I=(i_{j})_{j\in\mathbb{N}}$. We may now show the properties (1) and (2) of
Lemma 41 with respect to the $\beta,\gamma,I$ thus defined by induction. More
precisely, we prove by induction on $i\in\mathbb{N}$ that $Y(i)$ has the
following form:

  * •

$q_{0}$, if $i=0$;

  * •

$(\beta,\gamma,\delta(X[0,i)))$, if $i<i_{0}$;

  * •

$\gamma$, if $i\in I$;

  * •

$(\gamma,\delta(X[i_{j},i)))$ if $i_{j}<i<i_{j+1}$.

Properties (1) and (2) from Lemma 41 now follow as special cases. Since
$(\beta,\gamma)$ was a rejecting pair, by definition of $\mathcal{A}^{c}$, we
have from Lemma 41.(3) that $\mathcal{A}$ rejects $X$. This concludes the
proof.


* [64] J. G. Kirkwood, Quantum statistics of almost classical assemblies, Phys. Rev. 44, 31 (1933).
  * [65] P. A. M. Dirac, On the analogy between classical and quantum mechanics, Rev. Mod. Phys. 17, 195 (1945).
  * [66] G. Francica, What is the most general class of quasiprobabilities of work? Phys. Rev. E 106, 054129 (2022).
  * [67] S. Gherardini and G. Chiara, Quasiprobabilities in quantum thermodynamics and many-body systems: A tutorial, (2024), arXiv:2403.17138 [quant-ph].
  * [68] David R. M. Arvidsson-Shukur, William F. Braasch Jr., Stephan De Bievre, Justin Dressel, Andrew N. Jordan, Christopher Langrenez, Matteo Lostaglio, Jeff S. Lundeen and Nicole Yunger Halpern, Properties and Applications of the Kirkwood-Dirac Distribution, (2024),  arXiv:2403.18899 [quant-ph]. .
  * [69] S. De Bièvre, Complete Incompatibility, Support Uncertainty, and Kirkwood-Dirac Nonclassicality, Phys. Rev. Lett. 127, 190404 (2021).
  * [70] M. Lostaglio, A. Belenchia, A. Levy, S. Hernández-Gómez, N. Fabbri and S. Gherardini, Kirkwood-Dirac quasiprobability approach to the statistics of incompatible observables, Quantum 7, 1128 (2023).
  * [71] A. Santini, A. Solfanelli, S. Gherardini and M. Collura, Work statistics, quantum signatures, and enhanced work extraction in quadratic fermionic models, Phys. Rev. B 108, 104308 (2023).
  * [72] A. Budiyono and H. K. Dipojono, Quantifying quantum coherence via Kirkwood-Dirac quasiprobability, Phys. Rev. A 107, 022408 (2023).
  * [73] Ji-Hui Pei, Jin-Fu Chen and H. T. Quan, Exploring quasiprobability approaches to quantum work in the presence of initial coherence: Advantages of the Margenau-Hill distribution, Phys. Rev. E  108, 054109 (2023).
  * [74] G. Francica and L. Dell’Anna, Quasiprobability distribution of work in the quantum Ising model, Phys. Rev. E  108, 014106 (2023).
  * [75] H. Struchtrup, Work storage in states of apparent negative thermodynamic temperature, Phys. Rev. Lett.  120, 250602 (2018).
  * [76] D. Frenkel and P. B. Warren, Gibbs, Boltzmann, and negative temperatures,Am. J. Phys. 83, 163 (2015).
  * [77] S. N. Shevchenko, S. Ashhab and F. Nori, Landau–Zener–Stückelberg interferometry, Phys. Rep. 1, 492 (2010).
  * [78] J. Thingna, F. Barra and M. Esposito, Kinetics and thermodynamics of a driven open quantum system, Phys. Rev. E 96, 052132 (2017).
  * [79] J. Thingna, M. Esposito and F. Barra, Landau-Zener Lindblad equation and work extraction from coherences, Phys. Rev. E 99, 042142 (2019).
  * [80] T. Denzler and E. Lutz, Efficiency fluctuations of a quantum heat engine, Phys. Rev. Res. 2, 032062 (2020).
  * [81] Zhaoyu Fei, Jin-Fu Chen and Yu-Han Ma, Efficiency statistics of a quantum Otto cycle, Phys. Rev. A 105, 022609 (2020).
  * [82] R. Kosloff and T. Feldmann, Discrete four-stroke quantum heat engine exploring the origin of friction, Phys. Rev. E 65, 055102(R) (2002).
  * [83] T. Feldmann and R. Kosloff, Quantum four-stroke heat engine: Thermodynamic observables in a model with intrinsic friction, Phys. Rev. E 68, 016101 (2003).
  * [84] F. Plastina, A. Alecce, T. J. G. Apollaro, G. Falcone, G. Francica, F. Galve, N. Lo Gullo and R. Zambrini, Irreversible Work and Inner Friction in Quantum Thermodynamic Processes, Phys. Rev. Lett. 113, 260601 (2014).
  * [85] A. E. Makouri, A. Slaoui and M. Daoud, Enhancing the performance of coupled quantum Otto thermal machines without entanglement and quantum correlations, J. Phys. B : At. Mol. Opt. Phys. 56, 085501 (2023).

##  Appendix A Expression of the average energies for the undephased engine in
terms of the transition probabilities: arbitrary Hamiltonians, unitaries, and
unital channels

The Hamiltonian $H_{1}$, Eq. (31), can also be written as

$H_{1}=2\nu_{1}|+\rangle_{11}\langle+|-\nu_{1}\mathbb{1}_{2}.$ (92)

Since at the beginning of the cycle, the system is assumed to start in thermal
equilibrium, we have

$\rho_{1}:=p_{g}|-\rangle_{11}\langle-|+p_{e}|+\rangle_{11}\langle+|=-\tanh(\beta\nu_{1})|+\rangle_{11}\langle+|+p_{g}\mathbb{1}_{2},$
(93)

where $p_{e}=e^{-\beta\nu_{1}}/Z(p_{g}=e^{\beta\nu_{1}}/Z)$ is the excited
(ground) state occupation. The second equality in Eq. (93) can be proven
easily after simple algebra. Note that the partition function $Z$ is given by
$Z:=\cosh(\beta\nu_{1})$. Similarly to Eq. (92), $H_{2}$ is given by

$H_{2}=2\nu_{2}|+\rangle_{22}\langle+|-\nu_{2}\mathbb{1}_{2}.$ (94)

Let’s now compute the average energies. We start with the average energy
$\langle E_{1}\rangle$. We have,

$\begin{split}\langle E_{1}\rangle&=\mathrm{Tr}\left[\rho_{1}H_{1}\right]\\\
&=\mathrm{Tr}\left[(-\tanh(\beta\nu_{1})|+\rangle_{11}\langle+|+p_{g}\mathbb{1}_{2})(2\nu_{1}|+\rangle_{11}\langle+|-\nu_{1}\mathbb{1}_{2})\right]\\\
&=-2\nu_{1}\tanh(\beta\nu_{1})\mathrm{Tr}\left[|+\rangle_{11}\langle+|\right]+\nu_{1}\tanh(\beta\nu_{1})\mathrm{Tr}\left[|+\rangle_{11}\langle+|\right]+2\nu_{1}p_{g}\mathrm{Tr}\left[|+\rangle_{11}\langle+|\right]-\nu_{1}p_{g}\mathrm{Tr}\left[\mathbb{1}_{2}\right]\\\
&=-2\nu_{1}\tanh(\beta\nu_{1})+\nu_{1}\tanh(\beta\nu_{1})+2\nu_{1}p_{g}-2\nu_{1}p_{g}\\\
&=-\nu_{1}\tanh(\beta\nu_{1}).\end{split}$ (95)

In the second line, we replace $H_{1}$ and $\rho_{1}$ by their expressions,
i.e., Eq. (92) and Eq. (93). In the fourth line, we use the fact that
$\mathrm{Tr}\left[|+\rangle_{11}\langle+|\right]=1$ and
$\mathrm{Tr}\left[\mathbb{1}_{2}\right]=2$.

For the average energy $\langle E_{2}\rangle$ we have,

$\begin{split}\langle E_{2}\rangle&=\mathrm{Tr}\left[\rho_{2}H_{2}\right]\\\
&=\mathrm{Tr}\left[(-\tanh(\beta\nu_{1})U|+\rangle_{11}\langle+|U^{\dagger}+p_{g}\mathbb{1}_{2})(2\nu_{2}|+\rangle_{22}\langle+|-\nu_{2}\mathbb{1}_{2})\right]\\\
&=-2\nu_{2}\tanh(\beta\nu_{1})\mathrm{Tr}\left[U|+\rangle_{11}\langle+|U^{\dagger}|+\rangle_{22}\langle+|\right]+\nu_{2}\tanh(\beta\nu_{1})\mathrm{Tr}\left[U|+\rangle_{11}\langle+|U^{\dagger}\right]+2\nu_{2}p_{g}\mathrm{Tr}\left[|+\rangle_{22}\langle+|\right]-\nu_{2}p_{g}\mathrm{Tr}\left[\mathbb{1}_{2}\right]\\\
&=-2\nu_{2}\tanh(\beta\nu_{1})(1-\delta^{\prime})+\nu_{2}\tanh(\beta\nu_{1})+2\nu_{2}p_{g}-2\nu_{2}p_{g}\\\
&=-\nu_{2}(1-2\delta^{\prime})\tanh(\beta\nu_{1}).\end{split}$ (96)

In the fourth line, we use Eq. (33) and the fact that
$\delta^{\prime}=|_{2}\langle+|U|-\rangle_{1}|^{2}=|_{2}\langle-|U|+\rangle_{1}|^{2}$
and $\delta^{\prime}+|_{2}\langle+|U|+\rangle_{1}|^{2}=1$. The latter equality
is nothing but probability conservation.

The third average enegy is given by,

$\begin{split}\langle E_{3}\rangle&=\mathrm{Tr}\left[\rho_{3}H_{2}\right]\\\
&=\mathrm{Tr}\left[(-\tanh(\beta\nu_{1})\Phi(U|+\rangle_{11}\langle+|U^{\dagger})+p_{g}\mathbb{1}_{2})(2\nu_{2}|+\rangle_{22}\langle+|-\nu_{2}\mathbb{1}_{2})\right]\\\
&=-2\nu_{2}\tanh(\beta\nu_{1})\mathrm{Tr}\left[\Phi(U|+\rangle_{11}\langle+|U^{\dagger})|+\rangle_{22}\langle+|\right]+\nu_{2}\tanh(\beta\nu_{1})\mathrm{Tr}\left[\Phi(U|+\rangle_{11}\langle+|U^{\dagger})\right]+2\nu_{2}p_{g}\mathrm{Tr}\left[|+\rangle_{22}\langle+|\right]-\nu_{2}p_{g}\mathrm{Tr}\left[\mathbb{1}_{2}\right]\\\
&=-2\nu_{2}\tanh(\beta\nu_{1})(1-\theta_{c})+\nu_{2}\tanh(\beta\nu_{1})+2\nu_{2}p_{g}-2\nu_{2}p_{g}\\\
&=-\nu_{2}(1-2\theta_{c})\tanh(\beta\nu_{1}).\end{split}$ (97)

In the fourth line, we use Eq. (59) and the fact that
$\theta_{c}+{}_{2}\langle+|\Phi(U|+\rangle_{11}\langle+|U^{\dagger})|+\rangle_{2}={}_{2}\langle-|\Phi(U|+\rangle_{11}\langle+|U^{\dagger})|-\rangle_{2}+{}_{2}\langle+|\Phi(U|+\rangle_{11}\langle+|U^{\dagger})|+\rangle_{2}=1$.
Finally, we have

$\begin{split}\langle E_{4}\rangle&=\mathrm{Tr}\left[\rho_{4}H_{1}\right]\\\
&=\mathrm{Tr}\left[(-\tanh(\beta\nu_{1})V(\Phi(U|+\rangle_{11}\langle+|U^{\dagger}))V^{\dagger}+p_{g}\mathbb{1})(2\nu_{1}|+\rangle_{11}\langle+|-\nu_{1}\mathbb{1})\right]\\\
&=-2\nu_{1}\tanh(\beta\nu_{1})\mathrm{Tr}\left[V(\Phi(U|+\rangle_{11}\langle+|U^{\dagger}))V^{\dagger}|+\rangle_{22}\langle+|\right]+\nu_{1}\tanh(\beta\nu_{1})\mathrm{Tr}\left[V(\Phi(U|+\rangle_{11}\langle+|U^{\dagger}))V^{\dagger}\right]+2\nu_{1}p_{g}\mathrm{Tr}\left[|+\rangle_{22}\langle+|\right]\\\
&-\nu_{1}p_{g}\mathrm{Tr}\left[\mathbb{1}\right]\\\
&=-2\nu_{1}\tanh(\beta\nu_{1})(1-\zeta^{c})+\nu_{1}\tanh(\beta\nu_{1})+2\nu_{1}p_{g}-2\nu_{1}p_{g}\\\
&=-\nu_{1}(1-2\zeta^{c})\tanh(\beta\nu_{1}).\end{split}$ (98)

In the fourth line, we use Eq. (60) and the fact that
$\zeta^{c}+{}_{1}\langle+|V(\Phi(U|+\rangle_{11}\langle+|U^{\dagger}))V^{\dagger}|+\rangle_{1}={}_{1}\langle-|V(\Phi(U|+\rangle_{11}\langle+|U^{\dagger}))V^{\dagger}|-\rangle_{1}+{}_{1}\langle+|V(\Phi(U|+\rangle_{11}\langle+|U^{\dagger}))V^{\dagger}|+\rangle_{1}=1$.
From Eqs. (95)-(96)-(97)-(98), follow the averages of work and heat, which are
given by,

$\langle Q_{C}\rangle=\langle E_{1}\rangle-\langle
E_{4}\rangle=-2\zeta^{c}\nu_{1}\tanh(\beta\nu_{1}),$ (99) $\langle
Q_{M}\rangle=\langle E_{3}\rangle-\langle
E_{2}\rangle=2(\theta_{c}-\delta^{\prime})\nu_{2}\tanh(\beta\nu_{1}),$ (100)

and,

$\langle W\rangle=\langle Q_{M}\rangle+\langle
Q_{C}\rangle=2((\theta_{c}-\delta^{\prime})\nu_{2}-\zeta^{c}\nu_{1})\tanh(\beta\nu_{1}).$
(101)

Please note that $\langle Q_{C}\rangle\leq 0$ as expected, since
$\zeta^{c}\geq 0$.

##  Appendix B Expression of the second cumulants for the undepahed engine in
terms of the transition probabilities: arbitrary Hamiltonians, unitaries, and
unital channels

Let’s now start with the variance of $Q_{C}$. From definition 1 and Eq. (16),
it follows that

$\begin{split}\langle
Q_{C}^{2}\rangle_{c}:&=\frac{\partial^{2}\mathrm{log}(\chi_{UDE}(\gamma_{1}=\gamma_{C},\gamma_{2}=0,\gamma_{3}=0,\gamma_{4}=-\gamma_{C}))}{\partial(i\gamma_{C})^{2}}\bigg{\rvert}_{\gamma_{C}=0}.\end{split}$
(102)

Let’s now make
$a:=\chi_{UDE}(\gamma_{1}=\gamma_{C},\gamma_{2}=0,\gamma_{3}=0,\gamma_{4}=-\gamma_{C})$.
One can arrive at:

$\begin{split}\langle
Q_{C}^{2}\rangle_{c}&=\left(\frac{1}{a}\frac{\partial^{2}a}{\partial(i\gamma_{C})^{2}}\right)\bigg{\rvert}_{\gamma_{C}=0}-\left(\frac{1}{a}\frac{\partial
a}{\partial(i\gamma_{C})}\right)^{2}\bigg{\rvert}_{\gamma_{C}=0}\\\
&=\left(\frac{1}{a}\frac{\partial^{2}a}{\partial(i\gamma_{C})^{2}}\right)\bigg{\rvert}_{\gamma_{C}=0}-\langle
Q_{C}\rangle^{2}.\end{split}$ (103)

Using the fact that when $\gamma_{C}=0$ we obtain $a=1$ then the variance of
$Q_{C}$ is given by,

$\begin{split}\langle
Q_{C}^{2}\rangle_{c}&=\mathrm{Tr}\left[H_{1}^{2}V(\Phi(U\rho_{1}U^{\dagger}))V^{\dagger}\right]+\mathrm{Tr}\left[H_{1}^{2}\rho_{1}\right]-2\mathrm{Tr}\left[H_{1}V(\Phi(UH_{1}\rho_{1}U^{\dagger}))V^{\dagger}\right]-\langle
Q_{C}\rangle^{2}\\\
&=2\nu_{1}^{2}-2\mathrm{Tr}\left[H_{1}V(\Phi(UH_{1}\rho_{1}U^{\dagger}))V^{\dagger}\right]-\langle
Q_{C}\rangle^{2}.\end{split}$ (104)

Note that in the second line, we use the fact that
$H_{1}^{2}=\nu_{1}^{2}\mathbb{1_{2}}$. Now let’s compute
$\mathrm{Tr}\left[H_{1}V(\Phi(UH_{1}\rho_{1}U^{\dagger}))V^{\dagger}\right]$.
We have,

$\begin{split}\mathrm{Tr}\left[H_{1}V(\Phi(UH_{1}\rho_{1}U^{\dagger}))V^{\dagger}\right]&=\mathrm{Tr}\left[(\nu_{1}|+\rangle_{11}\langle+|-\nu_{1}|-\rangle_{11}\langle-|)V(\Phi(U(\nu_{1}p_{e}|+\rangle_{11}\langle+|-\nu_{1}p_{g}|-\rangle_{11}\langle-|)U^{\dagger}))V^{\dagger}\right]\\\
&=\nu_{1}^{2}p_{e}(1-\zeta^{c})-\nu_{1}^{2}p_{g}\zeta^{c}-\nu_{1}^{2}p_{e}\zeta^{c}+\nu_{1}^{2}p_{g}(1-\zeta^{c})\\\
&=\nu_{1}^{2}(1-2\zeta^{c}).\end{split}$ (105)

In the first line, we replace $H_{1}$ and $\rho_{1}$ by their expressions, and
in the second line, we use Eq. (60). Putting all things together, i.e., Eqs.
(104)-(105), one arrives at,

$\langle Q_{C}^{2}\rangle_{c}=4\zeta^{c}\nu_{1}^{2}-\langle Q_{C}\rangle^{2}.$
(106)

Using Eq. (99), we have, $\langle
Q_{C}^{2}\rangle_{c}=4\zeta^{c}\nu_{1}^{2}(1-\zeta^{c}\tanh^{2}(\beta\nu_{1}))$.
Furthermore, from the fact that $0\leq\zeta^{c}\leq 1$, one can see that
$\langle Q_{C}^{2}\rangle_{c}\geq 0$, in agreement with the fact that this is
a variance.

Now let’s compute the fluctuations of $Q_{M}$. The latter are given as
follows:

$\langle
Q_{M}^{2}\rangle_{c}:=\mathrm{Re}\bigg{\\{}\frac{\partial^{2}\mathrm{log}(\chi_{UDE}(\gamma_{1}=0,\gamma_{2}=-\gamma_{M},\gamma_{3}=\gamma_{M},\gamma_{4}=0))}{\partial(i\gamma_{M})^{2}}\bigg{\rvert}_{\gamma_{M}=0}\bigg{\\}}.$
(107)

$\mathrm{Re}$ here refers to the real part of the second cumulant of $Q_{M}$.
That is, in contrast to the second cumulant of $Q_{C}$, the second cumulant of
$Q_{M}$ has a real and imaginary part. After simple algebra (as we did for the
variance of $Q_{C}$), one can arrive at,

$\begin{split}\langle
Q_{M}^{2}\rangle_{c}&=\mathrm{Tr}\left[H_{2}^{2}\Phi(\rho_{2})\right]+\mathrm{Tr}\left[H_{2}^{2}\rho_{2}\right]-2\mathrm{Re}\\{\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]\\}-\langle
Q_{M}\rangle^{2}\\\
&=2\nu_{2}^{2}-2\mathrm{Re}\\{\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]\\}-\langle
Q_{M}\rangle^{2}\\\
&=2\nu_{2}^{2}-\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2}+\rho_{2}H_{2})\right]-\langle
Q_{M}\rangle^{2}.\end{split}$ (108)

In the second line, we use the fact that
$H_{2}^{2}=\nu_{2}^{2}\mathbb{1}_{2}$. In the last line, we use the fact that
$2\mathrm{Re}\\{\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]\\}=2(\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]+\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]^{\ast})/2=\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2}+\rho_{2}H_{2})\right]$,
where
$\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]^{\ast}(:=\mathrm{Tr}\left[\left(H_{2}\Phi(H_{2}\rho_{2})\right)^{\dagger}\right])$
is the complex conjugate of
$\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]$. Now let’s simplify the
latter term using an important trick. One can prove the next result:

######  Lemma 3.

The anticommutator $\\{H_{2},\rho_{2}\\}:=H_{2}\rho_{2}+\rho_{2}H_{2}$ can be
simplified as follows:

$\\{H_{2},\rho_{2}\\}=H_{2}\rho_{2}+\rho_{2}H_{2}=2\nu_{2}({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|-\langle-|\rho_{2}|-\rangle|-\rangle_{22}\langle-|)=2H_{2}\Delta_{2}(\rho_{2}).$
(109)

###### Proof.

Using the completeness relation in the eigenbasis of $H_{2}$, i.e.,
$|+\rangle_{22}\langle+|+|-\rangle_{22}\langle-|=\mathbb{1}_{2}$, we have

$\begin{split}H_{2}\rho_{2}+\rho_{2}H_{2}&=H_{2}\mathbb{1}_{2}\rho_{2}\mathbb{1}_{2}+\mathbb{1}_{2}\rho_{2}\mathbb{1}_{2}H_{2}\\\
&=\nu_{2}(|+\rangle_{22}\langle+|-|-\rangle_{22}\langle-|)({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|+{}_{2}\langle+|\rho_{2}|-\rangle_{2}|+\rangle_{22}\langle-|+{}_{2}\langle-|\rho_{2}|+\rangle_{2}|-\rangle_{22}\langle+|+{}_{2}\langle-|\rho_{2}|-\rangle_{2}|-\rangle_{22}\langle-|)\\\
&+({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|+{}_{2}\langle+|\rho_{2}|-\rangle_{2}|+\rangle_{22}\langle-|+{}_{2}\langle-|\rho_{2}|+\rangle_{2}|-\rangle_{22}\langle+|+{}_{2}\langle-|\rho_{2}|-\rangle_{2}|-\rangle_{22}\langle-|)\nu_{2}(|+\rangle_{22}\langle+|-|-\rangle_{22}\langle-|)\\\
&=\nu_{2}({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|+{}_{2}\langle+|\rho_{2}|-\rangle_{2}|+\rangle_{22}\langle-|-{}_{2}\langle-|\rho_{2}|+\rangle_{2}|-\rangle_{22}\langle+|-{}_{2}\langle-|\rho_{2}|-\rangle_{2}|-\rangle_{22}\langle-|)\\\
&+\nu_{2}({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|-{}_{2}\langle+|\rho_{2}|-\rangle_{2}|+\rangle_{22}\langle-|+{}_{2}\langle-|\rho_{2}|+\rangle_{2}|-\rangle_{22}\langle+|-{}_{2}\langle-|\rho_{2}|-\rangle_{2}|-\rangle_{22}\langle-|)\\\
&=2\nu_{2}({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|-{}_{2}\langle-|\rho_{2}|-\rangle_{2}|-\rangle_{22}\langle-|).\
\end{split}$ (110)

In the second line, we use the decomposition Eq. (55). This shows that the
result of the antricomutator $\\{H_{2},\rho_{2}\\}$ is something that is
diagonal in the eigenbasis of $H_{2}$. It can also be written as:
$\\{H_{2},\rho_{2}\\}=2H_{2}\Delta_{2}(\rho_{2})$; see the diagonal part of
$\rho_{2}$ in Eq. (55). ∎

The latter proved result would be important to simplify the variances of
$Q_{M}$ and $W$. Using equation (110), we have,

$\begin{split}\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2}+\rho_{2}H_{2})\right]&=2\mathrm{Tr}\left[(\nu_{2}|+\rangle_{22}\langle+|-\nu_{2}|-\rangle_{22}\langle-|)\Phi(\nu_{2}({}_{2}\langle+|\rho_{2}|+\rangle_{2}|+\rangle_{22}\langle+|-{}_{2}\langle-|\rho_{2}|-\rangle_{2}|-\rangle_{22}\langle-|))\right]\\\
&=2\nu_{2}^{2}\left({}_{2}\langle+|\rho_{2}|+\rangle_{2}(1-\theta)-{}_{2}\langle-|\rho_{2}|-\rangle_{2}\theta-{}_{2}\langle+|\rho_{2}|+\rangle_{2}\theta+{}_{2}\langle-|\rho_{2}|-\rangle_{2}(1-\theta)\right)\\\
&=2\nu_{2}^{2}(1-2\theta).\end{split}$ (111)

In the second line, we use Eq. (59), and in the third line,
$\mathrm{Tr}\left[\rho_{2}\right]={}_{2}\langle+|\rho_{2}|+\rangle_{2}+{}_{2}\langle-|\rho_{2}|-\rangle_{2}=1$.
Putting everything together, we obtain the next compact equation,

$\langle Q_{M}^{2}\rangle_{c}=4\nu_{2}^{2}\theta-\langle
Q_{M}\rangle^{2}=4\nu_{2}^{2}(\theta-((\theta_{c}-\delta^{\prime})\tanh(\beta\nu_{1}))^{2}).$
(112)

The imaginary part of the second cumulant of $Q_{M}$ is given by
$-2\mathrm{Im}\\{\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]\\}$.

Similarly to the variance of $Q_{C}$ and $Q_{M}$ we have,

$\langle
W^{2}\rangle_{c}:=\mathrm{Re}\bigg{\\{}\frac{\partial^{2}\mathrm{log}(\chi_{UDE}(\gamma_{1}=\gamma_{W},\gamma_{2}=-\gamma_{W},\gamma_{3}=\gamma_{W},\gamma_{4}=-\gamma_{W}))}{\partial(i\gamma_{W})^{2}}\bigg{\rvert}_{\gamma_{W}=0}\bigg{\\}}.$
(113)

And, its explicit expression is given by

$\begin{split}\langle
W^{2}\rangle_{c}&=\mathrm{Tr}\left[H_{1}^{2}\rho_{1}\right]+\mathrm{Tr}\left[H_{2}^{2}\rho_{2}\right]+\mathrm{Tr}\left[H_{2}^{2}\rho_{3}\right]+\mathrm{Tr}\left[H_{1}^{2}\rho_{4}\right]-2\mathrm{Tr}\left[H_{2}U(H_{1}\rho_{1})U^{\dagger}\right]+2\mathrm{Tr}\left[H_{2}\Phi(U(H_{1}\rho_{1})U^{\dagger})\right]\\\
&-2\mathrm{Tr}\left[H_{1}V(\Phi(U(H_{1}\rho_{1})U^{\dagger}))V^{\dagger}\right]-2\mathrm{Re}\\{\mathrm{Tr}\left[H_{2}\Phi(H_{2}\rho_{2})\right]\\}+2\mathrm{Re}\\{\mathrm{Tr}\left[H_{1}V(\Phi(H_{2}\rho_{2}))V^{\dagger}\right]\\}-2\mathrm{Re}\\{\mathrm{Tr}\left[H_{1}V(H_{2}\rho_{3})V^{\dagger}\right]\\}\\\
&-\langle W\rangle^{2}.\end{split}$ (114)

We see from the second cumulants of $Q_{M}$ and $W$ that the imaginary part
comes from the average of the next products: $E_{2}E_{3}$, $E_{2}E_{4}$, and
$E_{3}E_{4}$. However, the average of the product of $E_{1}$ with $E_{2}$,
$E_{3}$, and $E_{4}$ is always real, hence the nullity of the imaginary part
of the second cumulant of $Q_{C}$. Furthermore, following the same reasoning
as we did for $Q_{C}$ and $Q_{M}$, i.e., by applying lemma 109, one can prove
that the work fluctuations are given by

$\langle
W^{2}\rangle_{c}=4\nu_{1}\nu_{2}(\delta^{\prime}+\zeta-\theta_{c}-\zeta_{c})+4(\nu_{1}^{2}\zeta^{c}+\nu_{2}^{2}\theta)-\langle
W\rangle^{2}.$ (115)

Finally, note that Eqs. (99)-(100)-(101) and Eqs. (106)-(112)-(115) are
important results of the paper since they compress the expressions of the
averages and the fluctuations into simple expressions.

##  Appendix C Lower bounds on the RFs of $Q_{C}$

From Eq. (99) and Eq. (106), we have,

$\langle\Sigma\rangle\left(\frac{\langle Q_{C}^{2}\rangle_{c}}{\langle
Q_{C}\rangle^{2}}+1\right)=-\beta\langle Q_{C}\rangle\left(\frac{\langle
Q_{C}^{2}\rangle_{c}}{\langle
Q_{C}\rangle^{2}}+1\right)=2\beta\nu_{1}\coth(\beta\nu_{1})\geq 2.$ (116)

The lower bound is achieved when $\beta=0$, i.e., in the high-temperature
regime. From equation (116), we see that

$\frac{\langle Q_{C}^{2}\rangle_{c}}{\langle
Q_{C}\rangle^{2}}\geq\frac{2\beta\nu_{1}\coth(\beta\nu_{1}}{\langle\Sigma\rangle}-1\geq\frac{2}{\langle\Sigma\rangle}-1.$
(117)

Furthermore, one can also show that when $\zeta^{c}\leq 1/2$, it follows that

$\langle Q_{C}^{2}\rangle_{c}\geq\langle Q_{C}\rangle^{2}.$ (118)

Consider an arbitrary unitary $U$. When $V=U^{\dagger}$ and for the unital
channel of Sec. III, one can show that

$0\leq\zeta^{c}\leq 1/2.$ (119)

###### Proof.

After simple lines of algebra, one can show that $\zeta^{c}$ is given as
follows:

$\begin{split}\zeta^{c}&=\sum_{j}{}_{1}\langle-|U^{\dagger}\pi_{j}U|+\rangle_{11}\langle+|U^{\dagger}\pi_{j}U|-\rangle_{1}\\\
&=|_{1}\langle-|U^{\dagger}|\pi_{1}\rangle|^{2}|\langle\pi_{1}|U|+\rangle_{1}|^{2}+|_{1}\langle-|U^{\dagger}|\pi_{2}\rangle|^{2}|\langle\pi_{2}|U|+\rangle_{1}|^{2}.\end{split}$
(120)

Where we replace $\pi_{j}$ by $|\pi_{j}\rangle\langle\pi_{j}|$ for $j=1$ and
$2$. And by defining $p_{1}:=|\langle\pi_{1}|U|+\rangle_{1}|^{2}$ and
$p_{2}:=|\langle\pi_{2}|U|+\rangle_{1}|^{2}$, one can find that,

$\zeta^{c}=(1-p_{1})p_{1}+(1-p_{2})p_{2}.$ (121)

This follows from the microreversibility principle, i.e.,

$\begin{split}|_{1}\langle-|U^{\dagger}|\pi_{1}\rangle|^{2}&=|\langle\pi_{1}|U|-\rangle_{1}|^{2}\\\
&=\langle\pi_{1}|U(\mathbb{1}_{2}-|+\rangle_{11}\langle+|)U^{\dagger}|\pi_{1}\rangle\\\
&=1-|\langle\pi_{1}|U|+\rangle_{1}|^{2}\\\ &=1-p_{1}.\end{split}$ (122)

In the same manner, we have
$|_{1}\langle-|U^{\dagger}|\pi_{2}\rangle|^{2}=1-p_{2}$. Further, one can also
prove that $p_{2}=1-p_{1}$ as follows:

$\begin{split}p_{2}&=|\langle\pi_{2}|U|+\rangle_{1}|^{2}\\\
&={}_{1}\langle+|U^{\dagger}|\pi_{2}\rangle\langle\pi_{2}|U|+\rangle_{1}\\\
&={}_{1}\langle+|U^{\dagger}(\mathbb{1}_{2}-|\pi_{1}\rangle\langle\pi_{1}|)U|+\rangle_{1}\\\
&=1-|\langle\pi_{1}|U|+\rangle_{1}|^{2}\\\ &=1-p_{1}.\end{split}$ (123)

Putting everything together, we obtain

$\zeta^{c}=2p_{1}(1-p_{1}).$ (124)

And from the fact that $0\leq p_{1}\leq 1$, we conclude that

$0\leq\zeta^{c}\leq 1/2.$ (125)

The highest value is achieved when $p_{1}=1/2$. ∎

##  Appendix D Proof of $\zeta_{c}=\theta_{c}$ and $\delta^{\prime}=\zeta$,
when $V=U^{\dagger}$

Before we prove that, $\langle Q_{M}^{2}\rangle_{c}-\langle
W^{2}\rangle_{c}\geq 0$ in the heat engine region. Let’s first prove that
$\zeta_{c}=\theta_{c}$ for the unital channel given in Sec. III and when
$V=U^{\dagger}$. For arbitary $U$ and $V$ that satisfy $V=U^{\dagger}$, and
for the unital channel of Sec. III, one can show that $\zeta_{c}=\theta_{c}$.

###### Proof.

We have,

$\begin{split}\zeta_{c}&={}_{1}\langle-|V\Phi(|+\rangle_{22}\langle+|)V^{\dagger}|-\rangle_{1}\\\
&=\sum_{j}{}_{1}\langle-|U^{\dagger}\pi_{j}|+\rangle_{22}\langle+|\pi_{j}U|-\rangle_{1}\\\
&=\sum_{j}{}_{2}\langle+|\pi_{j}U|-\rangle_{11}\langle-|U^{\dagger}\pi_{j}|+\rangle_{2}\\\
&={}_{2}\langle+|\Phi(U|-\rangle_{11}\langle-|U^{\dagger})|+\rangle_{2}\\\
&=\theta_{c}.\end{split}$ (126)

In the second line, we replace $\Phi$ by its expression and $V$ by
$U^{\dagger}$. ∎

Now let’s prove thtat when $V=U^{\dagger}$ we have $\delta^{\prime}=\zeta$.

###### Proof.

We have,

$\begin{split}\zeta&=|{}_{1}\langle+|V|-\rangle_{2}|\\\
&=|{}_{1}\langle+|U^{\dagger}|-\rangle_{2}|\\\
&={}_{2}\langle-|U|+\rangle_{11}\langle+|U^{\dagger}|-\rangle_{2}\\\
&={}_{2}\langle-|U(\mathbb{1}_{2}-|-\rangle_{11}\langle-|)U^{\dagger}|-\rangle_{2}\\\
&=1-{}_{2}\langle-|U|-\rangle_{11}\langle-|U^{\dagger}|-\rangle_{2}\\\
&=1-({}_{1}\langle-|U^{\dagger}(\mathbb{1}_{2}-|+\rangle_{22}\langle+|)U|-\rangle_{1})\\\
&=1-(1-{}_{1}\langle-|U^{\dagger}|+\rangle_{22}\langle+|U|-\rangle_{1})\\\
&=|_{2}\langle+|U|-\rangle_{1}|^{2}\\\ &=\delta^{\prime}.\end{split}$ (127)

∎

##  Appendix E Proof of theorem 2 (Eq. (81))

###### Proof.

Using the results of Appendix D, one can show the next series of equalities;

$\begin{split}\langle
W^{2}\rangle_{c}&=4\nu_{1}\nu_{2}(\delta^{\prime}+\zeta-\theta_{c}-\zeta_{c})+4(\nu_{1}^{2}\zeta^{c}+\nu_{2}^{2}\theta)-\langle
W\rangle^{2}\\\
&=4\nu_{1}\nu_{2}(2\delta^{\prime}-2\theta_{c})+4(\nu_{1}^{2}\zeta^{c}+\nu_{2}^{2}\theta)-\langle
W\rangle^{2}\\\
&=4\nu_{1}(-2\nu_{2}(\theta_{c}-\delta^{\prime})+\nu_{1}\zeta^{c})+4\nu_{2}^{2}\theta-\langle
W\rangle^{2}\\\ &=4\nu_{1}(-\coth(\beta\nu_{1})\langle
Q_{M}\rangle-\coth(\beta\nu_{1})\langle
Q_{C}\rangle/2)+4\nu_{2}^{2}\theta-\langle W\rangle^{2}\\\
&=-2\nu_{1}\coth(\beta\nu_{1})(\langle Q_{M}\rangle+\langle
W\rangle)+4\nu_{2}^{2}\theta-\langle W\rangle^{2}.\end{split}$ (128)

In the fourth line, we use Eqs. (62)-(61). Further, now consider the
difference $\langle Q_{M}^{2}\rangle_{c}-\langle W^{2}\rangle_{c}$. One can
show the next series of equalities,

$\begin{split}\langle Q_{M}^{2}\rangle_{c}-\langle
W^{2}\rangle_{c}&=4\nu_{2}^{2}\theta-\langle
Q_{M}\rangle^{2}-(-2\nu_{1}\coth(\beta\nu_{1})(\langle Q_{M}\rangle+\langle
W\rangle)+4\nu_{2}^{2}\theta-\langle W\rangle^{2})\\\
&=2\nu_{1}\coth(\beta\nu_{1})(\langle Q_{M}\rangle+\langle W\rangle+(\langle
W\rangle-\langle Q_{M}\rangle)(\langle Q_{M}\rangle+\langle W\rangle)\\\
&=(\langle W\rangle+\langle Q_{M}\rangle)(2\nu_{1}+\langle
Q_{C}\rangle\tanh(\beta\nu_{1}))\coth(\beta\nu_{1})\\\
&=2\nu_{1}\coth(\beta\nu_{1})(\langle W\rangle+\langle
Q_{M}\rangle)(1-\zeta^{c}\tanh^{2}(\beta\nu_{1})).\end{split}$ (129)

Now that the latter result is always $\geq 0$ in the heat engine region.
Further, the term $(1-\zeta^{c}\tanh^{2}(\beta\nu_{1}))$ is always $\geq 0$,
since $0\leq\zeta^{c}\tanh^{2}(\beta\nu_{1})\leq 1$. On the other hand, the
term $\langle W\rangle+\langle Q_{M}\rangle$ is $\geq(\leq)0$ when both
$\langle W\rangle$ and $\langle Q_{M}\rangle$ are $\geq(\leq)0$. Of course,
$\langle W\rangle+\langle Q_{M}\rangle$ can still be $\geq 0$ even when
$\langle W\rangle\leq 0$ is $\leq$ and $\langle Q_{M}\rangle$ $\geq 0$ such
that their sum is $\geq 0$. From all this, we see that in the heat engine
region, we have $\langle Q_{M}^{2}\rangle_{c}-\langle W^{2}\rangle_{c}\geq 0$,
thus

$\frac{\langle W^{2}\rangle_{c}}{\langle Q_{M}^{2}\rangle_{c}}\leq 1.$ (130)

∎

Note that they become equal at the point where efficiency goes to 1. In this
case, $W$ and $Q_{M}$ converge to 0. But note that numerically, we found that
fluctuations of both $W$ and $Q_{M}$ are non-zero.

##  Appendix F Difference between the relative fluctuations

Let’s compute the difference between the relative fluctuations of work $W$ and
heat $Q_{M}$. We have,

$\begin{split}\frac{\langle W^{2}\rangle_{c}}{\langle
W\rangle^{2}}-\frac{\langle Q_{M}^{2}\rangle_{c}}{\langle
Q_{M}\rangle^{2}}&=\frac{\langle W^{2}\rangle_{c}\langle
Q_{M}\rangle^{2}-\langle Q_{M}^{2}\rangle_{c}\langle W\rangle^{2}}{\langle
W\rangle^{2}\langle Q_{M}\rangle^{2}}\\\
&=\frac{(-2\nu_{1}\coth(\beta\nu_{1})(\langle Q_{M}\rangle+\langle
W\rangle)+4\nu_{2}^{2}\theta-\langle W\rangle^{2})\langle
Q_{M}\rangle^{2}-(4\theta\nu_{2}^{2}-\langle Q_{M}\rangle^{2})\langle
W\rangle^{2}}{\langle W\rangle^{2}\langle Q_{M}\rangle^{2}}\\\
&=\frac{-2\nu_{1}\coth(\beta\nu_{1})(\langle Q_{M}\rangle+\langle
W\rangle)\langle Q_{M}\rangle^{2}+4\theta\nu_{2}^{2}(\langle
Q_{M}\rangle^{2}-\langle W\rangle^{2})}{\langle W\rangle^{2}\langle
Q_{M}\rangle^{2}}\\\ &=\frac{-2\nu_{1}\coth(\beta\nu_{1})(\langle
Q_{M}\rangle+\langle W\rangle)\langle
Q_{M}\rangle^{2}+4\theta\nu_{2}^{2}(\langle Q_{M}\rangle-\langle
W\rangle)(\langle Q_{M}\rangle+\langle W\rangle)}{\langle W\rangle^{2}\langle
Q_{M}\rangle^{2}}\\\ &=\frac{(\langle Q_{M}\rangle+\langle
W\rangle)(-2\nu_{1}\coth(\beta\nu_{1})\langle
Q_{M}\rangle^{2}-4\theta\nu_{2}^{2}\langle Q_{C}\rangle)}{\langle
W\rangle^{2}\langle Q_{M}\rangle^{2}}\\\ &=\frac{(\langle Q_{M}\rangle+\langle
W\rangle)(8\theta\zeta^{c}\nu_{1}\nu_{2}^{2}\tanh(\beta\nu_{1})-8\nu_{1}\nu_{2}^{2}\tanh(\beta\nu_{1})(\theta_{c}-\delta^{\prime})^{2})}{\langle
W\rangle^{2}\langle Q_{M}\rangle^{2}}\\\
&=\frac{8\nu_{1}\nu_{2}^{2}\tanh(\beta\nu_{1})(\langle Q_{M}\rangle+\langle
W\rangle)(\theta\zeta^{c}-(\theta_{c}-\delta^{\prime})^{2})}{\langle
W\rangle^{2}\langle Q_{M}\rangle^{2}}.\end{split}$ (131)

In the second line, we use Eqs. (66)-(128). In the sixth line, we use Eqs.
(61)-(62). Similarly to those steps of calculus, one can show that,

$\frac{\langle W^{2}\rangle_{c}}{\langle W\rangle^{2}}-\frac{\langle
Q_{C}^{2}\rangle_{c}}{\langle
Q_{C}\rangle^{2}}=\frac{(4\nu_{1}\nu_{2}\tanh(\beta\nu_{1}))^{2}(\theta\zeta^{c}-(\theta_{c}-\delta^{\prime})^{2})}{\langle
W\rangle^{2}\langle Q_{C}\rangle^{2}}.$ (132)