# Improved sensitivities of ESS$\nu$SB from a two-detector fit

F. Capozzi<EMAIL_ADDRESS>Dipartimento di Scienze Fisiche e
Chimiche, Università degli Studi dell’Aquila, 67100 L’Aquila, Italy  C. Giunti
<EMAIL_ADDRESS>Istituto Nazionale di Fisica Nucleare (INFN), Sezione
di Torino, Via P. Giuria 1, I–10125 Torino, Italy  C.A. Ternes
<EMAIL_ADDRESS>Istituto Nazionale di Fisica Nucleare (INFN), Sezione di
Torino, Via P. Giuria 1, I–10125 Torino, Italy  Dipartimento di Fisica,
Università di Torino, via P. Giuria 1, I–10125 Torino, Italy

( August 28, 2024, )

###### Abstract

We discuss the improvement of the sensitivity of ESS$\nu$SB to the discovery
of CP violation and to new neutrino physics which can be obtained with a two-
detector fit of the data of the near and far detectors. In particular, we
consider neutrino non-standard interactions generated by very heavy vector
mediators, nonunitary neutrino mixing, and neutrino oscillations due to the
mixing of the ordinary active neutrinos with a light sterile neutrino.

###### Contents

  1. I Introduction
  2. II Simulation details
  3. III CP-sensitivity
  4. IV Non-standard interactions
  5. V Nonunitary neutrino mixing
  6. VI Light sterile neutrinos
  7. VII Summary and conclusions

##  I Introduction

The European Spallation Source neutrino Super-Beam (ESS$\nu$SB) [1, 2, 3, 4]
is a proposed long-baseline neutrino oscillation experiment with a high
intensity neutrino beam produced at the upgraded ESS facility in Lund
(Sweden). The main goal of ESS$\nu$SB is the search for CP violation in the
lepton sector with a megaton underground Water Cherenkov far detector
installed at a distance of either 360 km or 540 km from the ESS. A near
detector located at a distance of 250 m from the neutrino source will be used
to monitor the neutrino beam intensity and reduce the systematic
uncertainties. Besides CP violation [5, 6], the ESS$\nu$SB experiment can
probe new neutrino physics beyond the standard three-neutrino mixing framework
and new neutrino interactions beyond the Standard Model [7, 8, 9, 10, 11, 12,
13].

In this paper we discuss the potentialities of a two-detector analysis of the
data of ESS$\nu$SB with the updated configuration described in Refs. [3, 4].
We show the advantages of a two-detector analysis with respect to an analysis
of the data of the far detector alone, as done in some of the previous studies
[5, 6, 9, 12]. We discuss the sensitivity of ESS$\nu$SB to the discovery of CP
violation (Section III), to neutrino non-standard interactions (NSI) generated
by very heavy vector mediators (Section IV), to nonunitarity of the neutrino
mixing matrix (Section V), and to neutrino oscillations due to the mixing of
the ordinary active neutrinos with a light sterile neutrino (Section VI).

##  II Simulation details

In this section we describe the simulation details of ESS$\nu$SB. Our
simulation of the far detector follows Refs. [3, 4] using the GLoBES [14, 15]
files for ESS$\nu$SB, which take into account the ESS$\nu$SB specific fluxes,
selection efficiencies, energy smearing and cross sections. The far detector
is a water Cherenkov detector with 538 kt fiducial volume at 360 km distance
from the source. There is another possible location at 540 km distance from
the source. However, it has been shown that the CP sensitivity is slightly
worse [3, 4], and we will not consider this possibility here. We assume a
running time of 5 years in neutrino mode and 5 years in antineutrino mode. In
addition to the far detector we simulate a near detector assuming the same
energy smearing as for the far detector. The near detector is also a water
Cherenkov detector, but placed at 250 m from the source and with a fiducial
volume of 1 kt.

In our analysis we include appearance and disappearance channels. Each channel
includes background contributions from wrong sign contamination of the beam,
flavor misinterpretations and misinterpretations of event topologies. In
addition to the considerations of Refs. [3, 4], which included only charged
current (CC) events, we also simulate a neutral current (NC) event sample at
the near and far detectors adding background contributions due to
misidentification of charged current as neutral current events. For this
channel we assume a conservative 20% energy resolution and 90% detection
efficiency, as was assumed for DUNE [16]. Also this is a conservative choice,
since better efficiencies have already been reached in Super-Kamiokande, which
also uses water as detection material [17]. In former analyses the authors
mostly considered a single detector simulation, assuming individual
normalization and shape uncertainties in each channel. Since we perform a
2-detector analysis, we can correlate many of the systematic uncertainties
among detectors and channels, improving the overall sensitivity of the
experiment. The systematic uncertainties that we consider are essentially
those of Ref. [18] for a superbeam experiment and are listed in Table 1. They
include an overall uncertainty on the fiducial volume of the near and far
detectors. This uncertainty is correlated between the neutrino and
antineutrino modes. Next, there is an uncertainty on the main flux component,
$\nu_{\mu}$ ($\overline{\nu}_{\mu}$) in neutrino (antineutrino) mode, and an
individual uncertainty for each of the intrinsic background components. These
uncertainties are uncorrelated between the neutrino and antineutrino modes,
but must be correlated among the detectors and different channels of the same
mode. We include a normalization uncertainty on each individual CC cross
section for neutrinos and antineutrinos independently, but we also include
penalties on the ratios between $\nu_{\mu}/\nu_{e}$ and
$\overline{\nu}_{\mu}/\overline{\nu}_{e}$ cross sections, since they might be
better constrained than individual measurements. Similarly, we include an
uncertainty on the ratio of cross sections between neutrinos and
antineutrinos. Since we include NC interactions in our analyses, there is an
additional uncertainty on the NC cross section. In order to be conservative,
in the NC channels we do not only use the “Flux error background” from Table
1, due to flux-contamination, but we also include an additional uncertainty on
the overall background. In our analyses we will consider an optimistic, a
default, and a conservative set of uncertainties as indicated in Table 1. It
should be noted that recently an analysis has been performed updating the
estimates for some of the cross section related uncertainties [19]. The
authors obtained that most of the uncertainties for the ratios lie between our
default and optimistic choices, but the uncertainty for the
$\overline{\nu}_{e}/\overline{\nu}_{\mu}$ ratio is even better than our
optimistic choice. Using these new values as default (and, e.g., the new
values scaled by 1/2 and 2 factors for the optimistic and conservative
choices) would only have marginal impact on our results.

For our statistical analysis we use the $\chi^{2}$ function

$\chi^{2}(\vec{p})=\min_{\vec{\alpha}}\left\\{\sum_{\text{D}}\sum_{\text{C}}2\sum_{i=1}^{50}P^{\text{DC}}_{i}(\vec{p},\vec{\alpha})-D^{\text{DC}}_{i}+D^{\text{DC}}_{i}\log(D^{\text{DC}}_{i}/P^{\text{DC}}_{i}(\vec{p},\vec{\alpha}))\right\\}+\sum_{k}(\alpha_{k}/\sigma_{k})^{2}+\chi^{2}_{\text{pen.}}\,,$
(1)

where $\vec{p}$ is a set of neutrino oscillation parameters, $\vec{\alpha}$
are the systematic uncertainties with corresponding penalties $\sigma_{k}$,
$D^{\text{DC}}_{i}$ is the simulated fake data in the $i$th energy bin for the
detector D and the channel C, and $P^{\text{DC}}_{i}(\vec{p},\vec{\alpha})$ is
the corresponding prediction in the same bin, which depends on the oscillation
parameters $\vec{p}$ and the systematic uncertainties $\vec{\alpha}$. Finally,
$\chi^{2}_{\text{pen.}}$ contains a penalty for $\theta_{13}$ taken from Ref.
[20]. The first two sums are taken over the near and far detectors (D) and
over the different detection channels (C).

Uncertainty | Opt. | Def. | Con.
---|---|---|---
Fiducial volume ND | 0.2% | 0.5% | 1%
Fiducial volume FD | 1% | 2.5% | 5%
Flux error signal $\nu$ | 5% | 7.5% | 10%
Flux error background $\nu$ | 10% | 15% | 20%
Flux error signal $\bar{\nu}$ | 10% | 15% | 20%
Flux error background $\bar{\nu}$ | 20% | 30% | 40%
NC background | 5% | 7.5% | 10%
CC cross section | 10% | 15% | 20%
NC cross section | 10% | 15% | 20%
$\nu_{e}$/$\nu_{\mu}$ ratio | 3.5% | 11% | 22%
$\nu$/$\overline{\nu}$ ratio | 3.5% | 11% | 22%
Table 1:  The systematic uncertainties considered in this paper. See the text
for more details.

##  III CP-sensitivity

In this section we compare the sensitivity to measure CP violation for our
2-detector configuration with and without NC channels with the single detector
analysis. We calculate the sensitivity to exclude $\delta_{13}=0$ and
$\delta_{13}=\pi$ as a function of the true value of $\delta_{13}$. In order
to create the fake data, we have fixed the remaining parameters to

$\displaystyle\Delta m_{21}^{2}=7.5\times 10^{-5}\text{eV}^{2},\qquad\Delta
m_{31}^{2}=2.5\times 10^{-3}\text{eV}^{2}$
$\displaystyle\sin^{2}\theta_{12}=0.32,\quad\sin^{2}\theta_{13}=0.022,\quad\sin^{2}\theta_{23}=0.5\,,$
(2)

in accordance with the allowed regions obtained from recent global analyses
[20, 21, 22]. In the analysis we marginalize over $\theta_{13}$ (using the
prior from Ref. [20]) and $\theta_{23}$ (freely). Since the upcoming JUNO
experiment [23] is going to measure soon the other three parameters with a
precision below 1%, we keep them fixed in the analysis.

Figure 1 shows the results of our analyses using only the far detector (dotted
lines), using both detectors (dashed lines), and using both detectors
including NC channels (solid lines) for the conservative (orange), default
(blue) and optimistic (green) set of systematic uncertainties from Table 1. We
find that the inclusion of the near detector improves the sensitivity, while
the addition of NC channels has only a marginal effect. The sensitivity could
be further enhanced by adding an atmospheric neutrino sample, which could be
detected at the far detector [24].

Figure 1: The sensitivity to measure CP violation at ESS$\nu$SB for different
choices of systematic uncertainties and detector configurations.

##  IV Non-standard interactions

We turn our attention now to some BSM scenarios and discuss the sensitivity of
ESS$\nu$SB to the parameters in each scenario. In this section we consider
neutral-current (NC) neutrino non-standard interactions (NSI) generated by
very heavy vector mediators which are described by the effective four-fermion
interaction Lagrangian (see the reviews in Refs. [25, 26, 27, 28])

$\mathcal{L}_{\text{NSI}}^{\text{NC}}=-\sqrt{2}G_{\text{F}}\sum_{\alpha,\beta=e,\mu,\tau}\overline{\nu_{\alpha
L}}\gamma^{\rho}\nu_{\beta
L}\sum_{f=e,u,d}\overline{f}\gamma_{\rho}\left(\varepsilon_{\alpha\beta}^{fV}-\varepsilon_{\alpha\beta}^{fA}\gamma_{5}\right)f,$
(3)

where $G_{\text{F}}$ is the Fermi constant. This choice of parameterization of
the NSI interaction Lagrangian is useful because the Standard Model neutral-
current weak interaction Lagrangian can be obtained with the substitutions
$\varepsilon_{\alpha\beta}^{fV}\to g_{V}^{f}\delta_{\alpha\beta}$ and
$\varepsilon_{\alpha\beta}^{fA}\to g_{A}^{f}\delta_{\alpha\beta}$, where
$g_{V}^{f}$ and $g_{A}^{f}$ are the Standard Model vector and axial neutral
current couplings of the fermion $f$ (see, e.g., Table 3.6 of Ref. [29]).
Therefore, the ratios $\varepsilon_{\alpha\beta}^{fV}/g_{V}^{f}$ and
$\varepsilon_{\alpha\beta}^{fA}/g_{A}^{f}$ describe the size of non-standard
interactions relative to the Standard Model vector and axial neutral-current
weak interactions. Note that, contrary to the Standard Model neutral-current
weak interactions, non-standard interactions can generate neutrino flavor
transitions for $\alpha\neq\beta$.

The effective Hamiltonian which describes neutrino propagation in unpolarized
matter depends on the following combinations of the vector NSI couplings:

$\varepsilon_{\alpha\beta}=\varepsilon_{\alpha\beta}^{eV}+\dfrac{N_{u}}{N_{e}}\,\varepsilon_{\alpha\beta}^{uV}+\dfrac{N_{d}}{N_{e}}\,\varepsilon_{\alpha\beta}^{dV}\,,$
(4)

where $N_{e}$, $N_{u}$, and $N_{d}$ are, respectively, the number densities of
electrons, up quarks, and down quarks. Since in long-baseline neutrino
oscillation experiments neutrinos propagate in the crust of the Earth where
the electron, proton and neutron number densities are approximately equal, we
consider the effective NSI parameters [30, 31]

$\varepsilon_{\alpha\beta}=\varepsilon_{\alpha\beta}^{eV}+3\varepsilon_{\alpha\beta}^{uV}+3\varepsilon_{\alpha\beta}^{dV}.$
(5)

In general, these NSI parameters are complex and can be written as

$\varepsilon_{\alpha\beta}=|\varepsilon_{\alpha\beta}|e^{i\phi_{\alpha\beta}}.$
(6)

We take into account the constraint
$\varepsilon_{\alpha\beta}=\varepsilon_{\beta\alpha}^{*}$, which follows from
the hermiticity of the Lagrangian.

