# Monte Carlo Top Quark Mass Calibration

Bahman Dehnadi,a André H. Hoang,bc Vicent Mateu,de b and Iain W. Stewartf
aUniversität Siegen, Department Physik, Walter-Flex-Straße 3, D-57068 Siegen,
Germany
bUniversity of Vienna, Faculty of Physics, Boltzmanngasse 5, A-1090 Wien,
Austria
cErwin Schrödinger International Institute for Mathematical Physics,
University of Vienna,
Boltzmanngasse 9, A-1090 Wien, Austria
dDepartamento de Física Fundamental and IUFFyM, Universidad de Salamanca,
E-37008 Salamanca, Spain
eInstituto de Física Teórica UAM-CSIC, E-28049 Madrid, Spain
fCenter for Theoretical Physics, Massachusetts Institute of Technology,
Cambridge, MA 02139, USA
E-mail

###### Abstract:

The most precise top quark mass measurements use kinematic reconstruction
methods, determining the top mass parameter of a Monte Carlo event generator,
$m_{t}^{\rm MC}$. Due to the complicated interplay of hadronization and parton
shower dynamics in Monte Carlo event generators relevant for kinematic
reconstruction, relating $m_{t}^{\rm MC}$ to field theory masses is a non-
trivial task. In this talk we report on a calibration procedure to determine
this relation using hadron level QCD predictions for 2-Jettiness in
$e^{+}e^{-}$ annihilation, an observable which has kinematic top mass
sensitivity and a close relation to the invariant mass of the particles coming
from the top decay. The theoretical ingredients of the QCD prediction are
reviewed. Fitting $e^{+}e^{-}$ 2-Jettiness calculations at NLL/NNLL order to
Pythia 8.205, we find that $m_{t}^{\rm MC}$ agrees with the MSR mass
$m_{t,1\,{\rm GeV}}^{\rm MSR}$ within uncertainties. At NNLL we find
$m_{t}^{\rm MC}=m_{t,1\,{\rm GeV}}^{\rm MSR}+(0.18\pm 0.22)\,{\rm GeV}$.
$m_{t}^{\rm MC}$ can differ from the pole mass $m_{t}^{\rm pole}$ by up to
$600\,{\rm MeV}$, and using the pole mass generally leads to larger
uncertainties. At NNLL we find $m_{t}^{\rm MC}=m_{t}^{\rm pole}+(0.57\pm
0.28)\,{\rm GeV}$ as the fit result. In contrast, converting $m_{t,1\,{\rm
GeV}}^{\rm MSR}$ obtained at NNLL to the pole mass gives a result for
$m_{t}^{\rm pole}$ that is substantially larger and incompatible with the fit
result. We also explain some theoretical aspects relevant for employing the
C-parameter as an alternative calibration observable.
SI-HEP-2018-10, IFT-UAM/CSIC-18-024, MIT-CTP/4990, UWTHPH 2018-11

##  1  Introduction

The most precise measurements of the top quark mass are based on direct
reconstruction methods exploiting its kinematic properties and have reached
uncertainties of about $0.5$ GeV [1, 2, 3]. They are based on multivariate
fits that use a maximum amount of information from the top decay final states.
This includes template and matrix element fits for distributions such as the
measured invariant mass. Since these observables are highly differential and
depend on experimental cuts and details of the jet dynamics, multipurpose
Monte Carlo (MC) event generators are employed in these analyses, and the
measured mass is the top mass parameter $m_{t}^{\rm MC}$ contained in the
particular MC event generator. Clearly, the interpretation of $m_{t}^{\rm MC}$
from the field theoretic point of view is influenced by the interplay of both
perturbative and non-perturbative QCD effects and – because MC generators
provide only approximate descriptions – may also depend in part on the MC
tuning and the set of observables used in the analyses. In the direct
reconstruction analyses referred to above the systematic uncertainties from MC
modeling are a dominant part of the uncertainty budget, but they do not
address in any way how $m_{t}^{\rm MC}$ is related to a mass parameter defined
precisely in quantum field theory that can be globally used for higher order
theoretical predictions. The relation is nontrivial because it requires an
understanding of the interplay between the partonic components of the MC
generator (hard matrix elements and parton shower) and the hadronization
model. Furthermore it may be affected by common basic approximations made in
the construction of the MC machinery. One can also say that – at the level of
precision achieved for top mass measurements in direct reconstruction – MC
generators should be considered as models whose partonic components and
hadronization models are, through the tuning procedure, capable of describing
experimental data to a precision that is higher than that of their partonic
input.

In the past $m_{t}^{\rm MC}$ has frequently simply been identified with the
pole mass, which is, however not defined beyond perturbation theory. This
identification may not immediately look incompatible with parton-shower
implementations for massive quarks, but a direct identification is disfavored
because the parton-shower does not account for perturbative corrections from
momenta below the MC shower cutoff $\Lambda_{c}\sim 1\,{\rm GeV}$ and as a
consequence, $m_{t}^{\rm MC}$ may be also sensitive to non-perturbative
effects from momenta below $\Lambda_{c}$. Also, the pole mass has an ${\cal
O}(\Lambda_{\rm QCD})$ renormalon ambiguity, while $m_{t}^{\rm MC}$ does not,
since information from perturbative QCD is not employed below $\Lambda_{c}$.
It has been argued [4, 5] that $m_{t}^{\rm MC}$ has a much closer (and
perturbatively more stable) relation to the MSR mass [6] $m_{t}^{\rm
MSR}(R\approx\Lambda_{c})$, where the scale $R$ defining this scheme is close
to $\Lambda_{c}$.

For a given MC generator (which in this context also implies that one
considers a given tune), $m_{t}^{\rm MC}$ can be calibrated with respect to a
field theory mass scheme through a fit of MC predictions to hadron level QCD
computations for observables closely related to the distributions that enter
the experimental reconstruction analyses. In Ref. [7] a precise quantitative
study was provided on the interpretation of $m_{t}^{\rm MC}$ in terms of the
MSR and pole mass schemes based on a hadron level prediction for the
2-Jettiness variable $\tau_{2}$ [8] for the production of a boosted top-
antitop quark pair in $e^{+}e^{-}$ annihilation. To be definite $\tau_{2}$ is
defined as:

$\tau_{2}=1-\max_{{\vec{n}}_{t}}\frac{\sum_{i}|{\vec{n}}_{t}\cdot\vec{p}_{i}|}{Q}\,,$
(1)

where the sum is over the 3-momenta of all final state particles, the maximum
defines the thrust axis $\vec{n}_{\rm t}$ and $Q$ is the center of mass
energy. In Refs. [9, 10] a factorization theorem has been proven for boosted
top quarks, yielding hadron level predictions for $\tau_{2}$. The $\tau_{2}$
distribution has a distinguished peak very sensitive to the top mass, and is a
delta function at $\tau_{2}^{\rm min}(m_{t})=1\,-\,\sqrt{1-4m_{t}^{2}/Q^{2}}$
at tree level. For $Q$ sufficiently larger than $m_{t}$ the peak region is
dominated by dijet events where the top quarks decay inside narrow back-to-
back cones, and there $\tau_{2}$ is directly related to the sum of the squared
invariant masses $M^{2}_{a,b}$ in the two hemispheres defined by the thrust
axis $\vec{n}_{t}$, $(\tau_{2})_{\rm peak}\approx(M_{a}^{2}+M_{b}^{2})/Q^{2}$
[9, 10]. Therefore $\tau_{2}$ in the peak region is an observable with direct
kinematic top mass sensitivity, just like those that enter the top quark mass
reconstruction methods, and the results of the calibration study should
provide information relevant for the interpretation of the direct
reconstruction measurements.

##  2  2-Jettiness Distribution

The $\tau_{2}$ distribution in the peak region for boosted top quarks has the
basic form

$\frac{\rm d\sigma}{\rm d\tau_{2}}\\!=\\!\\!\int\\!\rm
dk\,\bigg{(}\\!\frac{\rm d\hat{\sigma}_{\rm s}}{\rm d\tau_{2}}+\frac{\rm
d\hat{\sigma}_{\rm ns}}{\rm
d\tau_{2}}\\!\bigg{)}\\!\\!\bigg{(}\\!\tau_{2}-\frac{k}{Q}\\!\bigg{)}F_{\\!\tau_{2}}\\!(k)\\!\bigg{[}1+{\cal
O}\bigg{(}\\!\frac{\Lambda_{\rm
QCD}}{Q},\frac{\Gamma_{t}}{m_{t}}\\!\bigg{)}\bigg{]},$ (2)

where $\rm d\hat{\sigma}_{\rm s}/\rm d\tau_{2}$ contains the singular partonic
QCD corrections $\alpha_{s}^{j}\,[\,\ln^{k}(\tau_{2}-\tau_{2}^{\rm
min})/(\tau_{2}\,-\,\tau_{2}^{\rm min})\,]_{+}$ and
$\alpha_{s}^{j}\,\delta(\tau_{2}\,-\,\tau_{2}^{\rm min})$ in the dijet limit
and $\rm d\hat{\sigma}_{\rm ns}/\rm d\tau_{2}$ stands for the remaining
partonic nonsingular QCD corrections. The shape function $F_{\tau_{2}}$
describes non-perturbative effects from wide-angle soft gluon radiation [11].
The singular partonic contribution obeys the factorization theorem

$\displaystyle\frac{\rm d\hat{\sigma}_{\rm s}}{\rm
d\tau_{2}}=\;Q\,H_{Q}^{(6)}(Q,\mu_{Q})\,U_{H_{Q}}^{(6)}(Q,\mu_{Q},\mu_{m})\,H_{m}^{(6)}(Q,m_{t},\mu_{m})\,U_{H_{m}}^{(5)}\Big{(}\frac{Q}{m_{t}},\mu_{m},\mu_{B}\Big{)}$
(3) $\displaystyle\times\\!{\int}{\rm ds}{\int}{\rm
dk}\,J_{B,\tau_{2}}^{(5)}\Big{(}\frac{s}{m_{t}},\mu_{B},\Gamma_{t},\delta
m_{t}\Big{)}\,U_{S}^{(5)}(k,\mu_{B},\mu_{S})\,\hat{S}_{\tau_{2}}^{(5)}\Big{(}Q[\tau_{2}-\tau_{2}^{\rm
min}(m_{t})]-\frac{s}{Q}-k,\mu_{S}\Big{)},$

which is based on Soft-Collinear-Effective Theory [12, 13, 14, 15] and
separates the contributions from the hard interactions in the hard functions
$H_{Q}$ and $H_{m}$, the jet function $J_{B,\tau_{2}}$, and the soft cross-
talk between the top and antitop jets in the partonic soft function
$\hat{S}_{\tau}$. The jet function $J_{B,\tau_{2}}$ is derived in boosted HQET
[9] since the collinear top jet invariant mass in the peak region is very
close to the nominal top quark mass. It includes the collinear dynamics of the
decaying top quarks and leading top finite-width effects. The various
evolution factors $U_{X}$ sum large logarithms.

Results for $\rm d\hat{\sigma}_{s}/\rm d\tau_{2}$ with next-to-leading
logarithmic resummation $+\,{\cal O}(\alpha_{s})$ singular corrections (NLL +
NLO) can be found in Ref. [10], with the addition of the virtual top quark
contribution and rapidity logarithms in $H_{m}$ and the corresponding
evolution factor $U_{H_{m}}$ both from Ref. [16]. The N2LL evolution in
$U_{H_{Q}}$ and $U_{S}$ is known from the massless quark case, and is
consistent with the direct ${\cal O}(\alpha_{s}^{2})$ calculation of the
$J_{B,\tau_{2}}$ anomalous dimension [17]. We implemented all the N2LL order
ingredients for the proper treatment of the flavor number dependence
[superscript (6) for including top as dynamic quark versus superscript (5) for
excluding the top] in the RG evolution [18, 19]. We also include the ${\cal
O}(\alpha_{s})$ nonsingular corrections $\rm d\hat{\sigma}_{\rm ns}/\rm
d\tau_{2}$ [20].