In Refs. [30, 31], these neutral-current non-standard interactions have been
suggested as a solution of the disagreement of the measurements of
$\delta_{13}$ in the T2K [32] and NOvA [33] experiments. Here we investigate
if ESS$\nu$SB can test the region of parameter space preferred by these
analyses. The solution of the disagreement of the measurements of
$\delta_{13}$ in the T2K [32] and NOvA [33] experiments obtained in Refs. [30,
31] with non-standard interactions requires non-zero values of
$\epsilon_{e\mu}$ or $\epsilon_{e\tau}$. In order to see if ESS$\nu$SB can
test the allowed regions of these NSI parameters obtained in Refs. [30, 31],
we consider them one at a time, as done in Refs. [30, 31]. In other words,
when we consider $\epsilon_{e\mu}$ ($\epsilon_{e\tau}$) all the other NSI
parameters are kept fixed at $\epsilon_{\alpha\beta}=0$, including
$\epsilon_{e\tau}$ ($\epsilon_{e\mu}$). On the other hand, as in the Section
III, we marginalize over the standard neutrino mixing parameters, which in
this case include also $\delta_{13}$.

The results of our analysis are presented in Fig. 2, which shows the
sensitivity regions of ESS$\nu$SB in the $|\epsilon_{e\mu}|$-$\phi_{e\mu}$ and
and $|\epsilon_{e\tau}|$-$\phi_{e\tau}$ planes at 90% confidence level for the
1-detector (dotted) and 2-detector analysis without (dashed) and with (solid)
NC channels for the optimistic (green), default (blue) and conservative
(orange) choice of systematic uncertainties, as discussed in Section II. In
Fig. 2, we also depicted in magenta the boundary of the $90\%$ allowed regions
extracted from Ref. [30] and in cyan the one from the IceCube DeepCore
analysis [34].

In the case of $\epsilon_{e\mu}$-$\phi_{e\mu}$ we find that ESS$\nu$SB will be
able to disfavor an important part of the preferred region of Ref. [30] at 90%
confidence. In the case of $\epsilon_{e\tau}$-$\phi_{e\tau}$ ESS$\nu$SB can
exclude a larger part of the preferred region than in the
$\epsilon_{e\mu}$-$\phi_{e\mu}$ case. In both cases the ESS$\nu$SB
sensitivities are competitive with the current bounds from IceCube DeepCore.

Figure 2: The expected exclusion region in the
$\epsilon_{e\mu}$-$\delta_{e\mu}$ and $\epsilon_{e\tau}$-$\delta_{e\tau}$
planes at 90% C.L. for different choices of systematic uncertainties. Also
shown are the allowed region extracted from Ref. [30] and the bounds from Ref.
[34].

We also investigated the effect that NSI could have on the CP sensitivity of
ESS$\nu$SB. To illustrate this problem we fixed $|\epsilon_{e\mu}|=0.15$
(which is the best fit value of Ref. [30]) and we calculated several fake data
sets varying $|\phi_{e\mu}|$ and $\delta_{13}$. Next, we calculated the
$\chi^{2}$ for excluding any CP conserving combination of CP phases. The
results of this analysis are shown in Fig. 3. The bands are generated by the
variation of $\phi_{e\mu}$ in the fake data. It should be noted that these
bands do not go to zero close to $\delta_{13}=0$ and $\delta_{13}=\pi$.
Indeed, for the case of optimistic systematic uncertainties they vary from 0
to about 4$\sigma$. This means that even if $\delta_{13}=0$ or
$\delta_{13}=\pi$, ESS$\nu$SB can have the capability to measure possible CP
violation due to $|\phi_{e\mu}|$ if $|\epsilon_{e\mu}|$ is large enough.

Figure 3: The impact NSI could have on the measurement of CP violation at
ESS$\nu$SB for different choices of systematic uncertainties. The bands result
from varying $\phi_{e\mu}$ in the fake data. The dashed lines, corresponding
to the standard analysis without NSI, are the same as in Fig. 1 for the
analysis with two detectors and NC channels.

##  V Nonunitary neutrino mixing

In this section we consider nonunitary neutrino mixing. An effective
nonunitary $3\times 3$ neutrino mixing matrix can be the result of the
presence of heavy neutral leptons which mix with the three light neutrinos,
but do not participate in neutrino oscillations because they cannot be
produced in low-energy experiments. This can happen, for example, in the case
of the Type-I seesaw mechanism. In the traditional high-scale Type-I seesaw
mechanism the nonunitarity of the effective $3\times 3$ neutrino mixing matrix
is negligible. However, larger deviations from unitarity are generally
expected in low-scale Type-I seesaw models, such as those which implement the
inverse and linear seesaw mechanisms [35, 36, 37, 38, 39, 40, 41].

If there are $n$ neutral leptons, of which three are the ordinary light
neutrinos and $n-3$ are heavy neutral leptons, the effective low-energy
nonunitary $3\times 3$ neutrino mixing matrix $N$ is a submatrix of the
complete $n\times n$ unitary mixing matrix

$U^{n\times n}=\begin{pmatrix}N&S\\\ V&T\end{pmatrix}\,,$ (7)

where $S$, $V$, and $T$ are, respectively, $3\times(n-3)$, $(n-3)\times 3$,
and $(n-3)\times(n-3)$ matrices. The nonunitary $3\times 3$ mixing matrix $N$
can be written as [42]

$N=N^{NP}U=\begin{pmatrix}\alpha_{11}&0&0\\\ \alpha_{21}&\alpha_{22}&0\\\
\alpha_{31}&\alpha_{32}&\alpha_{33}\end{pmatrix}U\,,$ (8)

where $U$ is the standard unitary three-neutrino mixing matrix. The nonunitary
new physics effects are encoded in the triangular matrix $N^{NP}$, which
depends on three real positive diagonal parameters $\alpha_{ii}$, and three
complex parameters $\alpha_{ij}$ for $i\neq j$. Moreover, the off-diagonal
parameters are bounded by the inequality [43, 44]

$|\alpha_{ij}|\leq\sqrt{(1-\alpha_{ii}^{2})(1-\alpha_{jj}^{2})}\,,$ (9)

and, for small unitarity violations, the diagonal parameters are close to one.

The general expression of the probability of $\nu_{\alpha}\to\nu_{\beta}$
oscillations in vacuum is

$P_{\alpha\beta}=|(NN^{\dagger})_{\alpha\beta}|^{2}-4\sum_{k>j}\text{Re}\\!\left[N_{\alpha
k}^{*}N_{\beta k}N_{\alpha j}N_{\beta
j}^{*}\right]\sin^{2}\\!\left(\frac{\Delta
m_{kj}^{2}L}{4E}\right)+2\sum_{k>j}\text{Im}\\!\left[N_{\alpha k}^{*}N_{\beta
k}N_{\alpha j}N_{\beta j}^{*}\right]\sin\\!\left(\frac{\Delta
m_{kj}^{2}L}{2E}\right).$ (10)

The first term of this probability is not equal to $\delta_{\alpha\beta}$ as
in the unitary case and depends only on the values of the nonunitarity
$\alpha$ parameters (see Eq. (A5) of Ref. [44]). Therefore, in the case of
nonunitary neutrino mixing it is possible to have a zero-distance flavor
conversion.

In this section we discuss the sensitivity of ESS$\nu$SB to the nonunitarity
parameters. The role of the near detector is of particular importance, because
the zero-distance effect can alter the event rate at the near detector
dramatically.

ESS$\nu$SB is mainly sensitive to the nonunitarity parameters $\alpha_{22}$,
$\alpha_{11}$, and $|\alpha_{21}|$ through the $\nu_{\mu}$ and $\nu_{e}$
disappearance channels and the $\nu_{\mu}\to\nu_{e}$ appearance channel. The
results of our analysis are shown in Fig. 4, which has been obtained by
marginalizing over the standard three neutrino mixing parameters, over the
phase of $\alpha_{21}$, and over $|\alpha_{21}|$ ($\alpha_{11}$) in the left
(right) panel. Also shown, for the comparison with the sensitivity of
ESS$\nu$SB, are the current bounds obtained in Ref. [44]. We show again the
ESS$\nu$SB sensitivities for the different choices of uncertainties and for
the 1-detector and the 2-detector analyses with and without NC channels. As
one can see from the figure, ESS$\nu$SB can only set bounds similar to the
current ones on the diagonal parameters $\alpha_{11}$ and $\alpha_{22}$.
However, an important improvement can be expected in the case of
$|\alpha_{21}|$. It should also be noted that the inclusion of NC events helps
to improve the sensitivity on each parameter importantly.

The contours of Fig. 4 have been obtained keeping $\alpha_{3j}$ fixed at their
unitary values ($\alpha_{31}=\alpha_{32}=0$ and $\alpha_{33}=1$). However,
they can affect the ESS$\nu$SB sensitivity since they change the oscillation
probability through matter effects. On the other hand, we can also bound these
parameters directly by observation of the NC channels111Since the ESS$\nu$SB
sensitivity to the $\alpha_{3j}$ parameters without NC channels is very weak,
we do not discuss it here.. From here, we focus the discussion on the analysis
using both detectors and including the NC channels. In the left panel of Fig.
5 we show how the marginalization of $\alpha_{33}$ (the effects of
$|\alpha_{31}|$ and $|\alpha_{32}|$ are negligible in comparison with
$\alpha_{33}$) affects the sensitivity. The solid lines have been obtained by
marginalizing over $\alpha_{33}$, while the dashed lines correspond to the
previous analysis where $\alpha_{33}$ was kept fixed at the unitary value. As
one can see, the sensitivity to $\alpha_{11}$ is practically unaffected by the
different assumptions on the values of $\alpha_{33}$. On the other hand, the
sensitivity to $\alpha_{22}$ is weakened by the marginalization over
$\alpha_{33}$. We have also found that the marginalization over the
$\alpha_{3j}$ parameters does not affect the sensitivity to $|\alpha_{21}|$.
When bounding the non-diagonal parameters, two effects must be considered.
First, the parameters can enter directly the oscillation probabilities.
Second, if we obtain strong bounds on two diagonal parameters, we can place a
strong bound on the corresponding non-diagonal parameter through Eq. (9). In
our analysis the contribution of Eq. (9) to the bound on $|\alpha_{21}|$ is
weak. Therefore, the weaker bound on $\alpha_{22}$ that is obtained after
marginalization over $\alpha_{33}$ does not affect the bound on
$|\alpha_{21}|$.

In the right panel of Fig. 5 we show the sensitivity in the
$(1-\alpha_{33})-(1-\alpha_{22})$ plane. The solid lines represent the
sensitivity of ESS$\nu$SB alone. As can be seen, a correlation between the
parameters reduces the sensitivity to $\alpha_{22}$ when $1-\alpha_{33}$ is
relatively large. Note, that ESS$\nu$SB can improve the current bound (magenta
lines) on $\alpha_{33}$. In Fig. 5, we also show the sensitivity that can be
obtained by combining the ESS$\nu$SB sensitivity with the current bounds.
Since the current bound on $\alpha_{22}$ is better than the ESS$\nu$SB
sensitivity, the inclusion of the current bound breaks the degeneracy between
the parameters, leading to a great improvement of the combined sensitivity to
$\alpha_{33}$. As can be seen from the figure, the combined sensitivity to
$\alpha_{33}$ marginalized over $\alpha_{22}$ is about one order of magnitude
better than that of ESS$\nu$SB alone for any choice of systematic
uncertainties.

The left panel of Fig. 6 shows the sensitivity of ESS$\nu$SB to each of the
nonunitarity parameters $\alpha_{11}$ (blue), $\alpha_{22}$ (green), and
$|\alpha_{21}|$ (orange) for the 2-detector analysis with NC channels, for
different choices of systematic uncertainties, in comparison with the current
bounds obtained in Ref. [44] (dotted-dashed lines). The $\Delta\chi^{2}$ for
each parameter has been obtained by marginalizing over all the other
parameters. This figure highlights the important improvement that can be
expected on the bound on $|\alpha_{21}|$, which is only slightly affected by
the choice of uncertainties, unlike in the case of $\alpha_{11}$ and
$\alpha_{22}$, where the bounds get considerably worse when allowing for
larger uncertainties. In the right panel we show the bounds that can be
obtained on the $\alpha_{3j}$ parameters. In this case we have considered two
scenarios. First, we considered the ESS$\nu$SB sensitivity alone. As can be
seen in the figure, ESS$\nu$SB can improve the current bound on $\alpha_{33}$,
but not on the non-diagonal $\alpha_{3j}$ parameters. However, once we include
the current bound on $\alpha_{22}$, the constraints on all parameters improve
and become stronger than the current bounds. This happens due to the fact
that, unlike in the case of $|\alpha_{21}|$, the main contribution to the
bounds of $|\alpha_{31}|$ and $|\alpha_{32}|$ comes from Eq. (9). Therefore,
an improvement of the bounds on $\alpha_{33}$ and $\alpha_{22}$ has an
important impact on the sensitivity.

The sensitivity of ESS$\nu$SB to the nonunitarity of the neutrino mixing
matrix has been already studied in Ref. [12] considering only the far detector
in a one-detector analysis. The authors obtain similar bounds to ours in the
case of $|\alpha_{21}|$. However, the bounds obtained for $\alpha_{11}$ and
$\alpha_{22}$ are much stronger there. This happens due to a different
treatment of systematic uncertainties. In Ref. [12] only an overall
uncertainty on the signal and background of each channel has been considered,
while we treat each background component individually. Therefore, our more
conservative treatment of uncertainties leads to more conservative
sensitivities.

Figure 4: The expected region in different planes of the nonunitarity $\alpha$
parameters at 2$\sigma$ for different choices of systematic uncertainties.
Also shown are the current bounds taken from Ref. [44].

Figure 5: Left: Comparison of the ESS$\nu$SB sensitivities in the
$(1-\alpha_{11})-(1-\alpha_{22})$ plane obtained marginalizing over
$\alpha_{33}$ (solid lines) and keeping $\alpha_{33}=1$ fixed (dashed lines).
The dashed lines in this figures are the same as the solid lines in Fig. 4.
Right: The bounds in the $(1-\alpha_{33})-(1-\alpha_{22})$ plane than can be
obtained from an analysis of ESS$\nu$SB data alone and from a combined
analysis with the current bounds. In both panels we also show the current
bounds taken from Ref. [44].

Figure 6: The $\Delta\chi^{2}$ profiles for the ESS$\nu$SB sensitivity for the
2-detector analysis including NC channels to the nonunitarity parameters
$\alpha_{11}$, $\alpha_{22}$, and $|\alpha_{21}|$ (left panel) and
$\alpha_{33}$, $|\alpha_{31}|$, and $|\alpha_{32}|$ (right panel), in
comparison with the profiles obtained in Ref. [44]. The horizontal solid black
line shows the $\Delta\chi^{2}=2.71$ corresponding to 90% C.L.

Finally, let us discuss how nonunitary neutrino mixing could affect the CP
sensitivity at ESS$\nu$SB. In order to show the impact, we fixed
$\alpha_{11}=0.99$, $\alpha_{22}=0.998$, and $|\alpha_{21}|=0.007$. These
values lie within the bounds of the current analysis in Ref. [44], while lying
within the sensitivity range of ESS$\nu$SB (for $|\alpha_{21}|$). We generated
fake data sets varying $\delta_{13}$ and $\phi_{21}$, which is the CP phase
associated to $|\alpha_{21}|$, and we computed the sensitivity to exclude all
CP-conserving combinations of phases. We consider only the case of two
detectors with NC channels here. The results of this analysis are shown in
Fig. 7. The value of $\delta_{13}$ is varied on the $x$-axis and the width of
the bands is obtained from varying $\phi_{21}$. The dashed lines,
corresponding to the standard analysis, are the same as those obtained in Sec.
III. As can be seen, the presence of nonunitarity has small effects on the
overall CP sensitivity. It should be noted that the bands to not go to zero
around $\delta_{13}=0$ (and $2\pi$) and $\delta_{13}=\pi$. This is due to the
fact that even if there is no CP violation due to $\delta_{13}$, there might
be CP violation due to $\phi_{21}$ to which ESS$\nu$SB is sensitive. Here we
have discussed only the effect of $\phi_{21}$. The width of the bands could be
slightly increased further if we added the contributions of $\phi_{31}$ and
$\phi_{32}$. However, the effects of these phases are expected to be smaller
than those of $\phi_{21}$. We remind that the bounds on $|\alpha_{31}|$ and
$|\alpha_{32}|$ presented above have been obtained from the relation in Eq.
(9), since these parameters have only marginal effect on the oscillation
probabilities considered here. This means that if CP was violated due to
$\phi_{31}$ or $\phi_{32}$ (and not $\phi_{21}$ or $\delta_{13}$), ESS$\nu$SB
would most likely not see it.

Figure 7: The impact nonunitary neutrino mixing could have on the measurement
of CP violation at ESS$\nu$SB for different choices of systematic
uncertainties. The width of the bands result from varying $\phi_{21}$ in the
fake data. The dashed lines correspond to the standard analyses and are the
same as in Fig. 1.

##  VI Light sterile neutrinos

In this section we study the ESS$\nu$SB sensitivity to neutrino oscillations
generated by the mixing of the three active neutrinos $\nu_{e}$, $\nu_{\mu}$,
$\nu_{\tau}$ with a sterile neutrino $\nu_{s}$ which is mainly composed by a
new neutrino mass eigenstate $\nu_{4}$ having a mass $m_{4}\gtrsim
1\,\text{eV}$. This mass is light, but heavier than the masses $m_{1}$,
$m_{2}$, $m_{3}$ of the three standard neutrino mass eigenstates $\nu_{1}$,
$\nu_{2}$, $\nu_{3}$ which are constrained below the eV scale by $\beta$ decay
[45], neutrinoless double-$\beta$ decay [46] and cosmological [47] bounds. In
this scenario, called “3+1”, there is a new squared-mass difference
$\Delta{m}^{2}_{41}\equiv m_{4}^{2}-m_{1}^{2}\gtrsim 0.1\leavevmode\nobreak\
\text{eV}^{2}$ which is much larger than the solar and atmospheric neutrino
oscillations squared-mass differences, which generate the oscillations
observed in solar, atmospheric and long-baseline neutrino oscillation
experiments (see, e.g., the review in Ref. [48] and the recent three-neutrino
global analyses in Refs. [20, 22, 21]). The new squared-mass difference
$\Delta{m}^{2}_{41}$ generates short-baseline neutrino oscillations which may
explain, at least partially, the anomalies found in short-baseline neutrino
oscillation experiments: the Gallium Anomaly, the Reactor Antineutrino
Anomaly, and the LSND and MiniBooNE anomalies (see the reviews in Refs. [49,
50, 51, 52, 53, 54, 55]).

In the 3+1 scenario, the effective probabilities of neutrino oscillations in
vacuum in short-baseline experiments are given by

$P_{\nu_{\alpha}\to\nu_{\beta}}^{\text{SBL}}=\left|\delta_{\alpha\beta}-\sin^{2}2\vartheta_{\alpha\beta}\sin^{2}\\!\left(\frac{\Delta{m}^{2}_{41}L}{4E}\right)\right|,$
(11)

with the oscillation amplitudes given by the effective mixing parameters

$\sin^{2}2\vartheta_{\alpha\beta}=4|U_{\alpha
4}|^{2}\left|\delta_{\alpha\beta}-|U_{\beta 4}|^{2}\right|.$ (12)

These oscillation amplitudes depend on the absolute values of the elements in
the fourth column of the $4\times 4$ unitary mixing matrix $U$. Therefore, the
effective oscillation probabilities of neutrinos and antineutrinos in short-
baseline experiments are equal. There is, however, a difference between the
oscillation probabilities of neutrinos and antineutrinos at longer distances,
as those of long-baseline experiments [56, 57, 58, 59, 60, 61, 62, 63, 10],
where the effects of all the complex phases in the mixing matrix are
observable.

The elements of the fourth column of the mixing matrix must be small, because
3+1 active-sterile neutrino mixing must be a small perturbation of the
standard three-neutrino mixing which fits very well the robust data of solar,
atmospheric and long-baseline neutrino oscillation experiments [20, 22, 21].

In the standard parameterization of the $4\times 4$ unitary mixing matrix $U$
(see, e.g., Refs. [51, 53]) we have

$U_{e4}=\sin\vartheta_{14}\,e^{-i\delta_{14}}\quad\text{and}\quad U_{\mu
4}=\cos\vartheta_{14}\sin\vartheta_{24}\simeq\sin\vartheta_{24}.$ (13)

The approximation takes into account the smallness of the new mixing angle
$\vartheta_{14}$. Hence, the effective mixing parameters in short-baseline
$\nu_{e}$ and $\nu_{\mu}$ disappearance experiments are given by,
respectively,

$\displaystyle\hbox{}\sin^{2}2\vartheta_{ee}=4|U_{e4}|^{2}\left(1-|U_{e4}|^{2}\right)=\sin^{2}2\vartheta_{14},$
(14) $\displaystyle\hbox{}\sin^{2}2\vartheta_{\mu\mu}=4|U_{\mu
4}|^{2}\left(1-|U_{\mu 4}|^{2}\right)\simeq\sin^{2}2\vartheta_{24}.$ (15)

The effective mixing parameter in short-baseline $\nu_{\mu}\to\nu_{e}$
appearance experiments has the more complicated expression

$\sin^{2}2\vartheta_{\mu e}=4|U_{e4}|^{2}|U_{\mu
4}|^{2}=\sin^{2}2\vartheta_{14}\sin^{2}\vartheta_{24}\simeq\dfrac{1}{4}\,\sin^{2}2\vartheta_{ee}\sin^{2}2\vartheta_{\mu\mu}.$
(16)

The approximation follows from the smallness of the new mixing angles
$\vartheta_{14}$ and $\vartheta_{24}$.

Considering the ESS$\nu$SB average neutrino energy $E\simeq 400\,\text{MeV}$
[4], the oscillation phase at the near detector ($L\simeq 250\,\text{m}$) is
$\Delta{m}^{2}_{41}L/4E\gtrsim 0.8$ for $\Delta{m}^{2}_{41}\gtrsim
1\,\text{eV}^{2}$. Therefore, the short-baseline oscillations generated by
$\Delta{m}^{2}_{41}$ may be observable at the ESS$\nu$SB near detector and
average out at longer distances as that of the far detector. Hence, in a two-
detector analysis the sensitivity to active-sterile neutrino mixing is due to
the ESS$\nu$SB near detector and the far detector reduces the systematic
uncertainties. Note that in the calculation of the oscillation probability at
the far detector matter effects must be included.

Figure 8 shows the results of our analysis. As in the analyses presented in
the previous Sections, we marginalized over the standard three-neutrino
oscillation parameters. The three panels in Fig. 8 show the ESS$\nu$SB
sensitivity in the 8 $\sin^{2}2\vartheta_{14}$-$\Delta{m}^{2}_{41}$, 8
$\sin^{2}2\vartheta_{24}$-$\Delta{m}^{2}_{41}$, and 8 $\sin^{2}2\vartheta_{\mu
e}$-$\Delta{m}^{2}_{41}$ planes. Each of them has been obtained by
marginalizing over the other active-sterile mixing angles. Again we plot the
results using a single detector analysis (dotted lines), and a 2-detector
analysis without (dashed lines) and with (solid lines) the inclusion of NC
channels for the conservative (orange), default (blue) and optimistic (green)
choices of systematic uncertainties. It is noteworthy that the inclusion of
the near detector and the NC channels improves the sensitivity in all panels,
while the different choices of systematic uncertainties only show some effects
for very small and very large $\Delta m_{41}^{2}$. The reason is that for most
of the range of $\Delta m_{41}^{2}$ plotted in the figure oscillations appear
at the near detector inducing spectral distortions, while the far detector
would observe only an averaged oscillation probability. Due to the different
effects of the neutrino oscillation probability at the near and far detectors,
the systematic uncertainties (many of which are correlated among detectors)
could not cancel an oscillation effect and hence the sensitivity does not
depend on the choice of uncertainty. It has been shown [10], however, that the
inclusion of shape uncertainties can worsen the sensitivity in this region.
This type of uncertainty has not been considered here.

Figure 8 shows a comparison of the ESS$\nu$SB sensitivity in the
$\sin^{2}2\vartheta_{14}$-$\Delta{m}^{2}_{41}$ plane with the allowed regions
at 2$\sigma$ obtained in Ref. [64] from the analysis of the data of the GALLEX
[65, 66, 67], SAGE [68, 69, 70, 71], and BEST [72, 73] Gallium experiments
which have been obtained using the traditional Bahcall cross section model
[74]. These Gallium allowed regions are representative of the general allowed
regions which can be obtained from the Gallium data, because other cross
section models lead to similar regions [64, 75, 76]. They lie at large values
of $\sin^{2}2\vartheta_{14}$, which are incompatible with the requirement of
small active-sterile neutrino mixing discussed above. One can see that
ESS$\nu$SB is sensitive to the Gallium allowed region and can rule out the 3+1
neutrino oscillation explanation of the Gallium Anomaly. In the case of
optimistic uncertainties even the 1-detector analysis is capable of excluding
most of the Gallium $2\sigma$ preferred region. Therefore, ESS$\nu$SB can also
test the regions obtained by the Neutrino-4 collaboration [77], which require
similarly large mixing angles as the Gallium data. The Neutrino-4 results are,
however, controversial [78, 79, 80, 81].

In Fig. 8 we depicted also the allowed regions at $2\sigma$ obtained in Ref.
[64] from the combined analysis of the data of short-baseline $\nu_{e}$ and
$\bar{\nu}_{e}$ disappearance experiments, excluding the Gallium data222The
shape and significance of the allowed regions depend on the analysis of the
reactor spectral ratio data and the reactor rate data. Since at 2$\sigma$ the
differences are small, we show here only one representative example, which
corresponds to RSRF(N/DB)+KI in Fig. 10 of Ref. [64]. The interested reader is
referred to the discussions in Refs. [82, 64].. Since these regions lie at
small values of $\sin^{2}2\vartheta_{14}$, they satisfy the requirement of
small active-sterile neutrino mixing discussed above. As one can see from Fig.
8, the sensitivity of ESS$\nu$SB is not enough to probe these
$\nu_{e}$-disappearance allowed regions when considering the 1-detector
analysis or the 2-detector analysis without NC channels, which does not allow
probing large parts of the preferred $2\sigma$ regions. However, if the NC
channels are included, the island at $\Delta{m}^{2}_{41}\approx
1.3\,\text{eV}^{2}$ lies fully within the ESS$\nu$SB sensitivity reach, and
also a large part of the island at $\Delta{m}^{2}_{41}\approx
0.4\,\text{eV}^{2}$ can be probed.

Figure 8 shows a comparison of the ESS$\nu$SB sensitivity in the
$\sin^{2}2\vartheta_{24}$-$\Delta{m}^{2}_{41}$ plane with the current global
$3\sigma$ bound, which corresponds to the bound of Ref. [51] updated with the
latest IceCube data [83]. There is no allowed region from current data,
because the data of all $\nu_{\mu}$ and $\bar{\nu}_{\mu}$ disappearance
experiments are compatible with three-neutrino mixing, without any anomaly.
From Fig. 8, one can see that ESS$\nu$SB can improve the current bounds for
$\Delta m_{41}^{2}\gtrsim 0.3\,\text{eV}^{2}$ and $\Delta m_{41}^{2}\lesssim
40\,\text{eV}^{2}$ using two detectors. The sensitivity can be further
improved when including the NC channels.