For the shape function $F_{\tau_{2}}$ we use the convergent basis functions
introduced in Ref. [21] truncated to $4$ elements (where the 4-th element is
already numerically irrelevant), which determine the moments of the shape
function $\Omega_{i}$ [22, 23]. The leading power correction $\Omega_{1}$ is
defined in the R-gap scheme such that it cancels an $\mathcal{O}(\Lambda_{\rm
QCD})$ renormalon present in $\hat{S}_{\tau_{2}}$ [24]. This renders
$\Omega_{1}$ dependent on the subtraction scale $R_{S}$, and we quote results
for $\Omega_{1}$ at the reference scales $R_{S}=2$ GeV. Equation (3) is
written in terms of a generic mass scheme $m_{t}$, with $\delta
m_{t}=m_{t}^{\rm pole}-m_{t}$ in $J_{B,\tau_{2}}^{(5)}$ controlling the
dominant sensitivity to the mass scheme. In the pole mass scheme $\delta
m_{t}=0$. Using renormalon-free schemes, the $\overline{\rm MS}$ mass with
$\delta m_{t}\propto m_{t}$ is appropriate for the hard functions. In the jet
function $J_{B,\tau_{2}}^{(5)}$ one has to adopt a scheme such as MSR [6] with
$\delta m_{t}\sim R\sim\Gamma_{t}$ to avoid upsetting the power counting in
the peak region. The evolution of the MSR mass with $R$ and of $\Omega_{1}$
with $R_{S}$ is described by R-evolution [6, 25]. To sum large logarithms we
use $\tau_{2}$-dependent scales $\mu_{i}(\tau_{2})$ and $R_{i}(\tau_{2})$,
which can be expressed in terms of $9$ parameters. These parameters are varied
to estimate perturbative uncertainties.

For a given center of mass energy $Q$, the key parameters that enter the QCD
factorization predictions for the $\tau_{2}$ distribution are the top mass
$m_{t}$, the top width $\Gamma_{t}$, the hadronic parameters $\Omega_{i}$, and
the strong coupling $\alpha_{s}(m_{Z})$. We will consider fits both in the
pole and the MSR mass schemes. The results in the MSR scheme are quoted in
terms of $m_{t}^{\rm MSR}(1\,\mbox{GeV})$ following [4, 5].

##  3  Fit Procedure

For a given $m_{t}^{\rm MC}$ we produce MC datasets for $\rm d\sigma/\rm
d\tau_{2}$ in the peak region for various $Q$ values. For a given profile and
value of $\alpha_{s}(m_{Z})$ we fit the parameters $m_{t}$ and $\Omega_{i}$ of
the hadron level QCD predictions to this MC dataset. For each $Q$ value the
distribution is normalized over the fit range, and multiple $Q$s are needed
simultaneously to break degeneracies concerning $m_{t}$ and the soft function
moments $\Omega_{i}$. We construct the $\chi^{2}$-function using the
statistical uncertainties in the MC datasets. We do the fit by first, for a
given value of $m_{t}$, minimizing $\chi^{2}$ with respect to the $\Omega_{i}$
parameters. The resulting marginalized $\chi^{2}$ is then minimized with
respect to $m_{t}$ used in the QCD predictions. Uncertainties obtained for the
QCD parameters from this $\chi^{2}$ simply reflect the MC statistical
uncertainties used to construct the $\chi^{2}$. To estimate the perturbative
uncertainty in the QCD predictions we take $500$ random points in the profile-
function parameter space and perform a fit for each of them. The $500$ sets of
best-fit values provide an ensemble from which we remove the upper and lower
$1.5\%$ in the mass values to eliminate potential numerical outliers. From
this we then determine central values by averaging the largest and smallest
values and perturbative uncertainties from half the covered interval.

To illustrate the calibration procedure we use Pythia 8.205 [26, 27] with the
$e^{+}e^{-}$ default tune 7 (the Monash 2013 tune [28] for which
$\Lambda_{c}=0.5$ GeV) for top mass parameter values $m_{t}^{\rm MC}=170$,
$171$, $172$, $173$, $174$ and $175$ GeV. We use a fixed top quark width
$\Gamma_{t}=1.4\,{\rm GeV}$ which is independent of $m_{t}^{\rm MC}$. No other
changes are made to the default settings. To minimize statistical
uncertainties we generate each distribution with $10^{7}$ events. We have
carried out fits for the following seven Q sets (in GeV units):
$(600,1000,1400)$, $(700,1000,1400)$, $(800,1000,1400)$, $(600$ – $900)$,
$(600$ – $1400)$, $(700$ – $1000)$ and $(700$ – $1400)$, where the ranges
refer to steps of $100$. For each one of these sets we have considered three
ranges of $\tau_{2}$ in the peak region: $(60\%,80\%)$, $(70\%,80\%)$ and
$(80\%,80\%)$, where $(x\%,y\%)$ means that we include regions of the spectra
whose $\tau_{2}<\tau_{2}^{\rm peak}$ having cross-section values larger than
$x\%$ of the peak height, and $\tau_{2}>\tau_{2}^{\rm peak}$ with cross
sections larger than $y\%$ of the peak height, where $\tau_{2}^{\rm peak}$ is
the peak position. This makes a total of $21$ fit settings each of which gives
central values and scale uncertainties for the top mass and the $\Omega_{i}$.

Figure 1:  Distribution of best-fit mass values from the scan over parameters
describing perturbative uncertainties. Results are shown for cross sections
employing the MSR mass $m_{t}^{\rm MSR}(1\,{\rm GeV})$ (left) and the pole
mass $m_{t}^{\rm pole}$ (right), both at N2LL and NLL. The Pythia datasets use
$m_{t}^{\rm MC}=173$ GeV as an input.

##  4  Numerical Results of the Calibration

To visualize the stability of our fits we display in Fig. 1 the distribution
of best-fit mass values obtained for 500 random profile functions for
$m_{t}^{\rm MC}=173$ GeV based on the $Q$ set $(600-1400)$ and the bin range
$(60\%,80\%)$. Results are shown for $m_{t}^{\rm MSR}(1\,\mbox{GeV})$ and
$m_{t}^{\rm pole}$ at NLL and N2LL order, exhibiting good convergence, with
the higher order results having a smaller perturbative scale uncertainty. The
results for $m_{t}^{\rm MSR}(1\,\mbox{GeV})$ are stable and about $200$ MeV
below $m_{t}^{\rm MC}$ confirming the close relation of $m_{t}^{\rm
MSR}(1\,\mbox{GeV})$ and $m_{t}^{\rm MC}$ suggested in Refs. [4, 5]. We
observe that $m_{t}^{\rm pole}$ is about $1.1$ GeV (NLL) and $0.7$ GeV (N2LL)
lower than $m_{t}^{\rm MC}$, demonstrating that corrections here are bigger,
and that the MC mass cannot simply be identified with the pole mass. The
results from the fits to the 21 different Q sets and bin ranges mentioned
above are quite similar. Their differences can be interpreted as a
quantification of the level of incompatibility between the MC event generator
results and the QCD predictions. Unlike the perturbative uncertainties they
need not necessarily to decrease when going from NLL to N2LL due to intrinsic
limitations of the MC generator. We therefore use the differences from the 21
fits to assign an additional incompatibility uncertainty between QCD and the
MC generator for the calibration which one may interpret as an estimate for
the intrinsic MC uncertainty.

To quote final results we used the following procedure: (1) Take the average
of the highest and lowest central values from the 21 sets as the final central
value of our calibration. (2) Take the average of the scale uncertainties of
these sets as our final estimate for the perturbative uncertainty. (3) Take
the half of the difference of the largest and smallest central values from the
sets as the incompatibility uncertainty between QCD and the MC. (4)
Quadratically add the perturbative, and incompatibility errors to obtain a
final uncertainty.

Using $\alpha_{s}$ values within the uncertainty of the world average
$\alpha_{s}(m_{Z})=0.1181(13)$ gives an additional parametric uncertainty of
$\simeq 20$ MeV for $m_{t}^{\rm MSR}(1\,\mbox{GeV})$ and $m_{t}^{\rm pole}$ at
N2LL order. This is an order of magnitude smaller than the other uncertainties
and we therefore neglect it. Table 1 shows our final results for the MSR mass
$m_{t}^{\rm MSR}(1\,\mbox{GeV})$ and $m_{t}^{\rm pole}$ at NLL and N2LL order,
utilizing the $m_{t}^{\rm MC}=173$ GeV dataset. For $m_{t}^{\rm
MSR}(1\,\mbox{GeV})$ we observe a reduction of perturbative uncertainties from
$260$ MeV at NLL to $190$ MeV at N2LL. The corresponding incompatibility
uncertainties are $140$ and $110$ MeV. The corresponding fit results for the
first shape function moment are $\Omega_{1}^{\rm PY}=0.42\pm 0.07\pm 0.03$ GeV
at N2LL and $\Omega_{1}^{\rm PY}=0.41\pm 0.07\pm 0.02$ GeV at NLL order with
the first uncertainty coming from scale variation and second from
incompatibility. The result agrees nicely with the expectation that
$\Omega_{1}\sim\Lambda_{\rm QCD}$.

Using the pole mass scheme in our theory prediction and repeating the
calibration fit we find that there is a significant difference to $m_{t}^{\rm
MC}$, and we observe that the central value shifts by $330$ MeV between NLL
and N2LL order, see Tab. 1. There is a reduction of perturbative uncertainties
like in the MSR scheme, however the incompatibility uncertainty increases at
N2LL order. Interestingly, while we observe that $m_{t}^{\rm pole}<m_{t,1\,\rm
GeV}^{MSR}$ for our fit result in the pole mass scheme, one obtains
$m_{t}^{\rm pole}>m_{t,1\,\rm GeV}^{MSR}$ when converting our MSR mass result
to the pole mass. At NLO the corresponding correction reads $m_{t}^{\rm
pole}=m_{t,1\,\rm GeV}^{MSR}+0.17\,{\rm GeV}+\mathcal{O}(\alpha_{s}^{2})$.
This observation may not be unexpected, since the pole mass often leads to
poorer convergence of perturbative series due to the pole mass renormalon
problem. This indicates that the uncertainty in the relation between
$m_{t}^{\rm MC}$ and $m_{t}^{\rm pole}$ is actually larger than indicated by
the pole mass results in Tab. 1 by themselves.

$m_{t}^{\rm MC}=173$ GeV ($\tau_{2}^{e^{+}e^{-}}$)
---
mass | order | central | perturb. | incompatibility |  total
$m_{t,1\,\rm GeV}^{\rm MSR}$ | NLL | $172.80$ | $0.26$ | $0.14$ | $0.29$
$m_{t,1\,\rm GeV}^{\rm MSR}$ | N2LL | $172.82$ | $0.19$ | $0.11$ | $0.22$
$m_{t}^{\rm pole}$ | NLL | $172.10$ | $0.34$ | $0.16$ | $0.38$
$m_{t}^{\rm pole}$ | N2LL | $172.43$ | $0.18$ | $0.22$ | $0.28$
Table 1:  Results of the calibration for $m_{t}^{\rm MC}=173$ GeV in Pythia,
combining results from all Q sets and bin ranges. Shown are central values,
perturbative and incompatibility uncertainties, and the total uncertainty, all
in GeV. The results shown for the pole mass $m_{t}^{\rm pole}$ are not final
as explained in the text.

We have carried out the calibration procedure for $m_{t}^{\rm MC}$ values
between $170$ and $175$ GeV in steps of $1$ GeV, and the outcome of our fits
showed a behavior consistent with the results given in Tab. 1. In future
studies such calibration results should be independently determined for
different MC event generators and also for generator settings (such as
different tunes). In the case of the MSR mass it is clear that the results
from Tab. 1 are well behaved perturbatively and we therefore expect that
higher order results will lie within the given uncertainties. This means that
for the setup described before a MC top quark mass value of $m_{t}^{\rm
MC}=173$ GeV (as a representative example) can be associated with the MSR mass
value of $m_{t,1\,\rm GeV}^{\rm MSR}=172.82\pm 0.22$ GeV. Overall we find that