Figure 8 shows the sensitivity of ESS$\nu$SB in the $\sin^{2}2\vartheta_{\mu
e}$-$\Delta{m}^{2}_{41}$ plane. Let us remind that $\sin^{2}2\theta_{\mu e}$,
given in Eq. 16, is the effective mixing parameter relevant for appearance
experiments. Figure 8 shows also the region preferred at $3\sigma$ from a
global analysis of appearance experiments [51]. One can see that this allowed
region can be tested very well in ESS$\nu$SB.

Figure 8: Sensitivity reach of ESS$\nu$SB in the 8
$\sin^{2}2\vartheta_{14}$-$\Delta{m}^{2}_{41}$ (at $2\sigma$), 8
$\sin^{2}2\vartheta_{24}$-$\Delta{m}^{2}_{41}$ (at $3\sigma$), and 8
$\sin^{2}2\vartheta_{\mu e}$-$\Delta{m}^{2}_{41}$ (at $3\sigma$) planes. For
comparison, in 8 we show also the regions preferred by the Gallium data and
the regions preferred by the global $\nu_{e}$ disappearance analysis without
Gallium data [64], in 8 we show the bound obtained from a global $\nu_{\mu}$
disappearance analysis (the bound in Ref. [51] updated with the latest IceCube
data [83]), and in 8 we show the preferred region obtained from a global
$\nu_{e}$ appearance analysis [51].

Finally, as in the previous sections, we estimate how much the presence of a
light sterile neutrino might affect the sensitivity of ESS$\nu$SB to the
discovery of CP violation. We created fake data sets using as input the best
fit value of the analysis in Ref. [64], i.e. $\Delta
m_{41}^{2}=1.3\,\text{eV}^{2}$, $\sin^{2}2\theta_{14}=0.022$. In addition we
chose $\sin^{2}2\theta_{24}=0.022$, which is allowed from current data, but
lies within the sensitivity range of ESS$\nu$SB. Note that in order to obtain
some measurable effect from $\delta_{14}$, which is the CP phase of interest
here, both $\theta_{14}$ and $\theta_{24}$ must be different from zero. As in
the previous sections, we generated fake data sets varying $\delta_{13}$ and
also the new phase $\delta_{14}$, and then we marginalized over the CP
conserving combinations of CP phases. The results of this analysis are shown
in Fig. 9. As one can see, in the case of a sterile neutrino the sensitivity
to measure $\delta_{13}$ is slightly reduced. However, even at $\delta_{13}=0$
and $\delta_{13}=\pi$, there is still potential to observe CP violation at the
$\sim 2\sigma$ level. Note that, unlike in the case of nonunitary neutrino
mixing, the bands are partially below the sensitivity curves of the standard
analyses (dashed lines), instead of surrounding them. The same behavior has
been observed in the cases of other long baseline experiments in Ref. [60]. It
was shown that if the mixing angles are chosen to be large, the band due to
the variation of $\delta_{14}$ is wider, too. Since we chose the mixing angles
to be quite small, the full band lies partially below the lines for the
standard sensitivity.

Figure 9: The impact new mixing parameters due to a light sterile neutrino
could have on the determination of CP violation at ESS$\nu$SB for different
choices of systematic uncertainties. The width of the bands is due to the
variation of $\delta_{14}$ in the fake data. The dashed lines are the standard
sensitivities obtained in Sec. III.

Note that the results presented in this section update the results of former
analyses in Refs. [7, 9, 10]. In these references the authors used older
configurations of the experiment or positions of the near detector resulting
in slightly different sensitivities.

##  VII Summary and conclusions

We have discussed the sensitivity to CP violation and to several new physics
scenarios for ESS$\nu$SB. In particular, we have shown the improvement on the
sensitivity which can be obtained from a 2-detector fit and from the addition
of neutral current channels.

We have shown that ESS$\nu$SB will be able to test some of the parameter space
of the NSI parameters which is preferred by the current data, as shown in the
analyses of Refs. [31, 30]. It should be noted, however, that other future
experiments are expected to have similar or even better sensitivities than
ESS$\nu$SB, due to the usage of larger baselines and hence larger matter
effects [25, 26, 27, 28]. In Ref. [84] the authors suggest to use DUNE to test
the results from Refs. [31, 30]. Nevertheless, the strongest bounds on several
NSI parameters can be expected from future atmospheric neutrino experiments
[85].

In the case of nonunitary neutrino mixing we find that ESS$\nu$SB will be able
to improve some of the current bounds (e.g. $|\alpha_{21}|$), while providing
comparable bounds for other parameters ($\alpha_{11}$ and $\alpha_{22}$). A
great improvement can be expected with respect to the 1-detector analysis of
Ref. [12]. The sensitivity is similar to the one that can be expected from
DUNE [86] or T2HKK [87, 88], while improving over the sensitivities of several
other probes [87, 89, 90].

Finally we have shown that ESS$\nu$SB has excellent sensitivity to test all of
the short-baseline anomalies in the context of 3+1 neutrino mixing.
Complementary sensitivities are expected at DUNE [86], JUNO/TAO [91, 92, 93],
KM3NeT [94], and the SBN program at Fermilab [95].

Overall, we have shown that ESS$\nu$SB will be an excellent tool for the
measurement of CP violation and for the exploration of several scenarios of
physics beyond the standard model.

###### Acknowledgements.

We would like to thank Salva Rosauro-Alcaraz for providing the GLoBES files
for ESS$\nu$SB. C.A.T. is thankful for the hospitality at Università degli
Studi dell’Aquila and LNGS where part of this work was performed. C.G. and
C.A.T. are supported by the research grant “The Dark Universe: A Synergic
Multimessenger Approach” number 2017X7X85K under the program “PRIN 2017”
funded by the Italian Ministero dell’Istruzione, Università e della Ricerca
(MIUR). C.A.T. also acknowledges support from Departments of Excellence grant
awarded by MIUR and the research grant TAsP (Theoretical Astroparticle
Physics) funded by Istituto Nazionale di Fisica Nucleare (INFN).

## References

  * Baussan  _et al._ [2014] E. Baussan _et al._ (ESSnuSB), Nucl. Phys. B 885, 127 (2014), arXiv:1309.7022 [hep-ex] .
  * Wildner  _et al._ [2016] E. Wildner _et al._ , Adv. High Energy Phys. 2016, 8640493 (2016), arXiv:1510.00493 [physics.ins-det] .
  * Alekou  _et al._ [2021] A. Alekou _et al._ (ESSnuSB), Eur. Phys. J. C 81, 1130 (2021), arXiv:2107.07585 [hep-ex] .
  * Alekou  _et al._ [2022] A. Alekou _et al._ , (2022), arXiv:2203.08803 [physics.acc-ph] .
  * Agarwalla  _et al._ [2014] S. K. Agarwalla, S. Choubey, and S. Prakash, JHEP 12, 020 (2014), arXiv:1406.2219 [hep-ph] .
  * Blennow  _et al._ [2015a] M. Blennow, P. Coloma, and E. Fernandez-Martinez, JHEP 03, 005 (2015a), arXiv:1407.3274 [hep-ph] .
  * Blennow  _et al._ [2014] M. Blennow, P. Coloma, and E. Fernandez-Martinez, JHEP 12, 120 (2014), arXiv:1407.1317 [hep-ph] .
  * Blennow  _et al._ [2015b] M. Blennow, S. Choubey, T. Ohlsson, and S. K. Raut, JHEP 09, 096 (2015b), arXiv:1507.02868 [hep-ph] .
  * Kumar Agarwalla  _et al._ [2019] S. Kumar Agarwalla, S. S. Chatterjee, and A. Palazzo, JHEP 12, 174 (2019), arXiv:1909.13746 [hep-ph] .
  * Ghosh  _et al._ [2020] M. Ghosh, T. Ohlsson, and S. Rosauro-Alcaraz, JHEP 03, 026 (2020), arXiv:1912.10010 [hep-ph] .
  * Choubey  _et al._ [2021] S. Choubey, M. Ghosh, D. Kempe, and T. Ohlsson, JHEP 05, 133 (2021), arXiv:2010.16334 [hep-ph] .
  * Chatterjee  _et al._ [2022a] S. S. Chatterjee, O. G. Miranda, M. Tórtola, and J. W. F. Valle, Phys. Rev. D 106, 075016 (2022a), arXiv:2111.08673 [hep-ph] .
  * Chatterjee  _et al._ [2022b] S. S. Chatterjee, S. Lavignac, O. G. Miranda, and G. Sanchez Garcia, (2022b), arXiv:2208.11771 [hep-ph] .
  * Huber  _et al._ [2005] P. Huber, M. Lindner, and W. Winter, Comput. Phys. Commun. 167, 195 (2005), arXiv:hep-ph/0407333 .
  * Huber  _et al._ [2007] P. Huber, J. Kopp, M. Lindner, M. Rolinec, and W. Winter, Comput. Phys. Commun. 177, 432 (2007), arXiv:hep-ph/0701187 .
  * Coloma  _et al._ [2018] P. Coloma, D. V. Forero, and S. J. Parke, JHEP 07, 079 (2018), arXiv:1707.05348 [hep-ph] .
  * Abe  _et al._ [2019] K. Abe _et al._ (T2K), Phys. Rev. D 100, 112009 (2019), arXiv:1910.09439 [hep-ex] .
  * Coloma  _et al._ [2013] P. Coloma, P. Huber, J. Kopp, and W. Winter, Phys. Rev. D 87, 033004 (2013), arXiv:1209.5973 [hep-ph] .
  * Dieminger  _et al._ [2023] T. Dieminger, S. Dolan, D. Sgalaberna, A. Nikolakopoulos, T. Dealtry, S. Bolognesi, L. Pickering, and A. Rubbia, (2023), arXiv:2301.08065 [hep-ph] .
  * de Salas  _et al._ [2021] P. F. de Salas, D. V. Forero, S. Gariazzo, P. Martínez-Miravé, O. Mena, C. A. Ternes, M. Tórtola, and J. W. F. Valle, JHEP 02, 071 (2021), arXiv:2006.11237 [hep-ph] .
  * Capozzi  _et al._ [2021] F. Capozzi, E. Di Valentino, E. Lisi, A. Marrone, A. Melchiorri, and A. Palazzo, Phys. Rev. D 104, 083031 (2021), arXiv:2107.00532 [hep-ph] .
  * Esteban  _et al._ [2020] I. Esteban, M. C. Gonzalez-Garcia, M. Maltoni, T. Schwetz, and A. Zhou, JHEP 09, 178 (2020), arXiv:2007.14792 [hep-ph] .
  * Abusleme  _et al._ [2022] A. Abusleme _et al._ (JUNO), Chin. Phys. C 46, 123001 (2022), arXiv:2204.13249 [hep-ex] .
  * Blennow  _et al._ [2020] M. Blennow, E. Fernandez-Martinez, T. Ota, and S. Rosauro-Alcaraz, Eur. Phys. J. C 80, 190 (2020), arXiv:1912.04309 [hep-ph] .
  * Ohlsson [2013] T. Ohlsson, Rept.Prog.Phys. 76, 044201 (2013), arXiv:1209.2710 [hep-ph] .
  * Miranda and Nunokawa [2015] O. Miranda and H. Nunokawa, New J. Phys. 17, 095002 (2015), arXiv:1505.06254 [hep-ph] .
  * Farzan and Tortola [2018] Y. Farzan and M. Tortola, Front.in Phys. 6, 10 (2018), arXiv:1710.09360 [hep-ph] .
  * Dev  _et al._ [2019] P. S. B. Dev _et al._ , SciPost Phys.Proc. 2, 001 (2019), arXiv:1907.00991 [hep-ph] .
  * Giunti and Kim [2007] C. Giunti and C. W. Kim,  _Fundamentals of Neutrino Physics and Astrophysics_ (Oxford University Press, Oxford, UK, 2007) pp. 1–728.
  * Chatterjee and Palazzo [2021] S. S. Chatterjee and A. Palazzo, Phys. Rev. Lett. 126, 051802 (2021), arXiv:2008.04161 [hep-ph] .
  * Denton  _et al._ [2021] P. B. Denton, J. Gehrlein, and R. Pestes, Phys. Rev. Lett. 126, 051801 (2021), arXiv:2008.01110 [hep-ph] .
  * Abe  _et al._ [2021] K. Abe _et al._ (T2K), Phys.Rev. D103, 112008 (2021), arXiv:2101.03779 [hep-ex] .
  * Acero  _et al._ [2022a] M. A. Acero _et al._ (NOvA, R. Group), Phys.Rev.D 106, 032004 (2022a), arXiv:2108.08219 [hep-ex] .
  * Ehrhardt [2019] T. Ehrhardt, “Search for NSI in neutrino propagation with IceCube DeepCore,” https://indico.uu.se/event/600/contributions/1024/attachments/1025/1394/IceCube_NSI_Search_PPNT19.pdf (2019).
  * Mohapatra and Valle [1986] R. N. Mohapatra and J. W. F. Valle, Phys. Rev. D 34, 1642 (1986).
  * Akhmedov  _et al._ [1996a] E. K. Akhmedov, M. Lindner, E. Schnapka, and J. W. F. Valle, Phys. Lett. B 368, 270 (1996a), arXiv:hep-ph/9507275 .
  * Akhmedov  _et al._ [1996b] E. K. Akhmedov, M. Lindner, E. Schnapka, and J. W. F. Valle, Phys. Rev. D 53, 2752 (1996b), arXiv:hep-ph/9509255 .
  * Malinsky  _et al._ [2005] M. Malinsky, J. C. Romao, and J. W. F. Valle, Phys. Rev. Lett. 95, 161801 (2005), arXiv:hep-ph/0506296 .
  * Malinsky  _et al._ [2009a] M. Malinsky, T. Ohlsson, and H. Zhang, Phys. Rev. D 79, 073009 (2009a), arXiv:0903.1961 [hep-ph] .
  * Malinsky  _et al._ [2009b] M. Malinsky, T. Ohlsson, Z.-z. Xing, and H. Zhang, Phys. Lett. B 679, 242 (2009b), arXiv:0905.2889 [hep-ph] .
  * Hettmansperger  _et al._ [2011] H. Hettmansperger, M. Lindner, and W. Rodejohann, JHEP 04, 123 (2011), arXiv:1102.3432 [hep-ph] .
  * Escrihuela  _et al._ [2015] F. J. Escrihuela, D. V. Forero, O. G. Miranda, M. Tortola, and J. W. F. Valle, Phys. Rev. D 92, 053009 (2015), [Erratum: Phys.Rev.D 93, 119905 (2016)], arXiv:1503.08879 [hep-ph] .
  * Escrihuela  _et al._ [2017] F. J. Escrihuela, D. V. Forero, O. G. Miranda, M. Tórtola, and J. W. F. Valle, New J. Phys. 19, 093005 (2017), arXiv:1612.07377 [hep-ph] .
  * Forero  _et al._ [2021] D. V. Forero, C. Giunti, C. A. Ternes, and M. Tortola, Phys. Rev. D 104, 075030 (2021), arXiv:2103.01998 [hep-ph] .
  * Aker  _et al._ [2022] M. Aker _et al._ (KATRIN), Nature Phys. 18, 160 (2022), arXiv:2105.08533 [hep-ex] .
  * Agostini  _et al._ [2022] M. Agostini, G. Benato, J. A. Detwiler, J. Menéndez, and F. Vissani, (2022), arXiv:2202.01787 [hep-ex] .
  * Aghanim  _et al._ [2020] N. Aghanim _et al._ (Planck), Astron. Astrophys. 641, A6 (2020), [Erratum: Astron.Astrophys. 652, C4 (2021)], arXiv:1807.06209 [astro-ph.CO] .
  * Workman  _et al._ [2022] R. L. Workman _et al._ (Particle Data Group), PTEP 2022, 083C01 (2022).
  * Gariazzo  _et al._ [2016] S. Gariazzo, C. Giunti, M. Laveder, Y. F. Li, and E. M. Zavanin, J. Phys. G 43, 033001 (2016), arXiv:1507.08204 [hep-ph] .
  * Gonzalez-Garcia  _et al._ [2016] M. C. Gonzalez-Garcia, M. Maltoni, and T. Schwetz, Nucl. Phys. B 908, 199 (2016), arXiv:1512.06856 [hep-ph] .
  * Giunti and Lasserre [2019] C. Giunti and T. Lasserre, Ann. Rev. Nucl. Part. Sci. 69, 163 (2019), arXiv:1901.08330 [hep-ph] .
  * Diaz  _et al._ [2020] A. Diaz, C. A. Argüelles, G. H. Collin, J. M. Conrad, and M. H. Shaevitz, Phys. Rept. 884, 1 (2020), arXiv:1906.00045 [hep-ex] .
  * Böser  _et al._ [2020] S. Böser, C. Buck, C. Giunti, J. Lesgourgues, L. Ludhova, S. Mertens, A. Schukraft, and M. Wurm, Prog. Part. Nucl. Phys. 111, 103736 (2020), arXiv:1906.01739 [hep-ex] .
  * Dasgupta and Kopp [2021] B. Dasgupta and J. Kopp, Phys. Rept. 928, 1 (2021), arXiv:2106.05913 [hep-ph] .
  * Acero  _et al._ [2022b] M. A. Acero _et al._ , (2022b), arXiv:2203.07323 [hep-ex] .
  * Klop and Palazzo [2015] N. Klop and A. Palazzo, Phys. Rev. D 91, 073017 (2015), arXiv:1412.7524 [hep-ph] .
  * Berryman  _et al._ [2015] J. M. Berryman, A. de Gouvêa, K. J. Kelly, and A. Kobach, Phys. Rev. D 92, 073012 (2015), arXiv:1507.03986 [hep-ph] .
  * Gandhi  _et al._ [2015] R. Gandhi, B. Kayser, M. Masud, and S. Prakash, JHEP 11, 039 (2015), arXiv:1508.06275 [hep-ph] .
  * Palazzo [2016] A. Palazzo, Phys. Lett. B 757, 142 (2016), arXiv:1509.03148 [hep-ph] .
  * Dutta  _et al._ [2016] D. Dutta, R. Gandhi, B. Kayser, M. Masud, and S. Prakash, JHEP 11, 122 (2016), arXiv:1607.02152 [hep-ph] .
  * Capozzi  _et al._ [2017] F. Capozzi, C. Giunti, M. Laveder, and A. Palazzo, Phys. Rev. D 95, 033006 (2017), arXiv:1612.07764 [hep-ph] .
  * Fiza  _et al._ [2021] N. Fiza, M. Masud, and M. Mitra, JHEP 09, 162 (2021), arXiv:2102.05063 [hep-ph] .
  * Giarnetti and Meloni [2021] A. Giarnetti and D. Meloni, Universe 7, 240 (2021), arXiv:2106.00030 [hep-ph] .
  * Giunti  _et al._ [2022a] C. Giunti, Y. F. Li, C. A. Ternes, O. Tyagi, and Z. Xin, JHEP 10, 164 (2022a), arXiv:2209.00916 [hep-ph] .
  * Anselmann  _et al._ [1995] P. Anselmann _et al._ (GALLEX), Phys. Lett. B342, 440 (1995).
  * Hampel  _et al._ [1998] W. Hampel _et al._ (GALLEX), Phys. Lett. B420, 114 (1998).
  * Kaether  _et al._ [2010] F. Kaether, W. Hampel, G. Heusser, J. Kiko, and T. Kirsten, Phys. Lett. B 685, 47 (2010), arXiv:1001.2731 [hep-ex] .
  * Abdurashitov  _et al._ [1996] J. N. Abdurashitov _et al._ (SAGE), Phys. Rev. Lett. 77, 4708 (1996).
  * Abdurashitov  _et al._ [1999] J. N. Abdurashitov _et al._ (SAGE), Phys. Rev. C59, 2246 (1999), hep-ph/9803418 .
  * Abdurashitov  _et al._ [2006] J. N. Abdurashitov _et al._ (SAGE), Phys. Rev. C73, 045805 (2006), nucl-ex/0512041 .
  * Abdurashitov  _et al._ [2009] J. N. Abdurashitov _et al._ (SAGE), Phys. Rev. C 80, 015807 (2009), arXiv:0901.2200 [nucl-ex] .
  * Barinov  _et al._ [2022a] V. V. Barinov _et al._ , Phys. Rev. Lett. 128, 232501 (2022a), arXiv:2109.11482 [nucl-ex] .
  * Barinov  _et al._ [2022b] V. V. Barinov _et al._ , Phys. Rev. C 105, 065502 (2022b), arXiv:2201.07364 [nucl-ex] .
  * Bahcall [1997] J. N. Bahcall, Phys. Rev. C56, 3391 (1997), hep-ph/9710491 .
  * Berryman  _et al._ [2022a] J. M. Berryman, P. Coloma, P. Huber, T. Schwetz, and A. Zhou, JHEP 02, 055 (2022a), arXiv:2111.12530 [hep-ph] .
  * Giunti  _et al._ [2022b] C. Giunti, Y. F. Li, C. A. Ternes, and Z. Xin, (2022b), arXiv:2212.09722 [hep-ph] .
  * Serebrov  _et al._ [2021] A. Serebrov _et al._ , Phys.Rev.D 104, 032003 (2021), arXiv:2005.05301 [hep-ex] .
  * Danilov [2019] M. Danilov, J.Phys.Conf.Ser. 1390, 012049 (2019), arXiv:1812.04085 [hep-ex] .
  * Andriamirado  _et al._ [2020] M. Andriamirado _et al._ (PROSPECT, STEREO), (2020), arXiv:2006.13147 [hep-ex] .
  * Danilov and Skrobova [2020] M. V. Danilov and N. A. Skrobova, JETP Lett. 112, 452 (2020).
  * Giunti  _et al._ [2021] C. Giunti, Y. F. Li, C. A. Ternes, and Y. Y. Zhang, Phys. Lett. B 816, 136214 (2021), arXiv:2101.06785 [hep-ph] .
  * Giunti  _et al._ [2022c] C. Giunti, Y. F. Li, C. A. Ternes, and Z. Xin, Phys. Lett. B 829, 137054 (2022c), arXiv:2110.06820 [hep-ph] .
  * Aartsen  _et al._ [2020] M. G. Aartsen _et al._ (IceCube), Phys. Rev. Lett. 125, 141801 (2020), arXiv:2005.12942 [hep-ex] .
  * Denton  _et al._ [2022] P. B. Denton, A. Giarnetti, and D. Meloni, (2022), arXiv:2210.00109 [hep-ph] .
  * Manczak  _et al._ [2021] J. Manczak _et al._ (KM3NeT), PoS ICRC2021, 1165 (2021).
  * Coloma  _et al._ [2021] P. Coloma, J. López-Pavón, S. Rosauro-Alcaraz, and S. Urrea, JHEP 08, 065 (2021), arXiv:2105.11466 [hep-ph] .
  * Soumya [2022] C. Soumya, Phys. Rev. D 105, 015012 (2022), arXiv:2104.04315 [hep-ph] .
  * Agarwalla  _et al._ [2022] S. K. Agarwalla, S. Das, A. Giarnetti, and D. Meloni, JHEP 07, 121 (2022), arXiv:2111.00329 [hep-ph] .
  * Miranda  _et al._ [2020] O. G. Miranda, D. K. Papoulias, O. Sanders, M. Tórtola, and J. W. F. Valle, Phys. Rev. D 102, 113014 (2020), arXiv:2008.02759 [hep-ph] .
  * Gariazzo  _et al._ [2022] S. Gariazzo, P. Martínez-Miravé, O. Mena, S. Pastor, and M. Tórtola, (2022), arXiv:2211.10522 [hep-ph] .
  * Abusleme  _et al._ [2020] A. Abusleme _et al._ (JUNO), (2020), arXiv:2005.08745 [physics.ins-det] .
  * Berryman  _et al._ [2022b] J. M. Berryman, L. A. Delgadillo, and P. Huber, Phys. Rev. D 105, 035002 (2022b), arXiv:2104.00005 [hep-ph] .
  * Basto-Gonzalez  _et al._ [2022] V. S. Basto-Gonzalez, D. V. Forero, C. Giunti, A. A. Quiroga, and C. A. Ternes, Phys. Rev. D 105, 075023 (2022), arXiv:2112.00379 [hep-ph] .
  * Aiello  _et al._ [2021] S. Aiello _et al._ (KM3NeT), JHEP 10, 180 (2021), arXiv:2107.00344 [hep-ex] .
  * Machado  _et al._ [2019] P. A. Machado, O. Palamara, and D. W. Schmitz, Ann. Rev. Nucl. Part. Sci. 69, 363 (2019), arXiv:1903.04608 [hep-ex] .


$\displaystyle\sqsubseteq\overline{F}\alpha_{i}\odot c$
$\displaystyle(\text{by inductive hypothesis and that $\overline{F}$ is
monotone)})$ $\displaystyle=\alpha_{i+1}$ $\displaystyle(\text{by
definition})\,.$

Hence $\beta_{i}\sqsubseteq\alpha_{i}$ holds for each $i\in\omega$. This
implies $J\gamma_{i}\odot g\sqsubseteq J\gamma_{i}\odot l$ for each
$i\in\omega$. As
$(Z,(J\gamma_{i}:Z\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}F^{i}1)_{i\in\omega})$
is a 2-limit (Assumption 5), we have $g\sqsubseteq l$. Hence $l$ is the
largest homomorphism from $c$ to $J\zeta$.

$\textstyle{1}$$\textstyle{\overline{F}1}$$\textstyle{\overline{F}^{2}1}$$\textstyle{\overline{F}^{3}1}$$\textstyle{X}$$\textstyle{\overline{F}X}$$\textstyle{\overline{F}^{2}X}$$\textstyle{\overline{F}^{3}X}$$\textstyle{Z}$$\textstyle{\overline{F}Z}$$\textstyle{\overline{F}^{2}Z}$$\textstyle{\overline{F}^{3}Z}$$\textstyle{Z}$$\textstyle{\overline{F}Z}$$\textstyle{\overline{F}^{2}Z}$$\textstyle{\overline{F}^{3}Z}$$\textstyle{=}$$\textstyle{=}$$\textstyle{=}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\scriptstyle{J!_{F1}}$$\scriptstyle{JF!_{F1}}$$\scriptstyle{JF^{2}!_{F1}}$$\scriptstyle{JF^{2}!_{F1}}$$\scriptstyle{c}$$\scriptstyle{\overline{F}c}$$\scriptstyle{\overline{F}c}$$\scriptstyle{\overline{F}c}$$\scriptstyle{\alpha_{0}}$$\scriptstyle{\overline{F}\alpha_{0}}$$\scriptstyle{\overline{F}^{2}\alpha_{0}}$$\scriptstyle{\overline{F}^{3}\alpha_{0}}$$\scriptstyle{J\zeta}$$\scriptstyle{JF\zeta}$$\scriptstyle{JF^{2}\zeta}$$\scriptstyle{JF^{3}\zeta}$$\scriptstyle{J\zeta}$$\scriptstyle{JF\zeta}$$\scriptstyle{JF^{2}\zeta}$$\scriptstyle{J!_{Z}}$$\scriptstyle{JF!_{Z}}$$\scriptstyle{JF^{2}!_{Z}}$$\scriptstyle{JF^{3}!_{Z}}$$\scriptstyle{J!_{Z}}$$\scriptstyle{JF!_{Z}}$$\scriptstyle{JF^{2}!_{Z}}$$\scriptstyle{JF^{3}!_{Z}}$$\scriptstyle{g}$$\scriptstyle{\overline{F}g}$$\scriptstyle{\overline{F}^{2}g}$$\scriptstyle{\overline{F}^{3}g}$$\scriptstyle{l}$$\scriptstyle{g}$