$m_{t}^{\rm MC}=m_{t,1\,{\rm GeV}}^{\rm MSR}+(0.18\pm 0.22)\,{\rm GeV}\,,$ (4)

for MC top quark masses between $172$ and $174\,{\rm GeV}$. So $m_{t}^{\rm
MC}$ and $m_{t,1\,{\rm GeV}}^{\rm MSR}$ may be identified to within about
$200\,{\rm MeV}$.

To give a definite result including a reliable uncertainty estimate for the
relation of $m_{t}^{\rm MC}$ and the top quark pole mass (that accounts for
the observations discussed above) we adopt the following strategy at NNLL: (1)
We use the perturbative MSR-pole mass relation at NLO quoted above and take
the average between the direct pole mass calibration result from Tab. 1
(lowest line) and the converted result (using the MSR mass result as input)
for the final pole mass central value. (2) For the uncertainty we take the
quadratic sum of the direct determination uncertainty shown in Tab. 1 (lowest
line) and half of the difference with respect to the MSR converted result
(which amounts to $0.28\,{\rm GeV}$ at NNLL).

Applying this procedure we find that for the above described setup a MC top
quark mass value of $m_{t}^{\rm MC}=173$ GeV can be associated with the pole
mass value of $m_{t}^{\rm pole,\rm N^{2}LL}=172.71\pm 0.40$ GeV. To obtain the
relation of $m_{t}^{\rm MC}$ and $m_{t}^{\rm pole}$ at NLL order we proceed in
the analogous way by using the direct calibration result for the pole mass in
Tab. 1 (second-to-lowest line) and the tree-level relation $m_{t}^{\rm
pole}=m_{t,1\,\rm GeV}^{\rm MSR}$. Here, half of the difference of the two
resulting values for $m_{t}^{\rm pole}$ amounts to $0.35$ GeV. For $m_{t}^{\rm
MC}=173$ GeV the pole mass NLL result reads $m_{t}^{\rm pole,NLL}=172.45\pm
0.52$ GeV, which is consistent with the NNLL result. Overall we find that
$m_{t}^{\rm MC}=m_{t}^{\rm pole}+(0.29\pm 0.40)\,{\rm GeV}$ at NNLL order for
MC top quark masses between $172$ and $174\,{\rm GeV}$. So $m_{t}^{\rm pole}$
and $m_{t,1\,{\rm GeV}}^{\rm MSR}$ may also be identified - however, only
within about $400\,{\rm MeV}$.

To the extent that the treatment of the top in MC generators and QCD
factorizes for different kinematically sensitive observables and from whether
one considers $e^{+}e^{-}$ or $pp$ collisions, our method can be used to
calibrate $m_{t}^{\rm MC}$ in current experimental reconstruction analyses. It
is nevertheless important to clarify to which extent the MC top quark mass
determined for one process and observable has this universal meaning. A
promising approach to this is to do a similar analysis as the one presented in
this work while considering a different process e.g. $pp$ or a sufficiently
different $e^{+}e^{-}$ observable. $pp$ collisions introduce initial state
radiation, color reconnection, and additional hadronization and multi-parton
interaction effects, not present in $e^{+}e^{-}$. A possible way around the
most troublesome complications for $pp$ is to use so called “light jet-
grooming” as in Ref. [29]. Alternatively, it is also interesting to explore
sufficiently different observables for $e^{+}e^{-}$ which will be described in
the following. Prior to this, we believe that applying our $e^{+}e^{-}$
calibration to $m_{t}^{\rm MC}$ from a typical $pp$ reconstruction analysis
will give a more accurate result than simply assuming $m_{t}^{\rm
MC}=m_{t}^{\rm pole}$.

### Exploring MC top quark mass universality with different $e^{+}e^{-}$
observables

One possibility for an alternative $e^{+}e^{-}$ observable is a mass-sensitive
version of C-parameter, defined as:

$C_{\rm M}=\frac{3}{2}\left[2-\frac{1}{Q^{2}}\sum_{i\neq j}\frac{(p_{i}\cdot
p_{j})^{2}}{p_{i}^{0}p_{j}^{0}}\right]\,.$ (5)

The $C_{M}$ observable coincides with the regular C-parameter definition for
massless final state particles and was already used in Ref. [30] due to its
favorable features when looking at massive final state particles. The biggest
difference compared with thrust is the strong sensitivity to the top quark
decay. Due to the clustering property of thrust, the events where the decay
products respect the original hemisphere division (which give the leading
contribution) contribute in the same way to the thrust distribution as in the
case of a stable top. This is why the decay inclusive formula from Eq. (3)
works well in this case. For the mass-sensitive C-parameter (subsequently we
will refer to this simply as C-parameter) a more differential treatment of the
decay is needed to describe the unstable distribution correctly. This fact
becomes obvious when looking at the difference in peak position in the stable
$C_{\rm M}^{\rm min}=12(m_{t}/Q)^{2}[1-(m_{t}/Q)^{2}]$ and unstable case
$C_{\rm M}^{\rm min}\approx 12(m_{t}/Q)^{2}[1-4(m_{t}/Q)^{2}]$.

For the leading contribution, which comes from those events where the decays
respect the hemisphere division, the factorization theorem for the singular
part can be extended to the following form:

$\displaystyle\frac{1}{\sigma_{0}}\frac{{\rm d}\sigma^{\rm unstable}}{{\rm
d}C_{M}}$ $\displaystyle=\int{\rm d}\bar{C}\frac{1}{\sigma_{0}}\frac{{\rm
d}\sigma^{\rm stable}_{\rm s}}{{\rm d}C_{M}}(C_{\rm M}-\bar{C})F(\bar{C})\,,$
(6)

where $\frac{1}{\sigma_{0}}\frac{{\rm d}\sigma^{\rm stable}}{{\rm d}C_{M}}$
represents the C-parameter factorization formula for stable top quarks in
analogy to Eq. (3). As indicated in Eq. (6) this expression needs to be
convoluted with an additional function $F$, called the _decay function_. It is
given by $F(\bar{C})=\int\prod_{i}{\rm d}\phi_{i}{\rm
d}\theta_{i}\,\delta(\bar{C}-C_{M}^{\rm decay}(\theta_{i},\phi_{i})+C_{\rm
M}^{\rm min})$ with $C_{M}^{\rm decay}(\theta_{i},\phi_{i})$ giving the value
of the C-parameter for the (anti-)top decay products and $\phi_{i}$ and
$\theta_{i}$ denoting the polar and azimuthal angles of the decay products in
the rest frame of the decaying particle. This function may account for NLO QCD
corrections to the top quark decay and basically accounts for the C-parameter
difference between the stable case and the unstable case where the (anti-)top
quark is produced at LO as an on-shell particle. At LO it can be obtained from
standard fixed-order Monte Carlo programs. This approach is exact in the limit
that top production and decay factorize and allows to treat the radiation off
the top with analytical tools, as in the case of thrust and subsequently takes
care of the (anti-)top quark decay in a more differential manner. With this
setup a comparably precise calibration should be feasible while considering a
more decay sensitive, hence significantly different observable and will be
discussed in more detail in an upcoming publication [31].

### Acknowledgment

We acknowledge partial support by the FWF Austrian Science Fund under the
Doctoral Program No. W1252-N27 and the Project No. P28535-N27, the Spanish
MINECO “Ramón y Cajal” program (RYC-2014-16022), the U.S. Department of Energy
under the Grant No. DE-SC0011090, and the Simons Foundation through the Grant
327942. We also thank the Erwin-Schrödinger International Institute for
Mathematics and Physics, the University of Vienna and Cultural Section of the
City of Vienna (MA7) for partial support.

## References

  * [1] Tevatron Electroweak Working group collaboration, CDF and D0, _Combination of CDF and D0 results on the mass of the top quark using up to 9.7 fb -1 at the Tevatron_, 1407.2682.
  * [2] CMS collaboration, V. Khachatryan et al., _Measurement of the top quark mass using proton-proton data at ${\sqrt{(s)}}$ = 7 and 8 TeV_, _Phys. Rev._ D93 (2016) 072004, [1509.04044].
  * [3] ATLAS collaboration, M. Aaboud et al., _Measurement of the top quark mass in the $t\bar{t}\to$ dilepton channel from $\sqrt{s}=8$ TeV ATLAS data_, _Phys. Lett._ B761 (2016) 350–371, [1606.02179].
  * [4] A. H. Hoang and I. W. Stewart, _Top Mass Measurements from Jets and the Tevatron Top-Quark Mass_ , _Nucl. Phys. Proc. Suppl._ 185 (2008) 220–226, [0808.0222].
  * [5] A. H. Hoang, _The Top Mass: Interpretation and Theoretical Uncertainties_ , in _7th International Workshop on Top Quark Physics (TOP2014) Cannes, France, September 28-October 3, 2014_ , 2014.  1412.3649.
  * [6] A. H. Hoang, A. Jain, I. Scimemi and I. W. Stewart, _Infrared Renormalization Group Flow for Heavy Quark Masses_ , _Phys. Rev. Lett._ 101 (2008) 151602, [0803.4214].
  * [7] M. Butenschoen, B. Dehnadi, A. H. Hoang, V. Mateu, M. Preisser and I. W. Stewart, _Top Quark Mass Calibration for Monte Carlo Event Generators_ , _Phys. Rev. Lett._ 117 (2016) 232001, [1608.01318].
  * [8] I. W. Stewart, F. J. Tackmann and W. J. Waalewijn, _N-Jettiness: An Inclusive Event Shape to Veto Jets_ , _Phys.Rev.Lett._ 105 (2010) 092002, [1004.2489].
  * [9] S. Fleming, A. H. Hoang, S. Mantry and I. W. Stewart, _Jets from massive unstable particles: Top-mass determination_ , _Phys. Rev._ D77 (2008) 074010, [hep-ph/0703207].
  * [10] S. Fleming, A. H. Hoang, S. Mantry and I. W. Stewart, _Top Jets in the Peak Region: Factorization Analysis with NLL Resummation_ , _Phys. Rev._ D77 (2008) 114003, [0711.2079].
  * [11] G. P. Korchemsky and G. Sterman, _Power corrections to event shapes and factorization_ , _Nucl. Phys._ B555 (1999) 335–351, [hep-ph/9902341].
  * [12] C. W. Bauer, S. Fleming and M. E. Luke, _Summing Sudakov logarithms in $B\to X_{s}\gamma$ in effective field theory_, _Phys. Rev._ D63 (2000) 014006, [hep-ph/0005275].
  * [13] C. W. Bauer, S. Fleming, D. Pirjol and I. W. Stewart, _An effective field theory for collinear and soft gluons: Heavy to light decays_ , _Phys. Rev. D_ 63 (2001) 114020, [hep-ph/0011336].
  * [14] C. W. Bauer and I. W. Stewart, _Invariant operators in collinear effective theory_ , _Phys. Lett. B_ 516 (2001) 134–142, [hep-ph/0107001].
  * [15] C. W. Bauer, D. Pirjol and I. W. Stewart, _Soft-Collinear Factorization in Effective Field Theory_ , _Phys. Rev._ D65 (2002) 054022, [hep-ph/0109045].
  * [16] A. H. Hoang, A. Pathak, P. Pietrulewicz and I. W. Stewart, _Hard Matching for Boosted Tops at Two Loops_ , _JHEP_ 12 (2015) 059, [1508.04137].
  * [17] A. Jain, I. Scimemi and I. W. Stewart, _Two-loop Jet-Function and Jet-Mass for Top Quarks_ , _Phys. Rev._ D77 (2008) 094008, [0801.0743].
  * [18] S. Gritschacher, A. H. Hoang, I. Jemos and P. Pietrulewicz, _Secondary Heavy Quark Production in Jets through Mass Modes_ , _Phys. Rev._ D88 (2013) 034021, [1302.4743].
  * [19] P. Pietrulewicz, S. Gritschacher, A. H. Hoang, I. Jemos and V. Mateu, _Variable Flavor Number Scheme for Final State Jets in Thrust_ , _Phys. Rev._ D90 (2014) 114001, [1405.4860].
  * [20] B. Dehnadi.  PhD thesis, University of Vienna, June, 2016.
  * [21] Z. Ligeti, I. W. Stewart and F. J. Tackmann, _Treating the b quark distribution function with reliable uncertainties_ , _Phys. Rev._ D78 (2008) 114014, [0807.1926].
  * [22] R. Abbate, M. Fickinger, A. H. Hoang, V. Mateu and I. W. Stewart, _Thrust at N 3LL with Power Corrections and a Precision Global Fit for $\alpha_{s}(m_{Z})$_, _Phys. Rev._ D83 (2011) 074021, [1006.3080].
  * [23] R. Abbate, M. Fickinger, A. H. Hoang, V. Mateu and I. W. Stewart, _Precision Thrust Cumulant Moments at N 3LL_, _Phys. Rev._ D86 (2012) 094002, [1204.5746].
  * [24] A. H. Hoang and I. W. Stewart, _Designing Gapped Soft Functions for Jet Production_ , _Phys. Lett._ B660 (2008) 483–493, [0709.3519].
  * [25] A. H. Hoang, A. Jain, I. Scimemi and I. W. Stewart, _R-evolution: Improving perturbative QCD_ , _Phys. Rev._ D82 (2010) 011501, [0908.3189].
  * [26] T. Sjöstrand, S. Mrenna and P. Z. Skands, _PYTHIA 6.4 Physics and Manual_ , _JHEP_ 05 (2006) 026, [hep-ph/0603175].
  * [27] T. Sjöstrand, S. Ask, J. R. Christiansen, R. Corke, N. Desai, P. Ilten et al., _An Introduction to PYTHIA 8.2_ , _Comput. Phys. Commun._ 191 (2015) 159–177, [1410.3012].
  * [28] P. Skands, S. Carrazza and J. Rojo, _Tuning PYTHIA 8.1: the Monash 2013 Tune_ , _Eur. Phys. J._ C74 (2014) 3024, [1404.5630].
  * [29] A. H. Hoang, S. Mantry, A. Pathak and I. W. Stewart, _Extracting a Short Distance Top Mass with Light Grooming_ , 1708.02586.
  * [30] E. Gardi and L. Magnea, _The C parameter distribution in $e^{+}e^{-}$ annihilation_, _JHEP_ 0308 (2003) 030, [hep-ph/0306094].
  * [31] A. H. Hoang, V. Mateu and M. Preisser _Work in progress_ (2018) .