∎

######  Lemma A.0.

A polynomial functor $F$ and $\mathcal{G}$ on $\mathbf{Meas}$ satisfy
Assumptions 1, 2, 3, 4, and 5 in Prop. 5.1.

######  Proof.

It is known that Assumption 1 is satisfied [24].

It is also known that there exists distributive law
$\lambda:F\mathcal{G}\Rightarrow\mathcal{G}F$ exists [6]. Therefore Assumption
2 is satisfied.

Next, we prove that Assumption 3 is satisfied. Assume that a family of Kleisli
arrows
$(f_{i}:(X,\mathfrak{F}_{X})\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}(Y,\mathfrak{F}_{Y}))_{i\in\omega}$
constitute a decreasing sequence. We can define their greatest lower bound
$\bigsqcap_{i\in\omega}f_{i}:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}Y$
in a pointwise manner: namely, for $x\in X$ and $A\in\mathfrak{F}_{Y}$,

$(\bigsqcap_{i\in\omega}f_{i})(x)(A)=\lim_{i\to\infty}(f_{i}(x)(A))\,.$

It is easy to see that polynomial $F$ preserves this pointwise greatest lower
bound. It remains to prove that $\bigsqcap_{i\in\omega}f_{i}$ is a measurable
function from $(X,\mathfrak{F}_{X})$ to $\mathcal{G}(Y,\mathfrak{F}_{Y})$.
Moreover, we also have to prove the local continuity of composition. They can
be proved in the similar manner to the proof of [5, Proposition 9]. Therefore
Assumption 3 is satisfied.

It is easy to see that Assumption 4 is satisfied.

We prove that Assumption 5 is satisfied. If $F1$ is empty, then the limit $Z$
is also empty and Assumption 5 is satisfied. Assume that $F1$ is not empty. It
is known that the sub-Giry monad $\mathcal{G}$ preserves a limit over an
$\omega^{\text{op}}$-sequence consisting of standard Borel spaces and
surjective measurable functions [24]. In our setting, for each $i\in\omega$,
$F^{i}1$ is a standard Borel space because $1$ and all of $\Sigma_{n}$ are
standard Borel spaces, and moreover, standard Borel space is preserved by
countable coproducts and countable limits [18, 12.B]. Moreover, for each
$i\in\omega$, $F^{i}!_{F1}$ is surjective. Therefore the limit
$(Z,(\gamma_{i}:Z\to F^{i}1)_{i\in\omega})$ over the final sequence
$1\overset{!_{F1}}{\leftarrow}F1\overset{F!_{F1}}{\leftarrow}F^{2}1\overset{F^{2}!_{F1}}{\leftarrow}\ldots$
is preserved by $\mathcal{G}$. This immediately implies that
$J:\mathbf{Meas}\to\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{G})$ preserves the
limit. It is easy to see that the resulting limit is a $2$-limit. ∎

######  Proof of Thm. 5.2.1.

In the similar manner to the proof of Lem. A.4, we can show that $F$ and
$\mathcal{G}$ satisfy the assumptions in Lem. 4.2.1. Therefore immediate from
Lem. 4.2.1. ∎

######  Proof of Lem. 5.2.2.

We prove ${\sf tr^{\infty}}(c)\sqsubseteq{\sf tr^{\infty}}(d)\odot b$ along
the construction of ${\sf tr^{\infty}}(c)$ and ${\sf tr^{\infty}}(d)$ in the
proof of Prop. 5.1.

For each $i\in\omega$, we define
$\Psi^{i}_{X}(J!_{X}):X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}1$
and
$\Psi^{i}_{Y}(J!_{Y}):Y\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}1$
as in the proof of Prop. 5.1. We can prove that
$\Psi^{i}_{X}(J!_{X})\sqsubseteq\Psi^{i}_{Y}(J!_{Y})\odot b$ for all
$i\in\omega$ by the induction on $i$ as follows.

For $i=0$, by Assumption 1, we have
$\Psi^{0}_{X}(J!_{X})=\Psi^{0}_{Y}(J!_{Y})\odot b$.

Let $i>0$ and assume that
$\Psi^{i-1}_{X}(J!_{X})\sqsubseteq\Psi^{i-1}_{Y}(J!_{Y})\odot b$. Then

$\displaystyle\Psi^{i}_{X}(J!_{X})$
$\displaystyle=J!_{F1}\odot\overline{F}(\Psi^{i-1}_{X}(J!_{X}))\odot d$
$\displaystyle(\text{by definition of $\Psi_{X}$ })$ $\displaystyle\sqsubseteq
J!_{F1}\odot\overline{F}(\Psi^{i-1}_{Y}(J!_{Y}))\odot\overline{F}b\odot c$
$\displaystyle(\text{by induction hypothesis})$ $\displaystyle\sqsubseteq
J!_{F1}\odot\overline{F}(\Psi^{i-1}_{Y}(J!_{Y}))\odot d\odot b$
$\displaystyle(\text{$b$ is a bwd.\ simulation})$
$\displaystyle=\Psi^{i}_{Y}(J!_{Y})\odot b$ $\displaystyle(\text{by definition
of $\Psi_{Y}$})\,.$

Therefore we have $\Psi^{i}_{X}(J!_{X})\sqsubseteq\Psi^{i}_{Y}(J!_{Y})\odot b$
for all $i\in\omega$.

$\textstyle{1}$$\textstyle{\overline{F}1}$$\textstyle{\overline{F}^{2}1}$$\textstyle{\overline{F}^{3}1}$$\textstyle{Y}$$\textstyle{\overline{F}Y}$$\textstyle{\overline{F}^{2}Y}$$\textstyle{\overline{F}^{3}Y}$$\textstyle{X}$$\textstyle{\overline{F}X}$$\textstyle{\overline{F}^{2}X}$$\textstyle{\overline{F}^{3}X}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{=}$$\textstyle{{\scriptstyle=}}$$\textstyle{{\scriptstyle=}}$$\textstyle{{\scriptstyle=}}$$\textstyle{Z}$$\textstyle{\overline{F}Z}$$\textstyle{\overline{F}^{2}Z}$$\textstyle{\overline{F}^{3}Z}$$\textstyle{=}$$\textstyle{=}$$\textstyle{=}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\scriptstyle{J!_{F1}}$$\scriptstyle{JF!_{F1}}$$\scriptstyle{JF^{2}!_{F1}}$$\scriptstyle{JF^{2}!_{F1}}$$\scriptstyle{d}$$\scriptstyle{\overline{F}d}$$\scriptstyle{\overline{F}^{2}d}$$\scriptstyle{\overline{F}^{3}d}$$\scriptstyle{c}$$\scriptstyle{\overline{F}c}$$\scriptstyle{\overline{F}^{2}c}$$\scriptstyle{\overline{F}^{3}c}$$\scriptstyle{J!_{Y}}$$\scriptstyle{JF!_{Y}}$$\scriptstyle{JF^{2}!_{Y}}$$\scriptstyle{JF^{3}!_{Y}}$$\scriptstyle{b}$$\scriptstyle{\overline{F}b}$$\scriptstyle{\overline{F}^{2}b}$$\scriptstyle{\overline{F}^{3}b}$$\scriptstyle{J!_{X}}$$\scriptstyle{JF!_{X}}$$\scriptstyle{JF^{2}!_{X}}$$\scriptstyle{JF^{3}!_{X}}$$\scriptstyle{J\zeta}$$\scriptstyle{JF\zeta}$$\scriptstyle{JF^{2}\zeta}$$\scriptstyle{JF^{3}\zeta}$$\scriptstyle{J!_{Z}}$$\scriptstyle{JF!_{Z}}$$\scriptstyle{JF^{2}!_{Z}}$$\scriptstyle{JF^{3}!_{Z}}$