# Self-Supervised Masked Digital Elevation Models Encoding for Low-Resource
Downstream Tasks

Priyam Mazumdar, Aiman Soliman, Volodymyr Kindratenko, Luigi Marini, and
Kenton McHenry
National Center for Supercomputing Applications
University of Illinois Urbana - Champaign
Urbana, IL 61801
{priyamm2, asoliman, kindrtnk, lmarini<EMAIL_ADDRESS>

###### Abstract

The lack of quality labeled data is one of the main bottlenecks for training
Deep Learning models. As the task increases in complexity, there is a higher
penalty for overfitting and unstable learning. The typical paradigm employed
today is Self-Supervised learning, where the model attempts to learn from a
large corpus of unstructured and unlabeled data and then transfer that
knowledge to the required task. Some notable examples of self-supervision in
other modalities are BERT for Large Language Models, Wav2Vec for Speech
Recognition, and the Masked AutoEncoder for Vision, which all utilize
Transformers to solve a masked prediction task. GeoAI is uniquely poised to
take advantage of the self-supervised methodology due to the decades of data
collected, little of which is precisely and dependably annotated. Our goal is
to extract building and road segmentations from Digital Elevation Models (DEM)
that provide a detailed topography of the earths surface. The proposed
architecture is the Masked Autoencoder pre-trained on ImageNet (with the
limitation that there is a large domain discrepancy between ImageNet and DEM)
with an UperNet Head for decoding segmentations. We tested this model with 450
and 50 training images only, utilizing roughly 5% and 0.5% of the original
data respectively. On the building segmentation task, this model obtains an
82.1% Intersection over Union (IoU) with 450 Images and 69.1% IoU with only 50
images. On the more challenging road detection task the model obtains an 82.7%
IoU with 450 images and 73.2% IoU with only 50 images. Any hand-labeled
dataset made today about the earths surface will be immediately obsolete due
to the constantly changing nature of the landscape. This motivates the clear
necessity for data-efficient learners that can be used for a wide variety of
downstream tasks.

_Keywords_ Self-Supervised Learning, Deep Learning, Masked Image Modeling,
GeoAI, DEM, Segmentation, Small-Data

##  1 Introduction

Deep Learning has provided powerful and highly predictive models for a wide
variety of tasks, but it often comes at the cost of the immense amount of data
needed to curtail overfitting and promote generalization Schmitt et al.
(2020). The onset of the Transfer Learning methodology has opened these tools
to solve more niche problems with smaller datasets Pires de Lima and Marfurt
(2019). A common strategy is to utilize a model that has been trained to
perform some objective and exploit its feature extraction capabilities to
fine-tune it toward another problem.

Unfortunately, many of these pre-trained models are trained in a supervised
fashion, using labeled data, which may not be available for some areas of
interest Schmitt et al. (2020). Ideally, features should be learned through
the dataset itself without any labels. This technique of Self-Supervised pre-
training has been the current method of building a model that generalizes
features of the data which can be used for any downstream tasks Wang et al.
(2021). There are two main features that enable these models to be so
efficient: (i) utilizing an encoder network that ingests randomly masked data
and a lightweight decoder network that attempts to reconstruct the masked
portions, in this process, the model is forced to learn global relationships
that can be utilized in downstream tasks. (ii): employing a Transformer
architecture Vaswani et al. (2017) which encodes relationships between tokens
via the Attention mechanism. In NLP and Speech, the attention gives the model
a temporal awareness by learning the relationships between words. For Vision,
the model encodes which patches of the image are most related to each other,
offering powerful global spatial awareness. The specific variant we are using
in this paper is the Masked AutoEncoder He et al. (2021).

The contribution of this paper is to evaluate the use of the Masked
Autoencoder pre-trained on ImageNet for different downstream segmentation
tasks of digital elevation models (i.e., segmenting building footprints and
roads), particularly with differences in the learning domain between
traditional optical images and digital elevation data (e.g., single channel
with large dynamic range).

Figure 1: Masked Autoencoder Backbone + UperNet Head The Masked Autoencoder is
composed of the typical encoder/decoder structure, where during pre-training,
75% of the image is masked out and we perform a reconstruction loss. Once pre-
trained, outputs of the encoder from four seperate transformer blocks are
stacked to form a feature pyramid that are then fused via the UperNet
architecture for segmentation.

Left - DEM, Right - Label

Figure 2: Example of Missing Road Labels Example of missing road segmentation
labels in unfiltered road dataset. Prompted to hand-curate a set of labels
with higher quality for our road segmentation task.

##  2 Related Works

Several researchers utilized weakly supervised learning to avoid the lack of
training datasets. For example, Wei and Ji (2021) applied weakly supervised
training successfully for the task of road segmentation. Similarly, Soliman et
al. (2022) evaluated an existing dataset to train models to extract building
footprints from DEM and Wang et al. (2020) used a single labeled pixel per
image to segment optical satellite images.

However, advances in utilizing self-supervised learning strategies in modeling
language Devlin et al. (2018) and in computer vision Dosovitskiy et al. (2020)
has motivated researchers to evaluate the self-supervised approach to train
deep learning models on feature representations from geospatial and remote
sensing data without human annotation. For example, Gao et al. (2022)
demonstrated that a masked autoencoder is capable of outperforming supervised
methods in different downstream tasks by learning how to reconstruct masked
patches in optical satellite images. Zhu et al. (2023) proposed SpectralMAE,
which is a spectral-masked autoencoder model designed to reconstruct
hyperspectral images. Similarly, Scheibenreif et al. (2023) applied a masked
autoencoder for Hyperspectral Image Classification.Wang et al. (2021)
developed Mask DeepLab as a model for change detection by teaching the model
how to construct time difference images, while Reed et al. (2022) demonstrated
how to incorporate a sense of geographic scale in MAE learning.

However, there is a lack of studies evaluating self-supervised models in
segmenting Digital Elevation Models. Especially since DEMs have contrasting
characteristics to optical images and could be subject to resolution loss
during data pre-processing, for example, by the loss of their large dynamic
from local normalization. In addition, it is important to evaluate the need
for pre-training MAE on a large corpus of DEMs similar to some of the
foundation models in optical remote sensing Sun et al. (2022).

##  3 Model Architecture Details

We utilized the base Masked AutoEncoder (MAE) that was pre-trained on ImageNet
Russakovsky et al. (2014a) as our backbone to our segmentation model. The
original images are 224 x 224 pixels and the ViT Patch Embedding module splits
this into 192 patches each with shape 16 x 16 pixels. Each patch of the image
is passed through a linear layer to encode it as a token with embedding
dimension of 768. In the masking step, 75% of the tokens are randomly hidden.
The Encoder portion of the MAE has 12 transformer blocks and each block has 12
heads in the Multi-Headed Attention computation. The MAE opts for a light
weight decoder (rather than a symmetrical encoder/decoder architecture) so the
token embeddings are first reduced in size from 768 to 512. There are 8
transformer blocks in the decoder with each having 16 heads. Another linear
layer takes the output from the decoder and returns the tokens back to the
original shape (16x16) so we can perform a reconstruction loss of the masked
tokens.

While the MAE backbone is used to encode our images, an additional module is
necessary to actually generate segmentation masks. To perform this task we
will utilize the UperNet head. The UperNet architecture employs a feature
pyramid network (FPN) Lin et al. (2016) that fuses information extracted from
different layers of the Masked Autoencoder (specifically transformer blocks 3,
5, 7, 11). A similar architecture was previously used in Li et al. (2023) for
extraction of permafrost features from the arctic, although with a
convolutional ResNet50 backbone. All implementation was done with the PyTorch
Framework Russakovsky et al. (2014b) and MMSegmentation Contributors (2020).

All models were trained for 3000 iterations (with validation at every 150
iterations) with a batch size of 8, and the best validation accuracy is
presented. The backbone was frozen and only the UperNet head was tuned for the
specific segmentation task. The AdamW optimizer was used with a weight decay
of 0.05 along with a Polynomial Learning Rate scheduler to help curtail
overfitting and promote smooth learning on small datasets. We also used a
pixel-wise categorical cross entropy for our loss function with added class
weights due to the large imbalance of background pixels versus the label
pixels. For comparison, we additionally trained a UNet Ronneberger et al.
(2015) model from scratch for the same small-data tasks to compare against
some more traditional methods.

##  4 Results and Discussion

We look at how our model, a frozen MAE, and a trained UperNet Head, compare
against the more typical UNet model for this task. We took samples of 450,
200, 50, and 10 images from both the visually-labeled road and building
training datasets with a constant 50 images for validation. The IoU for the
predicted class for each model is presented in table 1.

Table 1: IoU for Building (B) and Road (R) segmentation. Building and Road
Segmentation IoU
---
Num. Samples |  MAE (B) |  UNet (B) |  MAE (R) |  UNet (R)
10 |  55.5% |  27.9% |  37.1% |  23.4%
50 |  69.1% |  55.0% |  73.2% |  70.4%
200 |  76.1% |  68.2% |  81.3% |  77.9%
450 |  82.1% |  76.5% |  82.7% |  78.4%

Our methods provide reliable segmentation performance on very few samples. On
the building segmentation task, we obtain a performance of 55.5% IoU with only
10 images, about 50% better than a UNet. On the Road segmentation task,
training on 10 images doesn’t provides a dependable model. As we increase the
number of training samples in both road and building segmentation, our IoU
continues to increase with the MAE consistently outperforming the UNet.

The road segmentation task, specifically, has varying levels of difficulty
depending on the nature of the landscape and the elevation difference. The
original data were elevation rasters with a high dynamic range. In flat lands
with well-defined roads like highways, (i.e. Figure 3), the streets are much
more clearly separated after locally normalizing the image between the maximum
and minimum elevation. On the other hand, in residential areas (i.e. Figure
4), normalizing with the max elevations on top of buildings conceals the
roads. Even so, our model detects roads in these challenging conditions.

Left - DEM, Middle - Prediction, Right - Label

Figure 3: Road Segmentation with a minimum elevation difference from a model
trained on 450 images.

Left - DEM, Middle - Prediction, Right - Label

Figure 4: Road Segmentation with high elevation difference from a model
trained on 450 images.

We should also notice that although the manually labeled dataset was curated
carefully, there are a few errors related to the alignment of the visual label
dataset and the tiling, especially around the edges of the manually labeled
data. As we can see in Figure 5, labels may be missing for some of the
buildings. Nevertheless, our model is capable of predicting them accurately.
In addition, road labels currently have an average width, however, road widths
vary within and between cities.

Left - DEM, Middle - Prediction, Right - Label

Figure 5: Missing Building Segmentations Even in a curated dataset, there can
still be some errors in the labels, leading to a slight under-reporting of
true model performance Table 2: Results from training each model on all
available road data (with noisy labels) and validating on the 50 high-quality
images. Noisy Labels Segmentation IoU
---
MAE |  78.2%
UNet |  74.4%

Noisy data can sometimes be unavoidable without a significant effort of
continuously maintaining labels; therefore, we wanted to test the robustness
of our model by training on a large amount of variable quality road
segmentation. As shown above, we had roughly 10,000 training images of roads,
500 of which were visually inspected for completeness. In order to test the
robustness of our model, we trained on the entire set of images but validated
on the visually labeled/inspected validation set to allow for comparison to
other experiments. As shown in Table 2, the MAE and UNet obtain a 78.2% and
74.4% IoU respectively, which downgraded the performance compared to our
previous training on 450 high-quality images. This offers some additional
evidence that using a smaller sample of quality data outperforms having a
large corpus of unverified data (Weakly supervised).

##  5 Conclusions

We present self-supervised learning as an effective strategy to perform
various downstream tasks with limited data resources. We obtained encouraging
results using an ImageNet pre-trained backbone, even with the domain
discrepancy from DEM. Following this proof-of-concept, we plan to pre-train an
MAE on a large corpus of DEM datasets so the numerical encoding are more
salient and provides a substantial performance jump. In the future, this model
can be used for various downstream tasks: (1) Segmentation with the UperNet
head, (2) Classification with a simple linear head, and (3) Object Detection
using MAE as a backbone to the Detectron architecture Li et al. (2022).
Training a DEM-specific MAE is likely to result in enhancing the model
performance as there is evidence that scaling the model up provides
significant gains He et al. (2021). Access to an adequate amount of DEM data
and compute environments will enable pre-training large Geo-AI models to
provide a data-efficient DEM encoder and make possible low-resource learning
for Geospatial tasks.

##  6 Acknowledgements

This work is supported by funding from the National Science Foundation, award
number 1927729.

## References

  * Schmitt et al. [2020] Michael Schmitt, Jonathan Prexl, Patrick Ebel, Lukas Liebel, and Xiao Xiang Zhu.  Weakly supervised semantic segmentation of satellite images for land cover mapping–challenges and opportunities.  _arXiv preprint arXiv:2002.08254_ , 2020.
  * Pires de Lima and Marfurt [2019] Rafael Pires de Lima and Kurt Marfurt.  Convolutional neural network for remote-sensing scene classification: Transfer learning analysis.  _Remote Sensing_ , 12(1):86, 2019.
  * Wang et al. [2021] Yanheng Wang, Lianru Gao, Danfeng Hong, Jianjun Sha, Lian Liu, Bing Zhang, Xianhui Rong, and Yonggang Zhang.  Mask deeplab: End-to-end image segmentation for change detection in high-resolution remote sensing images.  _International Journal of Applied Earth Observation and Geoinformation_ , 104:102582, 2021.
  * Vaswani et al. [2017] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin.  Attention is all you need.  _CoRR_ , abs/1706.03762, 2017.  URL http://arxiv.org/abs/1706.03762.
  * He et al. [2021] Kaiming He, Xinlei Chen, Saining Xie, Yanghao Li, Piotr Dollár, and Ross B. Girshick.  Masked autoencoders are scalable vision learners.  _CoRR_ , abs/2111.06377, 2021.  URL https://arxiv.org/abs/2111.06377.
  * Wei and Ji [2021] Yao Wei and Shunping Ji.  Scribble-based weakly supervised deep learning for road surface extraction from remote sensing images.  _IEEE Transactions on Geoscience and Remote Sensing_ , 2021.
  * Soliman et al. [2022] Aiman Soliman, Yifan Chen, Shirui Luo, Rauf Makharov, and Volodymyr Kindratenko.  Weakly supervised segmentation of buildings in digital elevation models.  _IEEE Geoscience and Remote Sensing Letters_ , 19:1–5, 2022\.  doi:10.1109/LGRS.2022.3177160.
  * Wang et al. [2020] Sherrie Wang, William Chen, Sang Michael Xie, George Azzari, and David B Lobell.  Weakly supervised deep learning for segmentation of remote sensing imagery.  _Remote Sensing_ , 12(2):207, 2020.
  * Devlin et al. [2018] Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova.  BERT: pre-training of deep bidirectional transformers for language understanding.  _CoRR_ , abs/1810.04805, 2018.  URL http://arxiv.org/abs/1810.04805.
  * Dosovitskiy et al. [2020] Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, Jakob Uszkoreit, and Neil Houlsby.  An image is worth 16x16 words: Transformers for image recognition at scale.  _CoRR_ , abs/2010.11929, 2020.  URL https://arxiv.org/abs/2010.11929.
  * Gao et al. [2022] Yuan Gao, Xiaojuan Sun, and Chao Liu.  A general self-supervised framework for remote sensing image classification.  _Remote Sensing_ , 14(19):4824, 2022.
  * Zhu et al. [2023] Lingxuan Zhu, Jiaji Wu, Wang Biao, Yi Liao, and Dandan Gu.  Spectralmae: Spectral masked autoencoder for hyperspectral remote sensing image reconstruction.  _Sensors_ , 23(7):3728, 2023.
  * Scheibenreif et al. [2023] Linus Scheibenreif, Michael Mommert, and Damian Borth.  Masked vision transformers for hyperspectral image classification.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 2165–2175, 2023.
  * Reed et al. [2022] Colorado J Reed, Ritwik Gupta, Shufan Li, Sarah Brockman, Christopher Funk, Brian Clipp, Salvatore Candido, Matt Uyttendaele, and Trevor Darrell.  Scale-mae: A scale-aware masked autoencoder for multiscale geospatial representation learning.  _arXiv preprint arXiv:2212.14532_ , 2022.
  * Sun et al. [2022] Xian Sun, Peijin Wang, Wanxuan Lu, Zicong Zhu, Xiaonan Lu, Qibin He, Junxi Li, Xuee Rong, Zhujun Yang, Hao Chang, et al.  Ringmo: A remote sensing foundation model with masked image modeling.  _IEEE Transactions on Geoscience and Remote Sensing_ , 2022.
  * Russakovsky et al. [2014a] Olga Russakovsky, Jia Deng, Hao Su, Jonathan Krause, Sanjeev Satheesh, Sean Ma, Zhiheng Huang, Andrej Karpathy, Aditya Khosla, Michael S. Bernstein, Alexander C. Berg, and Li Fei-Fei.  Imagenet large scale visual recognition challenge.  _CoRR_ , abs/1409.0575, 2014a.  URL http://arxiv.org/abs/1409.0575.
  * Lin et al. [2016] Tsung-Yi Lin, Piotr Dollár, Ross B. Girshick, Kaiming He, Bharath Hariharan, and Serge J. Belongie.  Feature pyramid networks for object detection.  _CoRR_ , abs/1612.03144, 2016.  URL http://arxiv.org/abs/1612.03144.
  * Li et al. [2023] Wenwen Li, Chia-Yu Hsu, Sizhe Wang, Chandi Witharana, and Anna Liljedahl.  Real-time geoai for high-resolution mapping and segmentation of arctic permafrost features, 2023.
  * Russakovsky et al. [2014b] Olga Russakovsky, Jia Deng, Hao Su, Jonathan Krause, Sanjeev Satheesh, Sean Ma, Zhiheng Huang, Andrej Karpathy, Aditya Khosla, Michael S. Bernstein, Alexander C. Berg, and Li Fei-Fei.  Imagenet large scale visual recognition challenge.  _CoRR_ , abs/1409.0575, 2014b.  URL http://arxiv.org/abs/1409.0575.
  * Contributors [2020] MMSegmentation Contributors.  MMSegmentation: Openmmlab semantic segmentation toolbox and benchmark.  https://github.com/open-mmlab/mmsegmentation, 2020.
  * Ronneberger et al. [2015] Olaf Ronneberger, Philipp Fischer, and Thomas Brox.  U-net: Convolutional networks for biomedical image segmentation.  _CoRR_ , abs/1505.04597, 2015.  URL http://arxiv.org/abs/1505.04597.
  * Li et al. [2022] Yanghao Li, Hanzi Mao, Ross Girshick, and Kaiming He.  Exploring plain vision transformer backbones for object detection, 2022\.


* [26] Saul A Kripke.  Semantical analysis of intuitionistic logic I.  In Studies in Logic and the Foundations of Mathematics, volume 40, pages 92–130. Elsevier, 1965.
  * [27] René Lavendhomme and Thierry Lucas.  Sequent calculi and decision procedures for weak modal systems.  Studia Logica, 66(1):121–145, 2000.
  * [28] Björn Lellmann and Elaine Pimentel.  Modularisation of sequent calculi for normal and non-normal modalities.  ACM Trans. Comput. Log., 20(2):7:1–7:46, 2019.
  * [29] Edwin D Mares.  Classically complete modal relevant logics.  Mathematical Logic Quarterly, 39(1):165–177, 1993.
  * [30] Mathieu Marion and Mehrnouche Sadrzadeh.  Reasoning about knowledge in linear logic: modalities and complexity.  In Logic, epistemology, and the unity of science, pages 327–350. Springer, 2009.
  * [31] Michael Mendler and Valeria de Paiva.  Constructive CK for contexts.  In Proceedings of CRR’05. CEUR-WS, 2005.
  * [32] Michael Mendler and Stephan Scheele.  Cut-free gentzen calculus for multimodal CK.  Inf. Comput., 209(12):1465–1490, 2011.
  * [33] Eugenio Orlandelli.  Sequent calculi and interpolation for non-normal modal and deontic logics.  Logic and Logical Philosophy, 30(1):139–183, 2020.
  * [34] Eric Pacuit.  Neighborhood Semantics for Modal Logic.  Springer, 2017.
  * [35] Gordon D. Plotkin and Colin Stirling.  A framework for intuitionistic modal logics.  In Proceedings of TARK’86, pages 399–406. Morgan Kaufmann, 1986\.
  * [36] Daniele Porello and Nicolas Troquard.  Non-normal modalities in variants of linear logic.  Journal of Applied Non-Classical Logics, 25(3):229–255, 2015.
  * [37] Igor Sedlár.  Epistemic extensions of modal distributive substructural logics.  Journal of Logic and Computation, 26(6):1787–1813, 2016.
  * [38] Krister Segerberg.  Propositional logics related to Heyting’s and Johansson’s.  Theoria, 34(1):26–61, 1968.
  * [39] Takahiro Seki.  General frames for relevant modal logics.  Notre Dame Journal of Formal Logic, 44(2):93–109, 2003.
  * [40] Takahiro Seki.  A sahlqvist theorem for relevant modal logics.  Stud Logica, 73(3):383–411, 2003.
  * [41] Alex K. Simpson.  The proof theory and semantics of intuitionistic modal logic.  PhD thesis, University of Edinburgh, UK, 1994.
  * [42] Anne Sjerp Troelstra and Helmut Schwichtenberg.  Basic proof theory, Second Edition, volume 43 of Cambridge tracts in theoretical computer science.  Cambridge University Press, 2000.
  * [43] Duminda Wijesekera.  Constructive modal logics I.  Ann. Pure Appl. Log., 50(3):271–301, 1990.
  * [44] Duminda Wijesekera and Anil Nerode.  Tableaux for constructive concurrent dynamic logic.  Ann. Pure Appl. Log., 135(1-3):1–72, 2005.
  * [45] Frank Wolter and Michael Zakharyaschev.  Intuitionistic modal logics as fragments of classical bimodal logics.  In Logic at Work, pages 168–186. Springer, 1999.

## Appendix: Proofs of cut admissibility

See 3.1

###### Proof.

The proof follows a standard strategy that goes back to Gentzen [19] (cf. [42]
for more details) and consists in proving the admissibility of the following
generalisation of $\mathsf{cut}$

$\Gamma\Rightarrow A$ $\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Sigma\Rightarrow C$

also known as _multicut_ , where $A^{n}$ denotes one or more occurrences of
$A$. The proof shows that every derivation containing one or more applications
of $\mathsf{mix}$ can be transformed into an equivalent derivation not
containing applications of $\mathsf{mix}$ by removing step by step all topmost
applications of $\mathsf{mix}$. Let us call _mix formula_ the formula which is
deleted by the application of $\mathsf{mix}$. The proof proceeds by induction
on lexicographically ordered pairs $(c,h)$, where $c$ is the _complexity_ of
the mix formula, defined as usual as $c(p)=c(\bot)=1$, $c(B\circ
C)=c(B)+c(C)+1$, $C(\heartsuit B)=c(B)+1$, with
$\circ\in\\{\land,\lor,\supset\\}$, $\heartsuit\in\\{\Box,\Diamond\\}$, and
$h$ is the _cut height_ , defined as the sum of the heights of the mix-free
derivations of the premisses of $\mathsf{mix}$, where the height of a mix-free
derivation is in turn defined as the length of the longest branch from the
root to an initial sequent. The proof distinguishes among the following cases.
In each case, the derivation on the left is converted into the derivation on
the right, where the original application of $\mathsf{mix}$ is possibly
replaced by one or more applications of $\mathsf{mix}$, each of them having a
mix formula with lower complexity or a having lower mix height. In the
derivations, given a rule $R$, we denote $R^{*}$ an arbitrary number of
repeated applications of $R$.

  1. 1

At least one premiss of $\mathsf{mix}$ is an initial sequent. There are two
subcases.

  2. 1.1

The left premiss of $\mathsf{mix}$ is an initial sequent.

$A\Rightarrow A$ $\triangledown$ $\Gamma,A^{n}\Rightarrow C$ $\mathsf{mix}$
$\Gamma,A\Rightarrow C$ $\leadsto$ $\triangledown$ $\Gamma,A^{n}\Rightarrow C$
$\mathsf{ctr}_{\mathsf{L}}^{m}$∗ $\Gamma,A\Rightarrow C$

  3. 1.2

The right premiss of $\mathsf{mix}$ is an initial sequent.

$\triangledown$ $\Gamma\Rightarrow A$ $A\Rightarrow A$ $\mathsf{mix}$
$\Gamma\Rightarrow A$ $\leadsto$ $\triangledown$ $\Gamma\Rightarrow A$

  4. 2

Neither premiss of $\mathsf{mix}$ is an initial sequent. There are three
subcases.

  5. 2.1

The mix formula is not principal in the last rule applied in the derivation
$\mathcal{D}$ of the left premiss of $\mathsf{mix}$. We consider several cases
depending on the last rule applied in $\mathcal{D}$.

  6. ($\land^{m}_{\mathsf{L}}$)

$\triangledown$ $\Gamma,B_{i}\Rightarrow A$ $\land^{m}_{\mathsf{L}}$
$\Gamma,B_{1}\land B_{2}\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma,B_{1}\land
B_{2}\Rightarrow C$ $\leadsto$ $\triangledown$ $\Gamma,B_{i}\Rightarrow A$
$\triangledown$ $\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Sigma,B_{i}\Rightarrow C$ $\land^{m}_{\mathsf{L}}$
$\Gamma,\Sigma,B_{1}\land B_{2}\Rightarrow C$

  7. ($\lor^{m}_{\mathsf{L}}$)

$\triangledown$ $\Gamma,B\Rightarrow A$ $\triangledown$ $\Gamma,C\Rightarrow
A$ $\lor^{m}_{\mathsf{L}}$ $\Gamma,B\lor C\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,B\lor C\Rightarrow
D$ $\leadsto$

$\triangledown$ $\Gamma,B\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow D$
$\triangledown$ $\Gamma,C\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,C\Rightarrow D$
$\lor^{m}_{\mathsf{L}}$ $\Gamma,\Sigma,B\lor C\Rightarrow C$

  8. ($\supset^{m}_{\mathsf{L}}$)

$\triangledown$ $\Gamma\Rightarrow B$ $\triangledown$ $\Gamma,C\Rightarrow A$
$\supset^{m}_{\mathsf{L}}$ $\Gamma,B\supset C\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,B\supset
C\Rightarrow D$ $\leadsto$

$\triangledown$ $\Gamma\Rightarrow B$ $\mathsf{wk}_{\mathsf{L}}^{m}$∗
$\Gamma,\Sigma\Rightarrow B$ $\triangledown$ $\Gamma,C\Rightarrow A$
$\triangledown$ $\Sigma,A^{n}\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Sigma,C\Rightarrow D$ $\supset^{m}_{\mathsf{L}}$
$\Gamma,\Sigma,B\supset C\Rightarrow D$

  9. ($\mathsf{wk}_{\mathsf{L}}^{m}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\mathsf{wk}_{\mathsf{L}}^{m}$
$\Gamma,B\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow C$ $\leadsto$ $\triangledown$
$\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$ $\mathsf{wk}_{\mathsf{L}}^{m}$
$\Gamma,\Sigma,B\Rightarrow C$

  10. ($\mathsf{ctr}_{\mathsf{L}}^{m}$)

$\triangledown$ $\Gamma,B,B\Rightarrow A$ $\mathsf{ctr}_{\mathsf{L}}^{m}$
$\Gamma,B\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow C$ $\leadsto$ $\triangledown$
$\Gamma,B,B\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma,B,B\Rightarrow C$
$\mathsf{ctr}_{\mathsf{L}}^{m}$ $\Gamma,\Sigma,B\Rightarrow C$

  11. Right rules and $\mathsf{K}_{\Box}^{m}$, $\mathsf{K}_{\Diamond}^{m}$ are not possible.
  12. 2.2

The mix formula is not principal in the last rule applied in the derivation
$\mathcal{D}$ of the right premiss of $\mathsf{mix}$. We consider several
cases depending on the last rule applied in $\mathcal{D}$.

  13. ($\land^{m}_{\mathsf{L}}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B_{i}\Rightarrow C$ $\land^{m}_{\mathsf{L}}$
$\Sigma,A^{n},B_{1}\land B_{2}\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Sigma,B_{1}\land B_{2}\Rightarrow C$ $\leadsto$ $\triangledown$
$\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n},B_{i}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma,B_{i}\Rightarrow C$ $\land^{m}_{\mathsf{L}}$
$\Gamma,\Sigma,B_{1}\land B_{2}\Rightarrow C$

  14. ($\land^{m}_{\mathsf{R}}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$ $\land^{m}_{\mathsf{R}}$
$\Sigma,A^{n}\Rightarrow B\land C$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow
B\land C$ $\leadsto$

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B$ $\triangledown$
$\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$ $\land^{m}_{\mathsf{R}}$
$\Gamma,\Sigma\Rightarrow B\land C$

  15. ($\lor^{m}_{\mathsf{L}}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B\Rightarrow D$ $\triangledown$ $\Sigma,A^{n},C\Rightarrow D$
$\lor^{m}_{\mathsf{L}}$ $\Sigma,A^{n},B\lor C\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Sigma,B\lor C\Rightarrow D$ $\leadsto$

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow D$
$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},C\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,C\Rightarrow D$
$\lor^{m}_{\mathsf{L}}$ $\Gamma,\Sigma,B\lor C\Rightarrow D$

  16. ($\lor^{m}_{\mathsf{R}}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B_{i}$ $\lor^{m}_{\mathsf{R}}$ $\Sigma,A^{n}\Rightarrow B_{1}\lor B_{2}$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B_{1}\lor B_{2}$ $\leadsto$
$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B_{i}$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B_{i}$ $\lor^{m}_{\mathsf{R}}$
$\Gamma,\Sigma\Rightarrow B_{1}\lor B_{2}$

  17. ($\supset^{m}_{\mathsf{L}}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B$ $\triangledown$ $\Sigma,A^{n},C\Rightarrow D$ $\supset^{m}_{\mathsf{L}}$
$\Sigma,A^{n},B\supset C\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,B\supset
C\Rightarrow D$ $\leadsto$

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B$ $\triangledown$
$\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n},C\Rightarrow D$
$\mathsf{mix}$ $\Gamma,\Sigma,C\Rightarrow D$ $\supset^{m}_{\mathsf{L}}$
$\Gamma,\Sigma,B\supset C\Rightarrow D$

  18. ($\supset^{m}_{\mathsf{R}}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B\Rightarrow C$ $\supset^{m}_{\mathsf{R}}$
$\Sigma,A^{n}\Rightarrow B\supset C$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow
B\supset C$ $\leadsto$ $\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow C$
$\supset^{m}_{\mathsf{R}}$ $\Gamma,\Sigma\Rightarrow B\supset C$

  19. ($\mathsf{wk}_{\mathsf{L}}^{m}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
C$ $\mathsf{wk}_{\mathsf{L}}^{m}$ $\Sigma,A^{n},B\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Sigma,B\Rightarrow C$ $\leadsto$ $\triangledown$ $\Gamma\Rightarrow
A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Sigma\Rightarrow C$ $\mathsf{wk}_{\mathsf{L}}^{m}$
$\Gamma,\Sigma,B\Rightarrow C$

  20. ($\mathsf{ctr}_{\mathsf{L}}^{m}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B,B\Rightarrow C$ $\mathsf{ctr}_{\mathsf{L}}^{m}$
$\Sigma,A^{n},B\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow C$
$\leadsto$ $\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B,B\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma,B,B\Rightarrow
C$ $\mathsf{ctr}_{\mathsf{L}}^{m}$ $\Gamma,\Sigma,B\Rightarrow C$

  21. $\mathsf{K}_{\Box}^{m}$, $\mathsf{K}_{\Diamond}^{m}$ are not possible.
  22. 2.3

The mix formula is principal in the last rule applied in the derivations
$\mathcal{D}_{1}$, $\mathcal{D}_{2}$ of both premisses of $\mathsf{mix}$. We
consider several cases depending on the last rule applied in
$\mathcal{D}_{1}$, $\mathcal{D}_{2}$.

  23. ($\land^{m}_{\mathsf{R}}$ \- $\land^{m}_{\mathsf{L}}$)

The mix formula $A$ has the form $B\land C$. We consider the following case,
the other case where the premiss of $\land^{m}_{\mathsf{L}}$ is
$\Sigma,(B\land C)^{n-1},C\Rightarrow D$ is analogous.

$\triangledown$ $\Gamma\Rightarrow B$ $\triangledown$ $\Gamma\Rightarrow C$
$\land^{m}_{\mathsf{R}}$ $\Gamma\Rightarrow B\land C$ $\triangledown$
$\Sigma,(B\land C)^{n-1},B\Rightarrow D$ $\land^{m}_{\mathsf{L}}$
$\Sigma,(B\land C)^{n}\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow
D$ $\leadsto$

$\triangledown$ $\Gamma\Rightarrow B$ $\triangledown$ $\Gamma\Rightarrow B$
$\triangledown$ $\Gamma\Rightarrow C$ $\land^{m}_{\mathsf{R}}$
$\Gamma\Rightarrow B\land C$ $\triangledown$ $\Sigma,(B\land
C)^{n-1},B\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow D$
$\mathsf{mix}$ $\Gamma,\Gamma,\Sigma\Rightarrow D$
$\mathsf{wk}_{\mathsf{L}}^{m}$∗ $\Gamma,\Sigma\Rightarrow D$

  24. ($\lor^{m}_{\mathsf{R}}$ \- $\lor^{m}_{\mathsf{L}}$)

The mix formula $A$ has the form $B\lor C$. We consider the following case,
the other case where the premiss of $\lor^{m}_{\mathsf{R}}$ is
$\Gamma\Rightarrow C$ is analogous.

$\triangledown$ $\Gamma\Rightarrow B$ $\lor^{m}_{\mathsf{R}}$
$\Gamma\Rightarrow B\lor C$ $\triangledown$ $\Sigma,(B\lor
C)^{n-1},B\Rightarrow D$ $\triangledown$ $\Sigma,(B\lor C)^{n-1},C\Rightarrow
D$ $\lor^{m}_{\mathsf{L}}$ $\Sigma,(B\lor C)^{n}\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Sigma\Rightarrow D$ $\leadsto$

$\triangledown$ $\Gamma\Rightarrow B$ $\triangledown$ $\Gamma\Rightarrow B$
$\lor^{m}_{\mathsf{R}}$ $\Gamma\Rightarrow B\lor C$ $\triangledown$
$\Sigma,(B\lor C)^{n-1},B\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Sigma,B\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Gamma,\Sigma\Rightarrow
D$ $\mathsf{wk}_{\mathsf{L}}^{m}$n $\Gamma,\Sigma\Rightarrow D$

  25. ($\supset^{m}_{\mathsf{R}}$ \- $\supset^{m}_{\mathsf{L}}$)

The mix formula $A$ has the form $B\supset C$.

$\triangledown$ $\Gamma,B\Rightarrow C$ $\supset^{m}_{\mathsf{R}}$
$\Gamma\Rightarrow B\supset C$ $\triangledown$ $\Sigma,(B\supset
C)^{n-1}\Rightarrow B$ $\triangledown$ $\Sigma,(B\supset C)^{n-1},C\Rightarrow
D$ $\supset^{m}_{\mathsf{L}}$ $\Sigma,(B\supset C)^{n}\Rightarrow D$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow D$ $\leadsto$

$\triangledown$ $\Gamma,B\Rightarrow C$ $\supset^{m}_{\mathsf{R}}$
$\Gamma\Rightarrow B\supset C$ $\triangledown$ $\Sigma,(B\supset
C)^{n-1}\Rightarrow B$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B$
$\triangledown$ $\Gamma,B\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Gamma,\Sigma\Rightarrow C$ $(\ast)$

$\Gamma,\Gamma,\Sigma\Rightarrow C$ $(\ast)$ $\triangledown$
$\Gamma,B\Rightarrow C$ $\supset^{m}_{\mathsf{R}}$ $\Gamma\Rightarrow B\supset
C$ $\triangledown$ $\Sigma,(B\supset C)^{n-1},C\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Sigma,C\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Gamma,\Gamma,\Sigma\Rightarrow D$ $\mathsf{ctr}_{\mathsf{L}}^{m}$∗
$\Gamma,\Sigma\Rightarrow D$

  26. ($R$ \- $\mathsf{ctr}_{\mathsf{L}}^{m}$)

The transformation below applies for any last rule $R$ in the derivation of
the left premiss of $\mathsf{mix}$.

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},A\Rightarrow C$ $\mathsf{ctr}_{\mathsf{L}}^{m}$
$\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$
$\leadsto$ $\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},A\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$

  27. ($R$ \- $\mathsf{wk}_{\mathsf{L}}^{m}$)

The transformation below applies for any last rule $R$ in the derivation of
the left premiss of $\mathsf{mix}$ (note that if $n=1$, then the conclusion of
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$ can be obtained from
$\Sigma\Rightarrow C$ by $\mathsf{wk}_{\mathsf{L}}^{m}$).

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n-1}\Rightarrow C$ $\mathsf{wk}_{\mathsf{L}}^{m}$
$\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$
$\leadsto$ $\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n-1}\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$

  28. ($\mathsf{K}_{\Box}^{m}$ \- $\mathsf{K}_{\Box}^{m}$)

The mix formula $A$ has the form $\Box B$.

$\triangledown$ $\Sigma\Rightarrow B$ $\mathsf{K}_{\Box}^{m}$
$\Box\Sigma\Rightarrow\Box B$ $\triangledown$ $B^{n},\Pi\Rightarrow C$
$\mathsf{K}_{\Box}^{m}$ $(\Box B)^{n},\Box\Pi\Rightarrow\Box C$ $\mathsf{mix}$
$\Box\Sigma,\Box\Pi\Rightarrow\Box C$ $\leadsto$ $\triangledown$
$\Sigma\Rightarrow B$ $\triangledown$ $B^{n},\Pi\Rightarrow C$ $\mathsf{mix}$
$\Sigma,\Pi\Rightarrow C$ $\mathsf{K}_{\Box}^{m}$
$\Box\Sigma,\Box\Pi\Rightarrow\Box C$

  29. ($\mathsf{K}_{\Box}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$)

The mix formula $A$ has the form $\Box B$.

$\triangledown$ $\Sigma\Rightarrow B$ $\mathsf{K}_{\Box}^{m}$
$\Box\Sigma\Rightarrow\Box B$ $\triangledown$ $B^{n},\Pi,C\Rightarrow D$
$\mathsf{K}_{\Diamond}^{m}$ $(\Box B)^{n},\Box\Pi,\Diamond
C\Rightarrow\Diamond D$ $\mathsf{mix}$ $\Box\Sigma,\Box\Pi,\Diamond
C\Rightarrow\Diamond D$ $\leadsto$ $\triangledown$ $\Sigma\Rightarrow B$
$\triangledown$ $B^{n},\Pi,C\Rightarrow D$ $\mathsf{mix}$
$\Sigma,\Pi,C\Rightarrow D$ $\mathsf{K}_{\Diamond}^{m}$
$\Box\Sigma,\Box\Pi,\Diamond C\Rightarrow\Diamond D$

  30. ($\mathsf{K}_{\Diamond}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$)

The mix formula $A$ has the form $\Diamond C$.

$\triangledown$ $\Sigma,B\Rightarrow C$ $\mathsf{K}_{\Diamond}^{m}$
$\Box\Sigma,\Diamond B\Rightarrow\Diamond C$ $\triangledown$ $\Pi,C\Rightarrow
D$ $\mathsf{K}_{\Diamond}^{m}$ $\Box\Pi,\Diamond C\Rightarrow\Diamond D$
$\mathsf{mix}$ $\Box\Sigma,\Box\Pi,\Diamond B\Rightarrow\Diamond D$ $\leadsto$
$\triangledown$ $\Sigma,B\Rightarrow C$ $\triangledown$ $\Pi,C\Rightarrow D$
$\mathsf{mix}$ $\Sigma,\Pi,B\Rightarrow D$ $\mathsf{K}_{\Diamond}^{m}$
$\Box\Sigma,\Box\Pi,\Diamond B\Rightarrow\Diamond D$

∎

See 5.8

###### Proof.

We extend the cases in the proof of Theorem 3.1 with the analysis of the new
modal rules. The cases 1.1 and 1.2 are as before.

  1. 2.1

The mix formula is not principal in the last rule applied in the derivation
$\mathcal{D}$ of the left premiss of $\mathsf{mix}$.

  2. ($\mathsf{T}_{\Box}^{m}$)

$\triangledown$ $\Gamma,B\Rightarrow A$ $\mathsf{T}_{\Box}^{m}$ $\Gamma,\Box
B\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$ $\mathsf{mix}$
$\Gamma,\Sigma,\Box B\Rightarrow C$ $\leadsto$ $\triangledown$
$\Gamma,B\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow C$ $\mathsf{T}_{\Box}^{m}$
$\Gamma,\Sigma,\Box B\Rightarrow C$

  3. 2.2

The mix formula is not principal in the last rule applied in the derivation
$\mathcal{D}$ of the right premiss of $\mathsf{mix}$.

  4. ($\mathsf{T}_{\Box}^{m}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B\Rightarrow C$ $\mathsf{T}_{\Box}^{m}$ $\Sigma,A^{n},\Box
B\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma,\Box B\Rightarrow C$ $\leadsto$
$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n},B\Rightarrow C$ $\mathsf{mix}$ $\Gamma,\Sigma,B\Rightarrow C$
$\mathsf{T}_{\Box}^{m}$ $\Gamma,\Sigma,\Box B\Rightarrow C$

  5. ($\mathsf{T}_{\Diamond}^{m}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow
B$ $\mathsf{T}_{\Diamond}^{m}$ $\Sigma,A^{n}\Rightarrow\Diamond B$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow\Diamond B$ $\leadsto$ $\triangledown$
$\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow B$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B$ $\mathsf{T}_{\Diamond}^{m}$
$\Gamma,\Sigma\Rightarrow\Diamond B$

  6. 2.3

The mix formula is principal in the last rule applied in the derivations
$\mathcal{D}_{1}$, $\mathcal{D}_{2}$ of both premisses of $\mathsf{mix}$. For
the cases where the last rule applied in $\mathcal{D}_{1}$, $\mathcal{D}_{2}$
is propositional see the proof of Theorem 3.1. We show the other cases.

  7. ($\mathsf{N}_{\Box}^{m}$ \- $\mathsf{M}_{\Box}^{m}$)

The mix formula $A$ has the form $\Box B$.

$\triangledown$ $\Rightarrow B$ $\mathsf{N}_{\Box}^{m}$ $\Rightarrow\Box B$
$\triangledown$ $B\Rightarrow C$ $\mathsf{M}_{\Box}^{m}$ $\Box
B\Rightarrow\Box C$ $\mathsf{mix}$ $\Rightarrow\Box C$ $\leadsto$
$\triangledown$ $\Rightarrow B$ $\triangledown$ $B\Rightarrow C$
$\mathsf{mix}$ $\Rightarrow C$ $\mathsf{N}_{\Box}^{m}$ $\Rightarrow\Box C$

  8. ($\mathsf{P}_{\Diamond}^{m}$ \- $\mathsf{M}_{\Diamond}^{m}$)

The mix formula $A$ has the form $\Diamond B$.

$\triangledown$ $\Rightarrow B$ $\mathsf{P}_{\Diamond}^{m}$
$\Rightarrow\Diamond B$ $\triangledown$ $B\Rightarrow C$
$\mathsf{M}_{\Diamond}^{m}$ $\Diamond B\Rightarrow\Diamond C$ $\mathsf{mix}$
$\Rightarrow\Diamond C$ $\leadsto$ $\triangledown$ $\Rightarrow B$
$\triangledown$ $B\Rightarrow C$ $\mathsf{mix}$ $\Rightarrow C$
$\mathsf{P}_{\Diamond}^{m}$ $\Rightarrow\Diamond C$

  9. ($\mathsf{N}_{\Box}^{m}$ \- $\mathsf{D}^{m}$)

The mix formula $A$ has the form $\Box B$ (note that by definition
$\mathsf{P}_{\Diamond}^{m}$ belongs to the calculus).

$\triangledown$ $\Rightarrow B$ $\mathsf{N}_{\Box}^{m}$ $\Rightarrow\Box B$
$\triangledown$ $B\Rightarrow C$ $\mathsf{D}^{m}$ $\Box B\Rightarrow\Diamond
C$ $\mathsf{mix}$ $\Rightarrow\Diamond C$ $\leadsto$ $\triangledown$
$\Rightarrow B$ $\triangledown$ $B\Rightarrow C$ $\mathsf{mix}$ $\Rightarrow
C$ $\mathsf{P}_{\Diamond}^{m}$ $\Rightarrow\Diamond C$

  10. ($\mathsf{N}_{\Box}^{m}$ \- $\mathsf{T}_{\Box}^{m}$)

The mix formula $A$ has the form $\Box B$.

$\triangledown$ $\Rightarrow B$ $\mathsf{N}_{\Box}^{m}$ $\Rightarrow\Box B$
$\triangledown$ $\Gamma,(\Box B)^{n-1},B\Rightarrow C$ $\mathsf{T}_{\Box}^{m}$
$\Gamma,(\Box B)^{n}\Rightarrow C$ $\mathsf{mix}$ $\Gamma\Rightarrow C$
$\leadsto$

$\triangledown$ $\Rightarrow B$ $\triangledown$ $\Rightarrow B$
$\mathsf{N}_{\Box}^{m}$ $\Rightarrow\Box B$ $\triangledown$ $\Gamma,(\Box
B)^{n-1},B\Rightarrow C$ $\mathsf{mix}$ $\Gamma,B\Rightarrow C$ $\mathsf{mix}$
$\Gamma\Rightarrow C$

  11. ($\mathsf{C}_{\Box}^{m}$ \- $\mathsf{C}_{\Box}^{m}$)

The mix formula $A$ has the form $\Box C$.

$\triangledown$ $\Sigma,B\Rightarrow C$ $\mathsf{C}_{\Box}^{m}$
$\Box\Sigma,\Box B\Rightarrow\Box C$ $\triangledown$ $C^{n},\Pi\Rightarrow D$
$\mathsf{C}_{\Box}^{m}$ $(\Box C)^{n},\Box\Pi\Rightarrow\Box D$ $\mathsf{mix}$
$\Box\Sigma,\Box\Pi,\Box B\Rightarrow\Box D$ $\leadsto$ $\triangledown$
$\Sigma,B\Rightarrow C$ $\triangledown$ $C^{n},\Pi\Rightarrow D$
$\mathsf{mix}$ $\Sigma,\Pi,B\Rightarrow D$ $\mathsf{C}_{\Box}^{m}$
$\Box\Sigma,\Box\Pi,\Box B\Rightarrow\Box D$

  12. ($\mathsf{C}_{\Box}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$)

The mix formula $A$ has the form $\Box C$.

$\triangledown$ $\Sigma,B\Rightarrow C$ $\mathsf{C}_{\Box}^{m}$
$\Box\Sigma,\Box B\Rightarrow\Box C$ $\triangledown$ $C^{n},\Pi,D\Rightarrow
E$ $\mathsf{K}_{\Diamond}^{m}$ $(\Box C)^{n},\Box\Pi,\Diamond
D\Rightarrow\Diamond E$ $\mathsf{mix}$ $\Box\Sigma,\Box\Pi,\Box B,\Diamond
D\Rightarrow\Diamond E$ $\leadsto$

$\triangledown$ $\Sigma,B\Rightarrow C$ $\triangledown$
$C^{n},\Pi,D\Rightarrow E$ $\mathsf{mix}$ $\Sigma,\Pi,B,D\Rightarrow E$
$\mathsf{K}_{\Diamond}^{m}$ $\Box\Sigma,\Box\Pi,\Box B,\Diamond
D\Rightarrow\Diamond E$

  13. ($\mathsf{C}_{\Box}^{m}$ \- $\mathsf{CD}^{m}$)

The mix formula $A$ has the form $\Box C$.

$\triangledown$ $\Sigma,B\Rightarrow C$ $\mathsf{C}_{\Box}^{m}$
$\Box\Sigma,\Box B\Rightarrow\Box C$ $\triangledown$ $C^{n},\Pi\Rightarrow D$
$\mathsf{CD}^{m}$ $(\Box C)^{n},\Box\Pi\Rightarrow\Diamond D$ $\mathsf{mix}$
$\Box\Sigma,\Box B,\Box\Pi\Rightarrow\Diamond D$ $\leadsto$ $\triangledown$
$\Sigma,B\Rightarrow C$ $\triangledown$ $C^{n},\Pi\Rightarrow D$
$\mathsf{mix}$ $\Sigma,B,\Pi\Rightarrow D$ $\mathsf{CD}^{m}$ $\Box\Sigma,\Box
B,\Box\Pi\Rightarrow\Diamond D$

  14. ($\mathsf{CD}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$)

The mix formula $A$ has the form $\Diamond B$.

$\triangledown$ $\Sigma\Rightarrow B$ $\mathsf{CD}^{m}$
$\Box\Sigma\Rightarrow\Diamond B$ $\triangledown$ $\Pi,B\Rightarrow C$
$\mathsf{K}_{\Diamond}^{m}$ $\Box\Pi,\Diamond B\Rightarrow\Diamond C$
$\mathsf{mix}$ $\Box\Sigma,\Box\Pi\Rightarrow\Diamond C$ $\leadsto$
$\triangledown$ $\Sigma\Rightarrow B$ $\triangledown$ $\Pi,B\Rightarrow C$
$\mathsf{mix}$ $\Sigma,\Pi\Rightarrow C$ $\mathsf{CD}^{m}$
$\Box\Sigma,\Box\Pi\Rightarrow\Diamond C$

  15. ($\mathsf{C}_{\Box}^{m}$ \- $\mathsf{T}_{\Box}^{m}$)

The mix formula $A$ has the form $\Box C$.

$\triangledown$ $\Sigma,B\Rightarrow C$ $\mathsf{C}_{\Box}^{m}$
$\Box\Sigma,\Box B\Rightarrow\Box C$ $\triangledown$ $\Gamma,(\Box
C)^{n-1},C\Rightarrow D$ $\mathsf{T}_{\Box}^{m}$ $\Gamma,(\Box
C)^{n}\Rightarrow D$ $\mathsf{mix}$ $\Gamma,\Box\Sigma,\Box B\Rightarrow D$
$\leadsto$

$\triangledown$ $\Sigma,B\Rightarrow C$ $\triangledown$ $\Sigma,B\Rightarrow
C$ $\mathsf{C}_{\Box}^{m}$ $\Box\Sigma,\Box B\Rightarrow\Box C$
$\triangledown$ $\Gamma,(\Box C)^{n-1},C\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Box\Sigma,\Box B,C\Rightarrow D$ $\mathsf{mix}$
$\Gamma,\Box\Sigma,\Box B,\Sigma,B\Rightarrow D$ $\mathsf{T}_{\Box}^{m}$∗
$\Gamma,\Box\Sigma,\Box B,\Box\Sigma,\Box B\Rightarrow D$
$\mathsf{ctr}_{\mathsf{L}}^{m}$∗ $\Gamma,\Box\Sigma,\Box B\Rightarrow D$

  16. ($\mathsf{T}_{\Diamond}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$)

The mix formula $A$ has the form $\Diamond B$.

$\triangledown$ $\Gamma\Rightarrow B$ $\mathsf{T}_{\Diamond}^{m}$
$\Gamma\Rightarrow\Diamond B$ $\triangledown$ $\Sigma,B\Rightarrow C$
$\mathsf{K}_{\Diamond}^{m}$ $\Box\Sigma,\Diamond B\Rightarrow\Diamond C$
$\mathsf{mix}$ $\Gamma,\Box\Sigma\Rightarrow\Diamond C$ $\leadsto$
$\triangledown$ $\Gamma\Rightarrow B$ $\triangledown$ $\Sigma,B\Rightarrow C$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow C$ $\mathsf{T}_{\Box}^{m}$∗
$\Gamma,\Box\Sigma\Rightarrow C$ $\mathsf{T}_{\Diamond}^{m}$
$\Gamma,\Box\Sigma\Rightarrow\Diamond C$

For the remaining combinations, ($\mathsf{M}_{\Box}^{m}$ \-
$\mathsf{M}_{\Box}^{m}$) is analogous to ($\mathsf{C}_{\Box}^{m}$ \-
$\mathsf{C}_{\Box}^{m}$) with $|\Sigma|=|\Pi|=0$ and $n=1$;
($\mathsf{M}_{\Diamond}^{m}$ \- $\mathsf{M}_{\Diamond}^{m}$) is analogous to
($\mathsf{K}_{\Diamond}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$) with
$|\Sigma|=|\Pi|=0$; ($\mathsf{M}_{\Box}^{m}$ \- $\mathsf{D}^{m}$) is analogous
to ($\mathsf{C}_{\Box}^{m}$ \- $\mathsf{CD}^{m}$) with $|\Sigma|=|\Pi|=0$ and
$n=1$; ($\mathsf{D}^{m}$ \- $\mathsf{M}_{\Diamond}^{m}$) is analogous to
($\mathsf{CD}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$) with $|\Sigma|=|\Pi|=0$;
($\mathsf{M}_{\Box}^{m}$ \- $\mathsf{T}_{\Box}^{m}$) is analogous to
($\mathsf{C}_{\Box}^{m}$ \- $\mathsf{T}_{\Box}^{m}$) with $|\Sigma|=0$; and
($\mathsf{T}_{\Diamond}^{m}$ \- $\mathsf{M}_{\Diamond}^{m}$) is analogous to
($\mathsf{T}_{\Diamond}^{m}$ \- $\mathsf{K}_{\Diamond}^{m}$) with
$|\Sigma|=0$. ∎

See 5.11

###### Proof.

We extend the cases in the proof of Theorem 5.8 with the combinations
involving $\bot^{i}_{\mathsf{L}}$ and $\mathsf{wk}_{\mathsf{R}}^{i}$. The
cases 1.1 and 2.1 are as in the proof of Theorem 5.8.

  1. 1.2

The right premiss of $\mathsf{mix}$ is the initial sequent
$\bot^{i}_{\mathsf{L}}$:

$\triangledown$ $\Gamma\Rightarrow\bot$ $\bot\Rightarrow$ $\mathsf{mix}$
$\Gamma\Rightarrow$

We need to consider the last rule applied in the derivation of the left
premiss of $\mathsf{mix}$ $\Gamma\Rightarrow\bot$, which is a left
propositional rule or $\mathsf{T}_{\Box}^{i}$. We show as an example the
latter possibility.

$\triangledown$ $\Gamma,B\Rightarrow\bot$ $\mathsf{T}_{\Box}^{i}$ $\Gamma,\Box
B\Rightarrow\bot$ $\bot\Rightarrow$ $\mathsf{mix}$ $\Gamma,\Box B\Rightarrow$
$\leadsto$ $\triangledown$ $\Gamma,B\Rightarrow\bot$ $\bot\Rightarrow$
$\mathsf{mix}$ $\Gamma,B\Rightarrow$ $\mathsf{T}_{\Box}^{i}$ $\Gamma,\Box
B\Rightarrow$

  2. 2.2

The mix formula is not principal in the last rule applied in the derivation
$\mathcal{D}$ of the right premiss of $\mathsf{mix}$.

  3. ($\mathsf{wk}_{\mathsf{R}}^{i}$)

$\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow$ $\mathsf{wk}_{\mathsf{R}}^{i}$
$\Sigma,A^{n}\Rightarrow B$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow B$
$\leadsto$ $\triangledown$ $\Gamma\Rightarrow A$ $\triangledown$
$\Sigma,A^{n}\Rightarrow$ $\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow$
$\mathsf{wk}_{\mathsf{R}}^{i}$ $\Gamma,\Sigma\Rightarrow B$

  4. 2.3

The mix formula is principal in the last rule applied in the derivations
$\mathcal{D}_{1}$, $\mathcal{D}_{2}$ of both premisses of $\mathsf{mix}$.

  5. ($\mathsf{wk}_{\mathsf{R}}^{i}$ \- $R$)

The transformation below applies for any last rule $R$ in the derivation of
the left premiss of $\mathsf{mix}$.

$\triangledown$ $\Gamma\Rightarrow$ $\mathsf{wk}_{\mathsf{R}}^{i}$
$\Gamma\Rightarrow A$ $\triangledown$ $\Sigma,A^{n}\Rightarrow\delta$
$\mathsf{mix}$ $\Gamma,\Sigma\Rightarrow\delta$ $\leadsto$ $\triangledown$
$\Gamma\Rightarrow$ $\mathsf{wk}_{\mathsf{L}}^{i}$∗ (if $|\Sigma|\geq 0$)
$\Gamma,\Sigma\Rightarrow$ $\mathsf{wk}_{\mathsf{R}}^{i}$∗ (if $|\delta|=1$)
$\Gamma,\Sigma\Rightarrow\delta$

∎