We define cones
$(X,(\alpha^{X}_{i}:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
and
$(Y,(\alpha^{Y}_{i}:Y\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
over the sequence
$1\overset{J!_{F1}}{\mathrel{\mspace{-4.0mu}\leftarrow\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}}\overline{F}1\overset{JF!_{F1}}{\mathrel{\mspace{-4.0mu}\leftarrow\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}}\overline{F}^{2}1\overset{JF^{2}!_{F1}}{\mathrel{\mspace{-4.0mu}\leftarrow\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}}\ldots$
as equation (7) in the proof of Prop. 5.1.

As is shown in the proof of Prop. 5.1, ${\sf
tr^{\infty}}(c):X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}Z$
is the unique mediating arrow from a cone
$(X,(\alpha^{X}_{i}:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
to a 2-limit
$(Z,(J\gamma_{i}:Z\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$.
Moreover, ${\sf
tr^{\infty}}(d):Y\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}Z$
is the unique mediating arrow from a cone
$(Y,(\alpha^{Y}_{i}:Y\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
to
$(Z,(J\gamma_{i}:Z\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
and therefore ${\sf tr^{\infty}}(d)\odot
b:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}Z$
is the unique mediating arrow from a cone $(X,(\alpha^{Y}_{i}\odot
b:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
to
$(Z,(J\gamma_{i}:Z\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$.

For all $i\in\omega$, we can prove
$\alpha^{X}_{i}\sqsubseteq\alpha^{Y}_{i}\odot b$ by the induction on $i$ as
follows:

For $i=0$,

$\displaystyle\alpha^{X}_{0}$
$\displaystyle=\bigsqcap_{i\in\omega}\Psi^{i}_{X}(J!_{X})$
$\displaystyle(\text{by definition})$
$\displaystyle\sqsubseteq\bigsqcap_{i\in\omega}(\Psi^{i}_{Y}(J!_{Y})\odot b)$
$\displaystyle(\text{by the above result})$
$\displaystyle=\bigl{(}\bigsqcap_{i\in\omega}\Psi^{i}_{Y}(J!_{Y})\bigr{)}\odot
b$ $\displaystyle(\text{by Assumption\leavevmode\nobreak\
\ref{asm:existenceWeaklyFinalCoalgGFPcont} in Prop.\leavevmode\nobreak\
\ref{prop:generalconstructionnotop}})$ $\displaystyle=\alpha^{Y}_{0}\odot b$
$\displaystyle(\text{by definition})\,.$

Let $i>0$ and assume that $\alpha^{X}_{i-1}\sqsubseteq\alpha^{Y}_{i-1}\odot
b$. Then

$\displaystyle\alpha^{X}_{i}$ $\displaystyle=\overline{F}\alpha^{X}_{i-1}\odot
c$ $\displaystyle(\text{by definition})$
$\displaystyle\sqsubseteq\overline{F}\alpha^{Y}_{i-1}\odot\overline{F}b\odot
c$ $\displaystyle(\text{by inductive hypothesis and the monotonicity of
$\overline{F}$})$ $\displaystyle\sqsubseteq\overline{F}\alpha^{Y}_{i-1}\odot
d\odot b$ $\displaystyle(\text{$b$ is a backward simulation})$
$\displaystyle=\alpha^{Y}_{i}\odot b$ $\displaystyle(\text{by definition}).$

Therefore we have $\alpha^{X}_{i}\sqsubseteq\alpha^{Y}_{i}\odot b$ for all
$i\in\omega$. As
$(Z,(J\gamma_{i}:Z\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1)_{i\in\omega})$
is a 2-limit, this implies ${\sf tr^{\infty}}(c)\sqsubseteq{\sf
tr^{\infty}}(d)\odot b$.

The last claim follows from $b$’s condition on initial states.

$\textstyle{1}$$\textstyle{\overline{F}1}$$\textstyle{\overline{F}^{2}1}$$\textstyle{\overline{F}^{3}1}$$\textstyle{Y}$$\textstyle{\overline{F}Y}$$\textstyle{\overline{F}^{2}Y}$$\textstyle{\overline{F}^{3}Y}$$\textstyle{X}$$\textstyle{\overline{F}X}$$\textstyle{\overline{F}^{2}X}$$\textstyle{\overline{F}^{3}X}$$\textstyle{=}$$\textstyle{=}$$\textstyle{=}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsupseteq}$$\textstyle{\sqsubseteq}$$\textstyle{{\scriptstyle\sqsubseteq}}$$\textstyle{{\scriptstyle\sqsubseteq}}$$\textstyle{{\scriptstyle\sqsubseteq}}$$\textstyle{{\scriptstyle\sqsubseteq}}$$\textstyle{Z}$$\textstyle{\overline{F}Z}$$\textstyle{\overline{F}^{2}Z}$$\textstyle{\overline{F}^{3}Z}$$\textstyle{=}$$\textstyle{=}$$\textstyle{=}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\scriptstyle{J!_{F1}}$$\scriptstyle{JF!_{F1}}$$\scriptstyle{JF^{2}!_{F1}}$$\scriptstyle{JF^{2}!_{F1}}$$\scriptstyle{d}$$\scriptstyle{\overline{F}d}$$\scriptstyle{\overline{F}^{2}d}$$\scriptstyle{\overline{F}^{3}d}$$\scriptstyle{c}$$\scriptstyle{\overline{F}c}$$\scriptstyle{\overline{F}^{2}c}$$\scriptstyle{\overline{F}^{3}c}$$\scriptstyle{\alpha^{Y}_{0}}$$\scriptstyle{\overline{F}\alpha^{Y}_{0}}$$\scriptstyle{\overline{F}^{2}\alpha^{Y}_{0}}$$\scriptstyle{\overline{F}^{3}\alpha^{Y}_{0}}$$\scriptstyle{b}$$\scriptstyle{\overline{F}b}$$\scriptstyle{\overline{F}^{2}b}$$\scriptstyle{\overline{F}^{3}b}$$\scriptstyle{\alpha^{X}_{0}}$$\scriptstyle{\overline{F}\alpha^{X}_{0}}$$\scriptstyle{\overline{F}^{2}\alpha^{X}_{0}}$$\scriptstyle{\overline{F}^{3}\alpha^{X}_{0}}$$\scriptstyle{J\zeta}$$\scriptstyle{JF\zeta}$$\scriptstyle{JF^{2}\zeta}$$\scriptstyle{JF^{3}\zeta}$$\scriptstyle{J!_{Z}}$$\scriptstyle{JF!_{Z}}$$\scriptstyle{JF^{2}!_{Z}}$$\scriptstyle{JF^{3}!_{Z}}$$\scriptstyle{{\sf
tr^{\infty}}(c)}$$\scriptstyle{{\sf tr^{\infty}}(d)}$

∎

######  Lemma A.0.

In Def. 5.2.2, if $T=\mathcal{G}$ and $F$ is a polynomial functor, Assumption
1 is satisfied if $b(x)(Y)=1$ for each $x\in X$.

######  Proof.

We assume that $b(x)(Y)=1$ for each $x\in X$. By the definition of
multiplication of the sub-Giry monad (see Def. 2), for $x\in X$,

$J!_{Y}\odot
b(x)(1)=b(x)\bigl{(}!_{Y}^{-1}(1)\bigr{)}=b(x)(Y)=1=J!_{X}(x)(1)\,.$

Therefore Assumption 1 is satisfied. ∎

###  A.5. Lift Monad and a Tree Automaton with Exception

####  A.5.1. Definitions

In this section, we give a definition of the lift monad and the order on the
homsets of the Kleisli category.

######  Definition A.0 (lift monad).

A _lift monad_ is a monad $(\mathcal{L},\eta^{\mathcal{L}},\mu^{\mathcal{L}})$
on $\mathbf{Sets}$ such that

  * •

$\mathcal{L}X=\\{\bot\\}+X$,

  * •

$\mathcal{L}f(y)=\begin{cases}f(y)&(y\neq\bot)\\\
\bot&(\text{otherwise}),\end{cases}$

  * •

$\eta^{\mathcal{L}}_{X}(x)=x$, and

  * •

$\mu^{\mathcal{L}}_{X}(z)=z$.

######  Definition A.0 (order enrichment of
$\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{L})$).

We define an order on $\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{L})(X,Y)$ by
$f\sqsubseteq g\;\overset{\text{def}}{\Leftrightarrow}\;\forall x\in
X.\,f(x)=\bot\,\text{or}\,f(x)=g(x)$.

####  A.5.2. Construction of Infinite Traces

In this section, we show that a polynomial functor $F$ on $\mathbf{Sets}$ and
the lift monad $\mathcal{L}$ satisfy the assumptions in Prop. 5.1, hence
constitute an infinite trace situation.

######  Proposition A.0.

A polynomial functor $F$ on $\mathbf{Sets}$ and a lift monad $\mathcal{L}$
satisfy Assumptions 1, 2, 3, 4, and 5 in Prop. 5.1 with respect to the order
in Def. A.5.1. Therefore, $F$ and $\mathcal{L}$ constitute an infinite trace
situation. ∎

######  Proof.

It is easy to see that $F$ and $\mathcal{L}$ on $\mathbf{Sets}$ satisfy the
Assumptions 1 and 4.

To prove that Assumption 3 is satisfied, it suffices to prove that for each
$x\in X$, $\bigsqcap_{i\in\omega}(g_{i}\odot b)(x)=\bot$ iff
$(\bigsqcap_{i\in\omega}g_{i})\odot b(x)=\bot$. If $b(x)=\bot$, then
$\bigsqcap_{i\in\omega}(g_{i}\odot b)(x)=(\bigsqcap_{i\in\omega}g_{i})\odot
b(x)=\bot$. Assume $b(x)\neq\bot$. Then

$\bigsqcap_{i\in\omega}(g_{i}\odot b)(x)=\bot\Leftrightarrow\exists
i\in\omega.\,g_{i}(b(x))=\bot\Leftrightarrow\bigsqcap_{i\in\omega}g_{i}(b(x))=\bot\Leftrightarrow(\bigsqcap_{i\in\omega}g_{i}\odot
b)(x)=\bot\,.$

It is known that Assumption 2 is satisfied [16, Lemma 2.4].

As a connected limit and a coproduct commute in $\mathbf{Sets}$ [1], the
Kleisli inclusion functor
$J:\mathbf{Sets}\to\mathcal{K}\mspace{-1.0mu}\ell(T)$ preserves
$\omega$-limit. It is easy to see that this limit is a 2-limit. Therefore
Assumption 5 is also satisfied. ∎

####  A.5.3. Coalgebraic Infinite Trace Semantics and Automata-theoretic
Semantics of Tree Automata with Exception

Next we characterize the coalgebraic infinite trace semantics using automata-
theoretic terms. For a ranked alphabet $\Sigma$,
$(\mathcal{L},F_{\Sigma})$-system can be regarded as a automaton with
exception that generates an infinite tree.

######  Definition A.0.

A $(\mathcal{L},F_{\Sigma})$-system $\mathcal{X}=(X,s,c)$ is called a _tree
automaton with exception_. For a $\Sigma$-labeled infinite tree $t=(D,l)$ and
a state $x\in X$, a $(X)_{n\in\omega}$-labeled infinite tree $t_{r}=(D,l_{r})$
that has the same domain as $t$ is called a _run of $\mathcal{X}$ from $x$
that generates $t$_ if

  * •

$l_{r}(\varepsilon)=x$, and

  * •

for each $\alpha\in D$ where $l(\alpha)=a\in\Sigma_{n}$, $l_{r}(\alpha)=y$ and
$l_{r}(\alpha i)=y_{i}$ for each $0\leq i\leq n-1$, we have
$c(y)=(a,y_{0},\ldots,y_{n-1})\neq\bot$.

For a state $x\in X$, an infinite tree $t$ is called an _infinite output of
$\mathcal{X}$ from $x$_ and denoted by $\text{Out}(\mathcal{X},x)$ if there
exists a run of $\mathcal{X}$ from $x$ that generates $t$.

An infinite tree $t$ is called an _infinite output of $\mathcal{X}$_ and
denoted by $\text{Out}(\mathcal{X})$ if $s(*)\neq\bot$ and $t$ is an output of
$\mathcal{X}$ from $s(*)$.

The notations $\text{Out}(\mathcal{X},x)$ and $\text{Out}(\mathcal{X})$ in the
above definition are justified by the following lemma. It is easy to prove, so
we omit the proof.

######  Lemma A.0.

Let $\mathcal{X}=(X,s,c)$ be a tree automaton with exception. For a state
$x\in X$, if an infinite output of $\mathcal{X}$ from $x$ exists, then it is
unique. Moreover, an infinite output of $\mathcal{X}$ exists, then it is
unique. ∎

We show that for a tree automaton $\mathcal{X}=(X,s,c)$ with exception, the
infinite output of $\mathcal{X}$ is the largest homomorphism from $c$ to
$J\zeta$.

######  Theorem A.0.

Let $\mathcal{X}=(X,s,c)$ be a tree automaton with exception.

With respect to the order in Def. A.5.1, for each $x\in X$, we have

${\sf tr^{\infty}}(c)(x)=\begin{cases}\text{Out}(\mathcal{X},x)&(\text{an
infinite output of $\mathcal{A}$ from $x$ exists})\\\
\bot&(\text{otherwise}).\end{cases}$

Moreover,

${\sf tr^{\infty}}(c)\odot s(*)=\begin{cases}\text{Out}(\mathcal{X})&(\text{an
infinite output of $\mathcal{A}$ exists})\\\
\bot&(\text{otherwise}).\end{cases}$

######  Proof.

We define
$h:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\text{Tree}_{\infty}(\Sigma)$
by

$h(x)=\begin{cases}\text{Out}(\mathcal{X},x)&(\text{an infinite output of
$\mathcal{A}$ from $x$ exists})\\\ \bot&(\text{otherwise}).\end{cases}$

We show that $h$ is the largest homomorphism from $c$ to $J\zeta$ where
$\zeta$ is a $F_{\Sigma}$-coalgebra defined in the proof of Thm. A.2.2.

We first show that $h$ is a homomorphism. Assume that $h(x)=t=(D,l)\neq\bot$.
Then there exists a run $t_{r}=(D,l_{r})$ of $\mathcal{X}$ from $x$ that
generates $t$. By definition, we have $c(x)=c(l_{r}(\varepsilon))\neq\bot$.
Hence we define $n\in\omega$, $a\in\Sigma_{n}$ and $x_{0},\ldots,x_{n-1}\in X$
by $(a,x_{0},\ldots,x_{n-1})=c(x)$. As $t_{r}=(D,l_{r})$ is a run of
$\mathcal{X}$ from $x$ that generates $t$, $i$’th subtree $t_{r,i}$ of $t_{r}$
is a run of $\mathcal{X}$ from $x_{i}$ that generates $i$’th subtree $t_{i}$
of $t$. Therefore $h(x_{i})=t_{i}\neq\bot$ for each $i\in\\{0,\ldots,n-1\\}$.
Then

$\overline{F}h\odot
c(x)=\overline{F}h(a,x_{0},\ldots,x_{n-1})=(a,t_{0},\ldots,t_{n-1})=J(\zeta)(t)=J(\zeta)\odot
h(x).$

Assume that $h(x)=\bot$. If $c(x)=\bot$, $\overline{F}h\odot c(x)=J\zeta\odot
h(x)=\bot$ holds by definition. Assume that
$c(x)=(a,x_{0},\ldots,x_{n-1})\neq\bot$ where $a\in\Sigma_{n}$. If
$h(x_{i})=t_{i}\neq\bot$ for all $i\in\\{0,\ldots,n-1\\}$, there exits a run
$t_{r,i}$ of $\mathcal{X}$ from $x_{i}$ that generates $t_{i}$ for each $i$.
Then a tree $(x,t_{r,0},\ldots,t_{r,n-1})$ is a run of $\mathcal{X}$ from $x$
that generates $t$, and it contradicts to $h(x)=\bot$. Therefore there exists
$i$ such that $h(x_{i})=\bot$ and we have $\overline{F}h\odot c(x)=J\zeta\odot
h(x)=\bot$.

Hence $h$ is a homomorphism from $c$ to $J\zeta$. It remains to prove that $h$
is the largest homomorphism. Let
$g:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\text{Tree}_{\infty}(\Sigma)$
be a homomorphism from $c$ to $J\zeta$. It suffices to prove that
$g(x)=t=(D,l)\neq\bot$, then $h(x)=t$, too. To this end, we construct a run
$t_{r}=(D,l_{r})$ of $\mathcal{X}$ from $x$ that generates $t$. For each
$\alpha\in D$, we define $l_{r}(\alpha)\in X$ such that
$g(l_{r}(\alpha))\neq\bot$ by the induction on the length of $\alpha$ as
follows.

For $\alpha=\varepsilon$, we define it by $l_{r}(\varepsilon)=x$. By
assumption, $g(l_{r}(\varepsilon))=g(x)\neq\bot$.

Assume that $l(\alpha)\in\Sigma_{n}$ and $g(l(\alpha))\neq\bot$. As $g$ is a
homomorphism from $c$ to $J\zeta$ and $g(l(\alpha))\neq\bot$, there exists
$x_{0},\ldots,x_{n-1}$ such that
$c(l_{r}(\alpha))=(l(\beta),x_{0},\ldots,x_{n-1})$ and $g(x_{i})\neq\bot$ for
each $i$. We define $l_{r}(\alpha i)$ by $l_{r}(\alpha i)=x_{i}$.

By axiom of dependent choice, this $l_{r}$ is well-defined and moreover, by
its construction, $(D,l_{r})$ is a run of $\mathcal{X}$ from $x$ that
generates $t$. Therefore $t\in L(\mathcal{X},x)$ for each $x\in X$ and we have
$g\sqsubseteq L(\mathcal{X},\underline{\phantom{n}}\,)$.

Hence ${\sf tr^{\infty}}(c)=L(\mathcal{X},\underline{\phantom{n}}\,)$. This
immediately implies ${\sf tr^{\infty}}(c)\odot s(*)=L(\mathcal{X})$. ∎

####  A.5.4. Kleisli Simulation for Systems with Exception

It is known that a polynomial $F$ and $\mathcal{L}$ satisfy assumptions of
Lem. 4.2.1 [14]. Hence we can use forward Kleisli simulation to check infinite
trace inclusion between tree automata with exception.

For a $(\mathcal{L},F)$-system, as we have seen in Prop. A.5.2, the largest
homomorphism can be constructed using Prop. 5.1. Therefore from Lem. 5.2.2, we
can use T-backward simulation in Def. 5.2.2 to check infinite trace inclusion.
For a $(\mathcal{L},F)$-system, the sufficient condition for a backward
simulation $b$ to satisfy the assumption in Def. 5.2.2 can be given as
follows.

######  Proposition A.0.

In Def. 5.2.2, if $T=\mathcal{L}$ and $F$ is a polynomial functor, then
Assumption 1 is satisfied if $b(x)\neq\bot$ for each $x\in X$.

######  Proof.

Let $*$ be the unique element in the final object $1$. It suffices to prove
that $J!_{Y}\odot b(x)=*$ for all $x\in X$. By the assumption, $b(x)\neq\bot$.
Therefore $*=!_{Y}(b(x))=J!_{Y}\odot b(x)$. ∎

####  A.5.5. Forward Partial Execution for Systems with Exception

From Thm. 4.3, soundness and adequacy of FPE for forward simulation hold.

By the construction of the largest homomorphism, soundness and adequacy of FPE
for backward simulation hold if the simulating automaton satisfies the
assumptions in Thm. 5.3. For a $(\mathcal{L},F)$-system, the assumptions can
be described as follows.

######  Proposition A.0.

If $T=\mathcal{L}$ and $F$ is a polynomial functor, the assumption in Thm. 5.3
is satisfied if $d(y)\neq\bot$ for each $y\in Y$. ∎

###  A.6. Subdistribution Monad and Infinite Trace Situation

We first give definitions of the subdistribution monad and orders on the
homsets of the Kleisli category.

######  Definition A.0 (subdistribution monad).

A _subdistribution monad_ is a monad
$(\mathcal{D},\eta^{\mathcal{D}},\mu^{\mathcal{D}})$ on $\mathbf{Sets}$ such
that

  * •

$\mathcal{D}X=\\{p:X\to[0,1]\mid\sum_{x\in X}p(x)\leq 1\\}$,

  * •

$\mathcal{D}f(p)(y)=\sum_{x\in f^{-1}(y)}p(x)$,

  * •

$\eta^{\mathcal{D}}_{X}(x)(y)=\begin{cases}1&(y=x)\\\
0&(\text{otherwise}),\end{cases}$ and

  * •

$\mu^{\mathcal{D}}_{X}(\Phi)(x)=\sum_{p\in\mathcal{D}X}\Phi(p)\cdot p(x)$.

######  Definition A.0 (order enrichment of
$\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{D})$).

We define an order on $\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{D})(X,Y)$ by
$f\sqsubseteq g\;\Leftrightarrow\;\forall x\in X.\,\forall y\in
Y.\,f(x)(y)\leq g(x)(y)$.

For a ranked alphabet $\Sigma$, we show that $F_{\Sigma}$ on $\mathbf{Sets}$
and the subdistribution monad $\mathcal{D}$ constitute an infinite trace
situation by giving an explicit definition of the largest homomorphism.

######  Proposition A.0.

Let $\Sigma$ be a ranked alphabet and $F_{\Sigma}$ be a functor on
$\mathbf{Sets}$ defined in Def. A.1. Then $F_{\Sigma}$ and the subdistribution
monad $\mathcal{D}$ constitute an infinite trace situation.

######  Proof.

We define $\zeta:\text{Tree}_{\infty}(\Sigma)\to
F_{\Sigma}\text{Tree}_{\infty}(\Sigma)$ in $\mathbf{Sets}$ in the same way as
the proof of Thm. A.2.2 Then $\zeta$ is a final $F_{\Sigma}$-coalgebra. For
each $\overline{F_{\Sigma}}$-coalgebra
$c:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F_{\Sigma}}X$,
we construct the largest homomorphism
$h:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F_{\Sigma}}\text{Tree}_{\infty}(\Sigma)$
from $c$ to $J\zeta$.

For each $x\in X$, an integer $k\in\omega$ and a $k$-prefix tree
$t^{k}\in\text{Tree}_{\infty}^{k}(\Sigma)$, we define a value
$\xi_{x}(t^{k})\in[0,1]$ by the induction on $k$ as follows:

  * •

if $k=0$, then $\xi_{x}(t^{k})=1$, and

  * •

if $t^{k}=(D^{k},l^{k})\in\text{Tree}_{\infty}^{k}(\Sigma)$ such that
$l^{k}(\varepsilon)=a\in\Sigma_{n}$ and the $i$’th subtree of $t^{k}$ is
$t^{k}_{i}$,

$\xi_{x}(t^{k})=\sum_{x_{0},\ldots,x_{n-1}\in
X}\bigl{(}c(x)(a,x_{0},\ldots,x_{n-1})\cdot\prod_{i=0}^{n-1}\xi_{x_{i}}(t^{k}_{i})\bigr{)}\,.$
(8)

For $t^{\prime}\in\text{Tree}_{\infty}(\Sigma)$ and $k\in\omega$, we denote
${}_{k}(t^{\prime})=(_{k}(D^{\prime}),_{k}(l^{\prime}))$ for a unique
$k$-prefix tree that is a prefix of $t^{\prime}$. As
$\sum_{n\in\omega}\sum_{a\in\Sigma_{n}}\sum_{x_{0},\ldots,x_{n-1}\in
X}c(x)(a,x_{0},\ldots,x_{n-1})\leq 1$, the sequence
$\bigl{(}\xi_{x}(_{k}(t))\bigr{)}_{k\in\omega}$ is decreasing with respect to
$k$. Therefore we define
$h:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F_{\Sigma}}\text{Tree}_{\infty}(\Sigma)$
by $h(x)(t)=\lim_{k\to\infty}\xi_{x}(_{k}(t))$.

We first show that this $h$ is a homomorphism. For each $x\in X$,
$n\in\omega$, and $t=(D,l)\in\text{Tree}_{\infty}(\Sigma)$ such that
$l(\varepsilon)=a\in\Sigma_{n}$ and $i$’th subtree of $t$ is $t_{i}$,

$\displaystyle J\zeta^{-1}\odot\overline{F_{\Sigma}}h\odot
c(x)(a,t_{0},\ldots,t_{n-1})$ $\displaystyle=\sum_{x_{0},\ldots,x_{n-1}\in
X}c(x)(a,x_{0},\ldots,x_{n-1})\cdot\prod_{i=0}^{n-1}h(x_{i})(t_{i})$
$\displaystyle(\text{by definition})$
$\displaystyle=\sum_{x_{0},\ldots,x_{n-1}\in
X}c(x)(a,x_{0},\ldots,x_{n-1})\cdot\prod_{i=0}^{n-1}\lim_{k\to\infty}\xi_{x_{i}}(_{k}(t_{i}))$
$\displaystyle(\text{by definition of $h$})$
$\displaystyle=\lim_{k\to\infty}\sum_{x_{0},\ldots,x_{n-1}\in
X}c(x)(a,x_{0},\ldots,x_{n-1})\cdot\prod_{i=0}^{n-1}\xi_{x_{i}}(_{k}(t_{i}))$
$\displaystyle=\lim_{k\to\infty}\xi_{x}(t)$ $\displaystyle(\text{by definition
of $\xi$})$ $\displaystyle=h(x)(t)$ $\displaystyle(\text{by definition of
$h$})\,.$

To conclude the proof, we show that $h$ is the largest homomorphism. Let
$g:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\text{Tree}_{\infty}(\Sigma)$
be a homomorphism from $c$ to $J\zeta$. We prove $g(x)(t)\leq h(x)(t)$ for all
$x\in X$ and $t\in\text{Tree}_{\infty}(\Sigma)$. To this end, we first prove
$g(x)(t)\leq\xi_{x}(_{k}(t))$ for all $k\in\omega$, $x\in X$ and
$t\in\text{Tree}_{\infty}(\Sigma)$, by the induction on $k$.

If $k=0$ then for all $x$ and $t$, $g(x)(t)\leq 1=\xi_{x}(_{k}(t))$.

Let $k>0$ and assume that $g(x)(t)\leq\xi_{x}(_{k-1}(t))$ for all $x$ and $t$.
Then

$\displaystyle g(x)(t)$
$\displaystyle=J\zeta^{-1}\odot\overline{F_{\Sigma}}g\odot c(x)(t)$
$\displaystyle(\text{$g$ is a homomorphism})$
$\displaystyle=\sum_{x_{0},\ldots,x_{n-1}\in
X}c(x)(a,x_{0},\ldots,x_{n-1})\cdot\prod_{i=0}^{n-1}g(x_{i})(t_{i})$
$\displaystyle(\text{by definition})$
$\displaystyle\leq\sum_{x_{0},\ldots,x_{n-1}\in
X}c(x)(a,x_{0},\ldots,x_{n-1})\cdot\prod_{i=0}^{n-1}\xi_{x_{i}}(_{k-1}(t_{i}))$
$\displaystyle(\text{by induction hypothesis})$ $\displaystyle=\xi_{x}(t)$
$\displaystyle(\text{by definition of $\xi$})$

Hence for all $x$ and $t$, we have
$g(x)(t)\leq\lim_{k\to\infty}\xi_{x}(_{k}(t))=h(x)(t)$. ∎

We have shown that $F_{\Sigma}$ and $\mathcal{D}$ constitute an infinite trace
situation. However, the largest homomorphism to $J\zeta$ cannot be constructed
in the general ways introduced in this paper.

It is easy to see that there exists $X$ and $Z$ in $\mathbf{Sets}$ such that
$\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{D})(X,Z)$ does not have $\top_{X,Z}$.
Therefore we cannot construct the largest homomorphism by using Prop. 4.1.

$\textstyle{\mathcal{X}}$$\textstyle{\circ}$$\scriptstyle{p,\frac{1}{2}}$$\scriptstyle{q,\frac{1}{2}}$

Moreover, in fact, we cannot construct the largest homomorphism even by using
Prop. 5.1. Let $F$ be an endofunctor on $\mathbf{Sets}$ that is defined by
$F(\underline{\phantom{n}}\,)=\\{p,q\\}\times(\underline{\phantom{n}}\,)$.
Then, the limit of the final sequence
$1\overset{!_{F1}}{\leftarrow}F1\overset{F!_{F1}}{\leftarrow}F^{2}1\overset{F^{2}!_{F1}}{\leftarrow}\ldots$
is given by $(Z,(\gamma_{i}:Z\to F^{i}1)_{i\in\omega})$ where
$Z=\\{p,q\\}^{\omega}$ and $\gamma_{i}(a_{0}a_{1}\ldots)=a_{0}a_{1}\ldots
a_{i-1}$. We define $X\in\mathcal{K}\mspace{-1.0mu}\ell(\mathcal{D})$ and
$c:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}X$
by $X=\\{*\\}$ and $c(*)(a,*)=\frac{1}{2}$ where $a\in\\{p,q\\}$. Moreover,
for each $i\in\omega$, we inductively define
$\alpha_{i}:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}\overline{F}^{i}1$
by $\alpha_{0}=J!_{X}$ and $\alpha_{i+1}=\overline{F}\alpha_{i}\odot c$. It is
easy to see that $(X,(\alpha_{i})_{i\in\omega})$ is a cone over a sequence
$1\overset{J!_{F1}}{\mathrel{\mspace{-4.0mu}\leftarrow\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}}\overline{F}1\overset{JF!_{F1}}{\mathrel{\mspace{-4.0mu}\leftarrow\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}}\overline{F}^{2}1\overset{JF^{2}!_{F1}}{\mathrel{\mspace{-4.0mu}\leftarrow\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}}\ldots$.
However, it is also easy to see that there does not exist
$f:X\mathrel{\mspace{-4.0mu}\to\mspace{-16.0mu}\raisebox{0.43057pt}[0.0pt][0.0pt]{$\shortmid$}\mspace{6.0mu}}Z$
such that $J\gamma_{i}\odot f=\alpha_{i}$. This means that Assumption 5 is not
satisfied.

As a consequence, we can construct the largest homomorphism from $c$ to
$J\zeta$ neither by using the construction in Prop. 4.1 nor Prop. 5.1.

###  A.7. Examples and Counterexamples

######  Example A.0.

In the construction of the largest homomorphism in Prop. 4.1, we need
$\omega+1$ times of iterations for the nondeterministic automaton
$\mathcal{X}$ on the left below. We need $2\omega+1$ times of iterations for
$\mathcal{Y}$ on the right below. In a similar manner, for each ordinal
$\mathfrak{a}$, we can construct an automaton for which we need $\mathfrak{a}$
times of iteration.

$\textstyle{\mathcal{X}}$$\textstyle{\checkmark}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\cdots}$$\textstyle{\dots}$$\textstyle{\circ}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$

$\textstyle{\mathcal{Y}}$$\textstyle{\checkmark}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\cdots}$$\textstyle{\cdots}$$\textstyle{\circ}$$\textstyle{\dots}$$\textstyle{\dots}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$

######  Example A.0.

There exists a (not total) backward simulation from the nondeterministic
automaton $\mathcal{X}$ to $\mathcal{Y}$ below. However, the simulated
automaton $\mathcal{X}$ outputs an infinite word $aaa\ldots$ while
$\mathcal{Y}$ does not. Therefore the infinite trace of $\mathcal{X}$ is not
include in that of $\mathcal{Y}$.

$\textstyle{\mathcal{X}}$$\textstyle{\checkmark}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$

$\textstyle{\mathcal{Y}}$$\textstyle{\checkmark}$$\textstyle{\circ}$$\textstyle{\circ}$$\scriptstyle{a}$

There exists a (not image-finite) backward simulation from $\mathcal{Z}$ to
$\mathcal{W}$ below, while trace inclusion from $\mathcal{Z}$ to $\mathcal{W}$
does not hold.

$\textstyle{\mathcal{Z}}$$\textstyle{\checkmark}$$\textstyle{\circ}$$\textstyle{\circ}$$\scriptstyle{a}$$\scriptstyle{a}$

$\textstyle{\mathcal{W}}$$\textstyle{\checkmark}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\dots}$$\textstyle{\cdots}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{a}$

######  Example A.0.

The infinite trace of the nondeterministic automata $\mathcal{X}$ below is
included in the infinite trace of $\mathcal{Y}$. There exists no forward
simulation from $\mathcal{X}$ to $\mathcal{Y}$ but a TIF-backward simulation
does exist.

$\textstyle{\mathcal{X}}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{c}$$\scriptstyle{d}$

$\textstyle{\mathcal{Y}}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\textstyle{\circ}$$\scriptstyle{a}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{c}$$\scriptstyle{d}$