# Excitation of the 229Th nucleus by the hole in the inner electronic shells

M. G. Kozlov1,2 A. V. Oleynichenko1 D. Budker3,4 D. A. Glazov5 Y. V. Lomachuk1
V. M. Shabaev6,1 A. V. Titov1 I. I. Tupitsyn6 A. V. Volotka5 1 Petersburg
Nuclear Physics Institute of NRC “Kurchatov Institute”, Gatchina, Leningrad
District 188300, Russia
2 St. Petersburg Electrotechnical University LETI, St. Petersburg 197376,
Russia
3 Helmholtz-Institut, GSI Helmholtzzentrum fur Schwerionenforschung, Mainz
55128, Germany
4 Johannes Gutenberg University, Mainz 55128, Germany
5 School of Physics and Engineering, ITMO University, Kronverkskiy 49, 197101
St. Petersburg, Russia
6 Department of Physics, St. Petersburg State University, Ulianovskaya 1,
Petrodvorets, 198504 St. Petersburg, Russia

###### Abstract

The 229Th nucleus has a long-lived isomeric state $A^{*}$ at 8.338(24) eV
[Kraemer et al, Nature, 617, 706 (2023)]. This state is connected to the
ground state by an M1 transition. For a hydrogenlike Th ion in the $1s$ state
the hyperfine structure splitting is about 0.7 eV. This means that the
hyperfine interaction can mix the nuclear ground state with the isomeric state
with a mixing coefficient $\beta$ about 0.03. If the electron is suddenly
removed from this system, the nucleus will be left in the mixed state. The
probability to find the nucleus in the isomeric state $A^{*}$ is equal to
$\beta^{2}\sim 10^{-3}$. For the $2s$ state the effect is roughly two orders
of magnitude smaller. An atom with a hole in the $1s$ or $2s$ shell is similar
to the hydrogenlike atom, only the hole has a short lifetime $\tau$. After the
hole is filled, there is a non-zero probability to find the nucleus in the
$A^{*}$ state. Estimates of this probability are presented along with a
discussion of possible experiments on Th-doped xenotime-type orthophosphate
crystals and other broad band gap materials.

The isomeric state $A^{*}$ $(\tfrac{3}{2}^{+})$ of the 229Th nucleus lies
$\Delta\approx 8.3$ eV above the ground state $A$ $(I^{\pi}=\tfrac{5}{2}^{+})$
[1, 2, 3]. This state is widely considered as ideal candidate for the creation
of a nuclear optical clock [4, 5]. That, as expected, will further stimulate
many practical and fundamental applications, including studying new physics
[6, 7, 8, 9], observing Dicke and Mössbauer effects in the UV range [10, 11],
and others. The properties of this metastable state have been investigated
experimentally [12, 13, 14] but these studies are hampered due to the limited
number of isomeric nuclei. That is why lot of attention is paid to find an
optimal way to populate isomeric state.

At present the 229Th in the isomeric state $A^{*}$ is usually directly
produced in nuclear reactions (for example, as a result of $\alpha$-decay of
233U). Alternatively, one can try to excite 229Th to the isomeric state [15,
16, 17]. Here we discuss a relatively simple way to achieve this goal using
the hyperfine mixing of nuclear states [18, 19, 20]. This may help to perform
accurate measurement of the nuclear transition frequency, which is crucial for
making an optical nuclear clock.

The hyperfine structure constants for the $1s$ and $2s$ electrons in the
hydrogenlike thorium are $a(1s)\approx 0.68$ eV and $a(2s)\approx 0.09$ eV
[20]. The off-diagonal hyperfine matrix element $b$ between nuclear states $A$
and $A^{*}$ is expected to be of the same order of magnitude, $b\sim a$ [18,
19]. Following Refs. [21, 22, 20], we assume that $|b(1s)|\approx 0.24$ and
$|b(2s)|\approx 0.03$. The hole in the $1s$, or in the $2s$ shell has the
hydrogenlike wavefunction and, therefore, the hydrogenlike values of the
hyperfine parameters.

Let us consider a process of the hole production in either $1s$ or $2s$ shell
of neutral thorium. This can be done by photo-ionization [23, 24, 25], or by
electron-impact ionization [26, 27]. The hole lives for a finite time $\tau$,
and during this time the non-diagonal hyperfine interaction mixes two low-
energy nuclear states. When the hole is filled, the nucleus is left in one of
these two states. Below we estimate the probability to find the nucleus in the
$A^{*}$ state. To this end, we first need to estimate the energy and the
lifetime of the hole.

The Dirac-Fock energies are $\varepsilon_{1s}\approx 111$ keV and
$\varepsilon_{2s}\approx 21$ keV. The lifetime of the hole is determined by
the radiative width [28]:

$\displaystyle\gamma_{1s}\approx 90\,\mathrm{eV};$
$\displaystyle\gamma_{2s}\approx 14\,\mathrm{eV}.$ (1)

Let us discuss how the hole in the inner shell is formed. Suppose, we use a
high-energy photon to excite an electron to the continuum ($E_{\gamma}\gtrsim
100$ keV for the K-shell and $E_{\gamma}\gtrsim 20$ keV for the L-shell). The
interaction operator has the form $j_{\mu}A^{\mu}$, where $A^{\mu}$ is vector
potential and the current $j_{\mu}$, generally speaking, includes electronic
and nuclear parts, $j_{\mu}=j_{\mu}^{(e)}+j_{\mu}^{(N)}$. However, the nucleus
has the $A^{*}$ level at 8 eV and only a few levels in the sub-MeV range.
Thus, for such photons we can neglect the nuclear term. We conclude that
photons interact only with the electronic degrees of freedom and do not affect
the nucleus. Then, in the shake-off approximation, the electron disappears
instantaneously, leaving the nucleus unchanged. For closed electronic shells
there is no magnetic interaction with the nucleus and the nucleus remains in
its ground state. When the hole is created, the nucleus starts to interact
magnetically with the spin of the hole. The non-diagonal part of this
interaction leads to mixing between nuclear states $A$ and $A^{*}$. The hole
lives for the average time $\tau$ before it is filled with an electron from
one of the higher shells. Once the hole is refilled, magnetic interaction
“turns off” and the nucleus is left in one of its eigenstates. Naively one can
expect that the probability $P^{*}$ to find the nucleus in the state $A^{*}$
is on the order of $(b\tau)^{2}$. Since this probability depends on both $b$
and $\tau$, it may be beneficial to have a hole in a shell other than the K
shell. Below we estimate $P^{*}$ more accurately, and find that it is almost
the same for K and for L1 shells.

Figure 1: Schematic level structure of 229Th ion with a hole in the inner $ns$
shell, $n=1,2$. $\Delta\approx 8.3$ eV is the energy of the isomeric nuclear
state $A^{*}$ $(I^{\pi}=\tfrac{3}{2}^{+})$. Blue dashed lines are allowed
transitions of the hole to the $(n+1)p$ shell. The hyperfine splittings for
the two nuclear states are comparable, while for the electronic $(n+1)p$ state
it is much smaller than for $ns$ state. The fine structure for the $p$ shell
is not shown.

## Four-level model.

A simplified level structure of the atom with a hole is shown in Fig. 1. The
upper four levels correspond to the hole in the inner shell $ns$, where
$n=1,2,...$. The lower four levels describe the atom with a hole in the
$(n+1)p$ shell. The hyperfine structure for these levels is much smaller and
we neglect it. For the $ns$ hole we include the non-diagonal hyperfine
interaction between two levels with the same total angular momentum $F=2$.
Radiative decay to the $(n+1)p$ state is described by the width $\gamma$. This
gives us a two-level model with the effective Hamiltonian:

$\displaystyle H_{\mathrm{eff}}$
$\displaystyle=\left(\begin{array}[]{cc}\omega-\frac{i}{2}\gamma&b\\\
b&\omega+\Delta-\frac{i}{2}\gamma\end{array}\right)\,.$ (4)

Here $\Delta\approx 8.3$ eV is the nuclear excitation energy, $\gamma$ is the
width of the electronic $ns$ state, $b$ is the non-diagonal hyperfine matrix
element, and $\omega$ is the energy interval to the $(n+1)p$ shell. The
problem with this model is that in the end we have zero population of both
states and it is difficult to estimate the probability $P^{*}$.

Let us consider a slightly more advanced four-level model. In addition to the
two $F=2$ levels for the $ns$ shell we add two levels in the $(n+1)p$ shell
separated by the energy interval $\omega$. Due to the fine and hyperfine
structure, there are, in fact, more than two levels where the $ns$ hole can
decay, but this should not significantly affect our conclusions. The
Hamiltonian now has the form:

$\displaystyle H=\left(\begin{array}[]{cccc}0&0&0&0\\\ 0&\Delta&0&0\\\
0&0&\omega&b\\\ 0&0&b&\omega+\Delta\end{array}\right)\,.$ (9)

We will describe this system by the density matrix $\rho$:

$\displaystyle\rho=\left(\begin{array}[]{cccc}p&0&0&0\\\ 0&p_{*}&0&0\\\
0&0&s&r\\\ 0&0&r^{*}&s_{*}\end{array}\right)\,.$ (14)

In this matrix, $s$ and $p$ correspond to the electron in $ns$ and $(n+1)p$
shells respectively and the nucleus in the ground state $A$; $s_{*}$ and
$p_{*}$ correspond to the nucleus in the excited state $A^{*}$.

The density matrix $\rho$ obeys the Liouville equation,

$\displaystyle\dot{\rho}$ $\displaystyle=-i\left[H,\rho\right]+\Lambda\,,$
(15)

where we set $\hbar=1$ and the matrix $\Lambda$ describes decay and pumping of
the levels:

$\displaystyle\Lambda=\gamma\left(\begin{array}[]{cccc}s&0&0&0\\\
0&s_{*}&0&0\\\ 0&0&-s&-r\\\ 0&0&-r^{*}&-s_{*}\end{array}\right)\,.$ (20)

We look for the solution of Eq. (15) with the initial condition $s(0)=1$ and
other variables equal to zero. At the asymptotic limit $t=\infty$ only $p$ and
$p_{*}$ are nonzero due to the decay of the $ns$ hole. In this model the
probability to find the nucleus in the excited state is $P^{*}=p_{*}(\infty)$.

Plugging (9,20) in (15) we get:

$\displaystyle\left\\{\begin{array}[]{lcl}\dot{p}&=&+\gamma s\,,\\\
\dot{p}_{*}&=&+\gamma s_{*}\,,\\\ \dot{s}&=&-ib(r^{*}-r)-\gamma s\,,\\\
\dot{s_{*}}&=&+ib(r^{*}-r)-\gamma s_{*}\,,\\\ \dot{r}&=&+ib(s-s_{*})+i\Delta
r-\gamma r\,,\\\ \dot{r^{*}}&=&-ib(s-s_{*})-i\Delta r^{*}-\gamma r^{*}\,.\\\
\end{array}\right.$ (27)

Remaining parameters of the density matrix are not linked to the parameter $s$
and, therefore, are all equal to zero at all times. This argument justifies
the form of the density matrix assumed in Eq. (14).

We see that the variables $s$, $s_{*}$, $r$, and $r^{*}$ do not depend on $p$
and $p_{*}$. We can make the following substitution:

$\displaystyle\left\\{\begin{array}[]{lcl}s&=&\frac{1}{2}e^{-\gamma
t}\left(1+\zeta\right)\,,\\\ s_{*}&=&\frac{1}{2}e^{-\gamma
t}\left(1-\zeta\right)\,,\\\ r&=&e^{-\gamma t}\left(\xi+i\varphi\right)\,.\\\
\end{array}\right.$ (31)

After that, the four lower equations of system (27) give:

$\displaystyle\dot{\zeta}$ $\displaystyle=-4b\varphi\,,$
$\displaystyle\zeta(0)=1\,,$ (32a) $\displaystyle\dot{\varphi}$
$\displaystyle=b\zeta+\Delta\xi\,,$ $\displaystyle\varphi(0)=0\,,$ (32b)
$\displaystyle\dot{\xi}$ $\displaystyle=-\Delta\varphi\,,$
$\displaystyle\xi(0)=0\,.$ (32c)

Let us differentiate (32b) and then use (32a) and (32c) for the right hand
side:

$\displaystyle\ddot{\varphi}$
$\displaystyle=b\dot{\zeta}+\Delta\dot{\xi}=-(4b^{2}+\Delta^{2})\varphi\,,\quad\Rightarrow$
(33) $\displaystyle\varphi$
$\displaystyle=\varphi_{0}\sin{\sqrt{4b^{2}+\Delta^{2}}t}\,.$ (34)

Equations (32a) and (32c) show that $\zeta$ and $\xi$ oscillate at the same
frequency as $\varphi$ and have the relative phase shift $\pi/2$. Therefore,
the solution, which satisfies initial conditions must have the form:

$\displaystyle\zeta$ $\displaystyle=(1-A)+A\cos{\sqrt{4b^{2}+\Delta^{2}}t}\,,$
(35) $\displaystyle\xi$
$\displaystyle=B\left(1-\cos{\sqrt{4b^{2}+\Delta^{2}}t}\right)\,.$ (36)

Substituting these expressions into (32), we get:

$\displaystyle A$ $\displaystyle=\frac{4b^{2}}{4b^{2}+\Delta^{2}}\,,$ (37)
$\displaystyle B$ $\displaystyle=-\frac{b\Delta}{4b^{2}+\Delta^{2}}\,,$ (38)
$\displaystyle\varphi_{0}$
$\displaystyle=\frac{b}{\sqrt{4b^{2}+\Delta^{2}}}\,.$ (39)

We can now write the matrix element $s_{*}$ of the density matrix:

$\displaystyle s_{*}$ $\displaystyle=e^{-\gamma
t}\frac{2b^{2}}{4b^{2}+\Delta^{2}}\left(1-\cos{\sqrt{4b^{2}+\Delta^{2}}t}\right)\,.$
(40)

Substituting this into the second equation in (27) and integrating this
equation from zero to infinity, we find:

$\displaystyle P^{*}=p_{*}(\infty)$
$\displaystyle=\frac{2b^{2}}{\gamma^{2}+4b^{2}+\Delta^{2}}\approx\frac{2b^{2}}{\gamma^{2}+\Delta^{2}}\,,$
(41)

where we took into account that $|b|\ll\Delta$. If we also neglect $\Delta$ in
the denominator, we reproduce the naive estimate given above up to a factor of
2.

Numerically Eq. (41) gives:

$\displaystyle P^{*}(1s)$
$\displaystyle=\frac{2b_{1s}^{2}}{\gamma_{1s}^{2}+\Delta^{2}}\sim 1\times
10^{-5}\,,$ (42) $\displaystyle P^{*}(2s)$
$\displaystyle=\frac{2b_{2s}^{2}}{\gamma_{2s}^{2}+\Delta^{2}}\sim 7\times
10^{-6}\,.$ (43)

We see that the probability to excite the nucleus for the $1s$ and $2s$ holes
is almost the same. The numerator in (41) rapidly decreases for the principle
quantum numbers $n>2$, while the denominator remains practically constant.
Thus, for the higher shells the probability to excite the nucleus is much
smaller. Taking into account much larger energy of the K hole, we conclude
that the optimal variant is to use L1 holes.

## Yield estimate of the isomeric nuclei.

Keeping in mind the narrow width of the nuclear transition, its experimental
study requires a large number of nuclei in the state $A^{*}$. The yield of
these metastable nuclei depends on the probability $P^{*}$, the number of the
229Th ions in the sample $N$, and the photon flux $F_{p}$ from the X-ray
source, if we use photo-ionization, or the electron flux $F_{e}$ if we use
electron impact to produce $2s$ holes.

To have large $N$ we need a solid sample with high concentration of 229Th. The
host crystal must be transparent for the 8.3 eV photons, which means a
sufficiently broad band gap. Moreover, the lifetime of the nuclear $A^{*}$
state depends on the oxidation state of thorium because the internal
conversion and electronic bridge processes drastically decrease the lifetime
of the isomeric state for Th and Th+ [29, 30, 31]. Thus, in order to suppress
these processes the Th2+, Th3+ or Th4+ ions immobilized in the solid matrix
are desirable. To sum up, an important problem to be studied separately is
finding a suitable material with such a wide band gap. Last but not least, the
solid sample should not degrade too quickly under the irradiation with X-ray
photons, thus the high radiation resistance of the material is also desirable.

In general there are two ways towards preparation of such 229Th-containing
solid samples. Within the first one thorium ions (or ions of the 229Th isotope
predecessors) are directly implanted into a thin film of the material. A
notable experiment of this type is reported in [32] where this technique was
used to determine the isomeric transition energy (some signal was detected,
however, characteristic energy was $7.1\,(+0.1-0.2)$ eV, which strongly
disagrees with other experiments). The beam of thorium ions was obtained by
laser ablation of a 229Th-enriched target and then implanted in a thin film of
SiO2 (with band gap $E_{g}\sim 9$ eV). The number of thorium nuclei in the
sample was estimated to be $N\approx 3\cdot 10^{12}$ [32]. The other class of
materials suitable for such experiments with wide band gap (10 eV and higher)
is fluorides of alkali and alkaline-earth metals. In the recent experiment [3]
radioactive ion beams of nuclei with the mass number $A=229$ (229Fr, 229Ra)
were implanted in CaF2 (band gap of 12.1 eV [33]) and MgF2 (12.4 eV [34])
crystals at 30 keV, with subsequent series of $\beta$-decays resulting in
229mTh nuclei. The observed signal from the M1 nuclear transition $A^{*}\to A$
suggested that only several percent of the implanted thorium ions decayed via
this channel. This could be explained by the fact that low-oxidation states of
thorium are favorable in such crystal environments. This is in qualitative
agreement with the previous theoretical predictions [35, 36]. The bottleneck
of experiments with such beams is their relatively low intensities ($\sim
10^{6}$ particles per second), which does not allow us to hope for $N>10^{10}$
in the prepared sample. Moreover, fluorides are unstable under such beams and
undergo metamictisation processes.

The other way is to perform experiments with crystals of pure thorium
compounds or some synthetic Th-doped materials. To the best of our knowledge,
ThF4 is the only purely thorium compound with a wide band gap (10.4 eV [37]);
the oxidation state of Th in this compound is +4, thus preventing internal
conversion processes. One can also consider the other fluoride matrix,
lanthanum fluoride LaF3, whose band gap was also found to be quite wide, 9.7
eV [38]. In this case the crystal should be doped with the Th3+ impurity ions.
Band gaps for many other rare-earth fluorides are smaller and do not appear to
be promising. The radiation resistance of these fluorides is questionable.
Among other materials which can be regarded as matrices for Th ions, there are
yttrium and lutetium orthophosphates (YPO4 and LuPO4), which seem to be the
most suitable ones due to their outstandingly large band gaps (8.6–9.4 eV for
YPO4 [39, 40, 41, 42] and 8.6–9.3 eV for LuPO4 [43, 44, 39, 40]; one can
expect higher band gap values for perfect crystals) and high chemical and
radiation resistance (see [45, 46] and references therein). Natural YPO4 is
the xenotime mineral; it is known that xenotime does not undergo
metamictisation on geological time scales. This is due to its rigid crystal
lattice formed by the PO4 groups which is not destroyed by radiation-induced
defects. The favorable oxidation state of Th in YPO4 is expected to be +3,
this was also confirmed theoretically [47]; the same could be expected for
LuPO4 due to the same crystal structure and proximity of ionic radii and
electronegativiy of Y3+ and Lu3+ cations. It should be pointed out that
chemical synthesis and subsequent growth of crystals of either ThF4 or
phosphates considered here are not problematic; appropriate techniques are
well established.

Despite these unique properties of phosphate matrices, there are several
issues still to be addressed. First of all, large amounts of thorium dopant
ions and other point defects can result in a decrease in the band gap. The
presence of thorium ions leads to significant lowering of symmetry of local
sites [47] and, at high concentrations of Th, the low-symmetry monazite-type
structure is more stable, with typically small band gaps ($\sim 3$ eV for
monazite CePO4 [48]). Moreover, one can also expect the appearance of Th-rich
domains with monazite structure. The optimal concentration of thorium ions
avoiding a significant decrease in the band gap can be estimated theoretically
but more reliable values should be rather obtained experimentally in real
crystalline samples. Typical mole fraction of impurity ions in typical
synthetic lanthanide-doped phosphate crystals is of order 0.1%. To estimate
the number of 229Th nuclei $N$ achievable in such a solid state experiment one
can use the value of molality measured for the 229Th NIST Standard Reference
Materials [49], which was found to be $1.2\times 10^{-10}$ mol g-1 [50].
Consider a macroscopic sample of Th-doped xenotime of mass 1 g. It will
contain $\approx 1.3\times 10^{-3}$ g of thorium. Multiplying this value by
the molality from [50], one obtains $1.5\times 10^{-13}$ mol or $N\sim
10^{11}$ nuclei of 229Th for such a sample. This is comparable with $N\sim
10^{12}$ reported for the experiment with SiO2 thin films [32]. However, an
experiment with xenotime does not require any beams and seems to be simpler
from the point of view of preparation. Moreover, 229Th can be produced in
nuclear reactors [51] and then used to prepare 229Th-rich samples of doped
xenotime with $N\gg 10^{12}$.

Another non-obvious obstacle is the possible presence of additional narrow
band gaps due to the $7p$-states of the substituting Th3+ ions which in
principle can overlap with the resonance frequency of nuclear isomeric
transition. The $P_{1/2}^{o}$ and $P_{3/2}^{o}$ states of the Th3+ atomic ion
occur at 7.47 and 9.06 eV, respectively [52], but in the solid matrix they can
be significantly shifted down (like energy levels of the Ce3+ impurity ions in
cerium-doped xenotime, see [53]). A theoretical study of these impurity levels
will be presented in a separate paper [54].

Another important parameter is the photon flux $F_{p}$. The photoionization
cross section from the L shell of thorium has been measured in Refs. [23, 24,
25]. A conventional vacuum X-ray tube can be used as a source of photons in
the 20–100 keV range. Synchrotron sources provide orders-of-magnitude higher
fluxes.

Let us estimate the required photon flux. The lifetime of the $A^{*}$ nuclear
state in the wide band gap crystal is expected to be on the order of $10^{3}$
s, so we can accumulate isomeric nuclei for a time $T\sim 10^{3}$ s. Suppose
we want to produce $1\times 10^{6}$ isomeric nuclei. Following Ref. [50] we
assume 229Th molality of $1\times 10^{-10}$ mol g-1 [50], therefore, we need
to produce $\sim 6\times 10^{18}$ $2s_{F=2}$ holes. For the optimal photon
energy about 20 – 25 keV most of these photons will be absorbed by the thorium
L shell electrons and $\tfrac{2}{8}\times\tfrac{5}{12}\approx 0.1$ of them
will be $2s_{F=2}$ electrons. This means that we need the photon flux
$F_{p}\sim 6\times 10^{16}$ s-1, which corresponds to a dissipated power in
the sample $\sim 200$ W. These numbers look realistic. Using 229Th-rich sample
we can produce more isomeric nuclei for the same experimental conditions, or
we can reduce the photon flux and dissipated power.

## Acknowledgements.

D.B. contributed to this work prior to February 2022. He was supported in part
by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation)
Project ID 390831469: EXC 2118 (PRISMA+ Cluster of Excellence) and the
Helmholtz Excellence Network ExNet02. The work on the analysis of possible
solid state experiments (by A.V.O., Y.V.L. and A.V.T. at NRC “Kurchatov
Institute” – PNPI) was supported by the Russian Science Foundation (Grant No.
20-13-00225, https://rscf.ru/en/project/23-13-45028/).

## References

  * Seiferle  _et al._ [2019] B. Seiferle, L. von der Wense, P. V. Bilous, I. Amersdorffer, C. Lemell, F. Libisch, S. Stellmer, T. Schumm, C. E. Düllmann, A. Pálffy, and P. G. Thirolf, Nature 573, 243 (2019).
  * Sikorsky  _et al._ [2020] T. Sikorsky, J. Geist, D. Hengstler, S. Kempf, L. Gastaldo, C. Enss, C. Mokry, J. Runke, C. E. Düllmann, P. Wobrauschek, K. Beeks, V. Rosecker, J. H. Sterba, G. Kazakov, T. Schumm, and A. Fleischmann, Physical Review Letters 125, 142503 (2020).
  * Kraemer  _et al._ [2023] S. Kraemer, J. Moens, M. Athanasakis-Kaklamanakis, S. Bara, K. Beeks, P. Chhetri, K. Chrysalidis, A. Claessens, T. E. Cocolios, J. G. M. Correia, H. D. Witte, R. Ferrer, S. Geldhof, R. Heinke, N. Hosseini, M. Huyse, U. Köster, Y. Kudryavtsev, M. Laatiaoui, R. Lica, G. Magchiels, V. Manea, C. Merckling, L. M. C. Pereira, S. Raeder, T. Schumm, S. Sels, P. G. Thirolf, S. M. Tunhuma, P. V. D. Bergh, P. V. Duppen, A. Vantomme, M. Verlinde, R. Villarreal, and U. Wahl, Nature 617, 706 (2023).
  * Peik and Tamm [2003] E. Peik and C. Tamm, Europhys. Lett. 61, 181 (2003).
  * Rellergert  _et al._ [2010] W. G. Rellergert, D. DeMille, R. R. Greco, M. P. Hehlen, J. R. Torgerson, and E. R. Hudson, Physical Review Letters 104, 200802 (2010).
  * Flambaum [2006] V. V. Flambaum, Physical Review Letters 97, 092502 (2006), arXiv:physics/0604188 .
  * Berengut  _et al._ [2009] J. C. Berengut, V. A. Dzuba, V. V. Flambaum, and S. G. Porsev, Phys. Rev. Lett. 102, 210801 (2009), arXiv:0903.1891 .
  * Safronova  _et al._ [2018a] M. S. Safronova, D. Budker, D. DeMille, D. F. Jackson Kimball, A. Derevianko, and C. W. Clark, Rev. Mod. Phys. 90, 025008 (2018a), 10.1103/RevModPhys.90.025008, arXiv:1710.01833 .
  * Fadeev  _et al._ [2020] P. Fadeev, J. C. Berengut, and V. V. Flambaum, Phys. Rev. A 102, 052833 (2020).
  * Dicke [1953] R. H. Dicke, Physical Review 89, 472 (1953).
  * Tkalya [2011] E. V. Tkalya, Physical Review Letters 106, 162501 (2011).
  * von der Wense  _et al._ [2016] L. von der Wense, B. Seiferle, M. Laatiaoui, J. B. Neumayr, H.-J. Maier, H.-F. Wirth, C. Mokry, J. Runke, K. Eberhardt, C. E. Düllmann, N. G. Trautmann, and P. G. Thirolf, Nature 533, 47 (2016), 1710.11398 .
  * Thielking  _et al._ [2018] J. Thielking, M. V. Okhapkin, P. Glowacki, D. M. Meier, L. von der Wense, B. Seiferle, C. E. Düllmann, P. G. Thirolf, and E. Peik, Nature 556, 321 (2018), 1709.05325 [nucl-ex] .
  * Safronova  _et al._ [2018b] M. S. Safronova, S. G. Porsev, M. G. Kozlov, J. Thielking, M. V. Okhapkin, P. Głowacki, D. M. Meier, and E. Peik, Phys. Rev. Lett. 121, 213001 (2018b), arXiv:1806.03525 .
  * von der Wense  _et al._ [2020] L. von der Wense, P. V. Bilous, B. Seiferle, S. Stellmer, J. Weitenberg, P. G. Thirolf, A. Pálffy, and G. Kazakov, The European Physical Journal A 56 (2020), 10.1140/epja/s10050-020-00177-x.
  * Beeks [2022] K. A. A. G. Beeks,  _The Nuclear Excitation of Thorium-229 in the CaF 2 Environment_, Ph.D. thesis, Technische Universität Wien (2022).
  * Jin  _et al._ [2023] J. Jin, H. Bekker, T. Kirschbaum, Y. A. Litvinov, A. Pálffy, J. Sommerfeldt, A. Surzhykov, P. G. Thirolf, and D. Budker, Phys. Rev. Res. 5, 023134 (2023).
  * Lyuboshitz  _et al._ [1966] V. L. Lyuboshitz, V. A. Onishchuk, and M. I. Podgoretskij, Sov. J. Nucl. Phys. 3, 420 (1966).
  * Karpeshin  _et al._ [1998] F. F. Karpeshin, S. Wycech, I. M. Band, M. B. Trzhaskovskaya, M. Pfützner, and J. Żylicz, Phys. Rev. C 57, 3085 (1998).
  * Shabaev  _et al._ [2022] V. M. Shabaev, D. A. Glazov, A. M. Ryzhkov, C. Brandau, G. Plunien, W. Quint, A. M. Volchkova, and D. V. Zinenko, Physical Review Letters 128, 043001 (2022), arXiv:2109.01642 .
  * Minkov and Pálffy [2019] N. Minkov and A. Pálffy, Physical Review Letters 122, 162502 (2019).
  * Shigekawa  _et al._ [2021] Y. Shigekawa, A. Yamaguchi, K. Suzuki, H. Haba, T. Hiraki, H. Kikunaga, T. Masuda, S. Nishimura, N. Sasao, A. Yoshimi, and K. Yoshimura, Physical Review C 104, 024306 (2021).
  * Puri  _et al._ [1999] S. Puri, D. Mehta, J. Shahi, M. Garg, N. Singh, and P. Trehan, Nuclear Instruments and Methods in Physics Research Section B: Beam Interactions with Materials and Atoms 152, 19 (1999).
  * Kumar  _et al._ [2001] A. Kumar, S. Puri, J. S. Shahi, M. L. Garg, D. Mehta, and N. Singh, Journal of Physics B: Atomic, Molecular and Optical Physics 34, 613 (2001).
  * Kumar  _et al._ [2002] A. Kumar, S. Puri, D. Mehta, M. L. Garg, and N. Singh, X-Ray Spectrometry 31, 103 (2002).
  * Xu and Xu [1995] J. Q. Xu and X. J. Xu, Phys. Rev. B 51, 7834 (1995).
  * Rahangdale  _et al._ [2015] H. V. Rahangdale, P. K. Das, S. De, J. P. Santos, D. Mitra, M. Guerra, and S. Saha, “Absolute L-shell ionization and X-ray production cross sections of Lead and Thorium by 16-45 keV electron impact,” (2015), arXiv:1508.02877 [physics.atom-ph] .
  * Campbell and Papp [2001] J. L. Campbell and T. Papp, Atomic Data and Nuclear Data Tables 77, 1 (2001).
  * Tkalya [2003] E. V. Tkalya, Physics-Uspekhi 46, 315 (2003).
  * Karpeshin and Trzhaskovskaya [2007] F. F. Karpeshin and M. B. Trzhaskovskaya, Physical Review C 76, 054313 (2007).
  * Porsev and Flambaum [2010] S. G. Porsev and V. V. Flambaum, Phys. Rev. A 81, 042516 (2010).
  * Borisyuk  _et al._ [2018] P. V. Borisyuk, E. V. Chubunova, N. N. Kolachevsky, Y. Y. Lebedinskii, O. S. Vasiliev, and E. V. Tkalya, “Excitation of 229Th nuclei in laser plasma: the energy and half-life of the low-lying isomeric state,” (2018), arXiv:1804.00299 .
  * Rubloff [1972] G. W. Rubloff, Phys. Rev. B 5, 662 (1972).
  * Thomas  _et al._ [1973] J. Thomas, G. Stephan, J. C. Lemonnier, M. Nisar, and S. Robin, Phys. Stat. Sol. 56, 163 (1973).
  * Dessovic  _et al._ [2014] P. Dessovic, P. Mohn, R. A. Jackson, G. Winkler, M. Schreitl, G. Kazakov, and T. Schumm, Journal of Physics: Condensed Matter 26, 105402 (2014).
  * Pimon  _et al._ [2020] M. Pimon, J. Gugler, P. Mohn, G. A. Kazakov, N. Mauser, and T. Schumm, Journal of Physics: Condensed Matter 32, 255503 (2020).
  * Gouder  _et al._ [2019] T. Gouder, R. Eloirdi, R. L. Martin, M. Osipenko, M. Giovannini, and R. Caciuffo, Phys. Rev. Res. 1, 033005 (2019).
  * Wiemhöfer  _et al._ [1990] H.-D. Wiemhöfer, S. Harke, and U. Vohrer, Solid State Ion. 40-41, 433 (1990).
  * Balcerzyk  _et al._ [2000] M. Balcerzyk, Z. Gontarz, M. Moszynski, and M. Kapusta, J. Lumin. 87-89, 963 (2000).
  * Makhov  _et al._ [2002] V. N. Makhov, N. Y. Kirikova, M. Kirm, J. C. Krupa, P. Liblik, A. Lushchik, C. Lushchik, E. Negodin, and G. Zimmerer, Nucl. Instrum. Methods. Phys. Res. A 486, 437 (2002).
  * Wang  _et al._ [2009] D.-W. Wang, S.-H. Huang, F.-T. You, and Y. Tao, Chinese Phys. C 33, 1019 (2009).
  * Poolton  _et al._ [2010] N. R. J. Poolton, A. J. J. Bos, G. O. Jones, and P. Dorenbos, J. Phys. Condens. Matter 22, 185403 (2010).
  * Nakazawa and Shiga [1977] E. Nakazawa and F. Shiga, J. Lumin. 15, 255 (1977).
  * Lempicki  _et al._ [1993] A. Lempicki, A. J. Wojtowicz, and E. Berman, Nucl. Instrum. Methods. Phys. Res. A 333, 304 (1993).
  * Urusov  _et al._ [2012] V. S. Urusov, A. E. Grechanovsky, and N. N. Eremin, Glass Phys. Chem. 38, 55 (2012).
  * Cutts [2016] G. Cutts,  _Radiation Damage in Xenotime: An Atomistic Modelling and X-ray Total Scattering Study_ , Ph.D. thesis, University of Birmingham (2016).
  * Lomachuk  _et al._ [2020] Y. V. Lomachuk, D. A. Maltsev, N. S. Mosyagin, L. V. Skripnikov, R. V. Bogdanov, and A. V. Titov, Phys. Chem. Chem. Phys. 22, 17922 (2020).
  * Palma-Ramírez  _et al._ [2015] D. Palma-Ramírez, M. A. Domínguez-Crespo, A. M. Torres-Huerta, H. Dorantes-Rosales, E. Ramírez-Meneses, and E. Rodríguez, J. Alloys Compd. 643, S209 (2015).
  * NIS [2022] (2022), Standardization of 229Th (SRM 4328d), https://www.nist.gov/pml/radiation-physics/standardization-229th-srm-4328d.
  * Essex  _et al._ [2018] R. M. Essex, J. L. Mann, R. W. Williams, W. S. Kinman, A. Hubert, M. E. Bennett, and A. Gourgiotis, Appl. Radiat. Isot. 134, 23 (2018).
  * Hogle  _et al._ [2016] S. Hogle, R. A. Boll, K. Murphy, D. Denton, A. Owens, T. J. Haverlock, M. Garland, and S. Mirzadeh, Appl. Radiat. Isot. 114, 19 (2016).
  * Klinkenberg and Lang [1949] P. F. A. Klinkenberg and R. J. Lang, Physica 15, 774 (1949).
  * van Pieterson  _et al._ [2002] L. van Pieterson, M. F. Reid, R. T. Wegh, S. Soverna, and A. Meijerink, Phys. Rev. B 65, 045113 (2002).
  * Oleynichenko  _et al._ [2023] A. V. Oleynichenko, Y. V. Lomachuk, D. A. Maltsev, N. S. Mosyagin, V. M. Shakhova, A. V. Zaitsevskii, and A. V. Titov, to be published (2023).


* [ADVC16] Giorgio Audrito, Ferruccio Damiani, Mirko Viroli, and Roberto Casadei.  Run-time management of computation domains in field calculus.  In 1st International Workshops on Foundations and Applications of Self* Systems (FAS*W), pages 192–197. IEEE, 2016.
  * [ARGL+07] Michael P. Ashley-Rollman, Seth Copen Goldstein, Peter Lee, Todd C. Mowry, and Padmanabhan Pillai.  Meld: A declarative approach to programming ensembles.  In IEEE International Conference on Intelligent Robots and Systems (IROS ’07), pages 2794–2800, 2007.
  * [AVD+19] Giorgio Audrito, Mirko Viroli, Ferruccio Damiani, Danilo Pianini, and Jacob Beal.  A higher-order calculus of computational fields.  ACM Transactions on Computational Logic (TOCL), 20(1):5:1–5:55, 2019.
  * [BB06] Jacob Beal and Jonathan Bachrach.  Infrastructure for engineered emergence in sensor/actuator networks.  IEEE Intelligent Systems, 21:10–19, March/April 2006.
  * [BDU+13] Jacob Beal, Stefan Dulman, Kyle Usbeck, Mirko Viroli, and Nikolaus Correll.  Organizing the aggregate: Languages for spatial computing.  In Formal and Practical Aspects of Domain-Specific Languages: Recent Developments, chapter 16, pages 436–501. IGI Global, 2013.
  * [BPV15] Jacob Beal, Danilo Pianini, and Mirko Viroli.  Aggregate programming for the Internet of Things.  IEEE Computer, 48(9), 2015.
  * [But02] William Butera.  Programming a Paintable Computer.  PhD thesis, MIT, Cambridge, USA, 2002.
  * [BVPD17] Jacob Beal, Mirko Viroli, Danilo Pianini, and Ferruccio Damiani.  Self-adaptation to device distribution in the Internet of Things.  ACM Transactions on Autonomous and Adaptive Systems (TAAS), 12(3):12:1–12:29, 2017.
  * [CGG+05] Carlo Curino, Matteo Giani, Marco Giorgetta, Alessandro Giusti, Amy L. Murphy, and Gian Pietro Picco.  Mobile data collection in sensor networks: The tinylime middleware.  Elsevier Pervasive and Mobile Computing Journal, 4:446–469, 2005\.
  * [Chu32] Alonzo Church.  A set of postulates for the foundation of logic.  Annals of Mathematics, 33(2):346–366, 1932.
  * [CN03] Lauren Clement and Radhika Nagpal.  Self-assembly and self-repairing topologies.  In Workshop on Adaptability in Multi-Agent Systems, RoboCup Australian Open, 2003.
  * [Coo99] Daniel Coore.  Botanical Computing: A Developmental Approach to Generating Inter connect Topologies on an Amorphous Computer.  PhD thesis, MIT, Cambridge, MA, USA, 1999.
  * [DG08] Jeffrey Dean and Sanjay Ghemawat.  Mapreduce: simplified data processing on large clusters.  Communications of the ACM, 51(1):107–113, 2008.
  * [FMSM+13] Jose Luis Fernandez-Marquez, Giovanna Di Marzo Serugendo, Sara Montagna, Mirko Viroli, and Josep Lluís Arcos.  Description and composition of bio-inspired design patterns: a complete overview.  Natural Computing, 12(1):43–67, 2013.
  * [FPBV17] Matteo Francia, Danilo Pianini, Jacob Beal, and Mirko Viroli.  Towards a foundational api for resilient distributed systems design.  In 2017 IEEE 2nd International Workshops on Foundations and Applications of Self* Systems (FAS* W), pages 27–32. IEEE, 2017.
  * [GGG05] Ramakrishna Gummadi, Omprakash Gnawali, and Ramesh Govindan.  Macro-programming wireless sensor networks using kairos.  In Distributed Computing in Sensor Systems (DCOSS), pages 126–140, 2005.
  * [GGMP02] Jean-Louis Giavitto, Christophe Godin, Olivier Michel, and Przemyslaw Prusinkiewicz.  Computational models for integrative and developmental biology.  Technical Report 72-2002, U. d’Evry, LaMI, 2002.
  * [GMCS05] Jean-Louis Giavitto, Olivier Michel, Julien Cohen, and Antoine Spicher.  Computations in space and space in computations.  In Unconventional Programming Paradigms, volume 3566 of Lecture Notes in Computer Science, pages 137–152. Springer, Berlin, 2005.
  * [HH17] S. Hoyer and J. Hamman.  xarray: N-D labeled arrays and datasets in Python.  Journal of Open Research Software, 5(1), 2017.
  * [Hun07] J. D. Hunter.  Matplotlib: A 2d graphics environment.  Computing In Science & Engineering, 9(3):90–95, 2007.
  * [HW08] M. Haklay and P. Weber.  OpenStreetMap: User-generated street maps.  IEEE Pervasive Computing, 7(4):12–18, oct 2008.
  * [IPW01] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler.  Featherweight Java: A minimal core calculus for Java and GJ.  ACM Transactions on Programming Languages and Systems, 23(3), 2001\.
  * [Kon03] Attila Kondacs.  Biologically-inspired self-assembly of 2d shapes, using global-to-local compilation.  In International Joint Conference on Artificial Intelligence (IJCAI), pages 633–638. Morgan Kaufmann Publishers Inc., 2003.
  * [Lam78] Leslie Lamport.  Time, clocks, and the ordering of events in a distributed system.  Commun. ACM, 21(7):558–565, 1978.
  * [LLM17] Alberto Lluch-Lafuente, Michele Loreti, and Ugo Montanari.  Asynchronous distributed execution of fixpoint-based computational fields.  Logical Methods in Computer Science, 13(1), 2017.
  * [LMMD88] C. Lasser, J.P. Massar, J. Miney, and L. Dayton.  Starlisp Reference Manual.  Thinking Machines Corporation, 1988.
  * [MFHH02] Samuel Madden, Michael J. Franklin, Joseph M. Hellerstein, and Wei Hong.  TAG: A Tiny AGgregation Service for Ad-hoc Sensor Networks.  SIGOPS Oper. Syst. Rev., 36:131–146, 2002.
  * [MZ09] Marco Mamei and Franco Zambonelli.  Programming pervasive and mobile computing applications: The tota approach.  ACM Transactions on Software Engineering Methodologies (TOSEM), 18(4):1–56, 2009.
  * [Nag01] Radhika Nagpal.  Programmable Self-Assembly: Constructing Global Shape using Biologically-inspired Local Interactions and Origami Mathematics.  PhD thesis, MIT, Cambridge, MA, USA, 2001.
  * [NW04] Ryan Newton and Matt Welsh.  Region streams: Functional macroprogramming for sensor networks.  In Workshop on Data Management for Sensor Networks, DMSN ’04, pages 78–87. ACM, 2004.
  * [PDB+19] Aaron Paulos, Soura Dasgupta, Jacob Beal, Yuanqiu Mo, Khoi Hoang, Lyles J Bryan, Partha Pal, Richard Schantz, Jon Schewe, Ramesh Sitaraman, et al.  A framework for self-adaptive dispersal of computing services.  In 2019 IEEE 4th International Workshops on Foundations and Applications of Self* Systems (FAS* W), pages 98–103. IEEE, 2019.
  * [PMV13] Danilo Pianini, Sara Montagna, and Mirko Viroli.  Chemical-oriented simulation of computational systems with ALCHEMIST.  J. Simulation, 7(3):202–215, 2013.
  * [PVB15] Danilo Pianini, Mirko Viroli, and Jacob Beal.  Protelis: Practical aggregate programming.  In ACM Symposium on Applied Computing 2015, pages 1846–1853, April 2015.
  * [ST20] Swarm tactics: A collection of technologies for developing, simulating and executing swarm tactics at scale.  http://www.swarmtactics.com/, 2020.  Accessed: April 3, 2020.
  * [VAB+18] Mirko Viroli, Giorgio Audrito, Jacob Beal, Ferruccio Damiani, and Danilo Pianini.  Engineering resilient collective adaptive systems by self-stabilisation.  ACM Transactions on Modelling and Computer Simulation (TOMACS), 28(2):16:1–16:28, 2018.
  * [Val90] Leslie G Valiant.  A bridging model for parallel computation.  Communications of the ACM, 33(8):103–111, 1990.
  * [VBD+19] Mirko Viroli, Jacob Beal, Ferruccio Damiani, Giorgio Audrito, Roberto Casadei, and Danilo Pianini.  From distributed coordination to field calculus and aggregate computing.  Journal of Logical and Algebraic Methods in Programming, 109, 2019\.  Article 100486.
  * [VPB12] Mirko Viroli, Danilo Pianini, and Jacob Beal.  Linda in space-time: an adaptive coordination model for mobile ad-hoc environments.  In Marjan Sirjani, editor, Coordination Languages and Models, volume 7274 of LNCS, pages 212–229. Springer-Verlag, June 2012.  Proceedings of the 14th Conference of Coordination Models and Languages (Coordination 2012),Stockholm (Sweden), 14-15 June.
  * [VPM+15] Mirko Viroli, Danilo Pianini, Sara Montagna, Graeme Stevenson, and Franco Zambonelli.  A coordination model of pervasive service ecosystems.  Science of Computer Programming, 110:3 – 22, 2015.
  * [WSBC04] Kamin Whitehouse, Cory Sharp, Eric Brewer, and David Culler.  Hood: a neighborhood abstraction for sensor networks.  In Proceedings of the 2nd international conference on Mobile systems, applications, and services. ACM Press, 2004.
  * [Yam07] Daniel Yamins.  A Theory of Local-to-Global Algorithms for One-Dimensional Spatial Multi-Agent Systems.  PhD thesis, Harvard, Cambridge, MA, USA, 2007.
  * [YG02] Yong Yao and Johannes Gehrke.  The cougar approach to in-network query processing in sensor networks.  SIGMOD Record, 31:9–18, 2002.

##  Appendix A Proof of TCNS Completeness

In this section, we prove that the TCNS is able to capture the message passing
details of any augmented event structure.

Restatement of Theorem 2 (TCNS Completeness). _Let $\mathbf{E}=\langle
E,\rightsquigarrow,<,d\rangle$ be an augmented event structure. Then there
exist (infinitely many) system evolutions following $\mathbf{E}$._

######  Proof A.1.

Define a set $T=\left\\{\epsilon^{c}\mid~{}\epsilon\in
E\right\\}\cup\left\\{\epsilon^{s}\mid~{}\epsilon\in E\right\\}$, including
two elements $\epsilon^{c},\epsilon^{s}$ for every event $\epsilon$
(representing the _computation_ and _send_ phase of the event). Define
$\rightsquigarrow$ on $T$ as:

  1. (1)

$\epsilon_{1}^{s}\rightsquigarrow\epsilon_{2}^{c}$ for each pair of neighbour
events $\epsilon_{1}\rightsquigarrow\epsilon_{2}$;

  2. (2)

$\epsilon_{1}^{c}\rightsquigarrow\epsilon_{2}^{s}$ for each pair of time-
dependent events $\epsilon_{1}\dashrightarrow\epsilon_{2}$;121212We recall
that $\epsilon_{1}\dashrightarrow\epsilon_{2}$ iff
$\epsilon_{2}\rightsquigarrow\operatorname{next}(\epsilon_{1})$ and
$\epsilon_{2}\not\rightsquigarrow\epsilon_{1}$ (c.f. Definition 2.1).

  3. (3)

$\epsilon^{c}\rightsquigarrow\epsilon^{s}$ for each event $\epsilon\in E$.

First, we prove that the $\rightsquigarrow$ relation on $T$ is acyclic due to
the _immediacy_ property. Notice that $\rightsquigarrow$ always alternates
between _computation_ and _send_ elements of $T$, and in a chain of
$\rightsquigarrow$ every other transition must be of type (1). Suppose then by
contradiction that
$\epsilon_{1}^{s}\rightsquigarrow\epsilon_{2}^{c}\rightsquigarrow\ldots\rightsquigarrow\epsilon_{2n}^{c}\rightsquigarrow\epsilon_{1}^{s}$
is a cycle in $T$. If no transition of type (2) is present, the cycle in $T$
corresponds to a cycle
$\epsilon_{2}\rightsquigarrow\epsilon_{4}\rightsquigarrow\ldots\rightsquigarrow\epsilon_{2n}\rightsquigarrow\epsilon_{2}$
in $E$ which is a contradiction. Then some transitions of type (2) must be
present: assume they are
$\epsilon^{c}_{2k_{i}}\rightsquigarrow\epsilon^{s}_{2k_{i}+1}$ corresponding
to $\epsilon_{2k_{i}}\dashrightarrow\epsilon_{2k_{i}+1}$ for $i\leq m$ and
$m\leq n$, $k_{i}\leq n$ increasing. Then
$\epsilon^{s}_{2k_{i}+1}\rightsquigarrow\ldots\rightsquigarrow\epsilon^{c}_{2k_{i+1}}$
corresponds to a chain
$\epsilon_{2k_{i}+1}\rightsquigarrow\ldots\rightsquigarrow\epsilon_{2k_{i+1}}$
in $E$, hence in particular $\epsilon^{s}_{2k_{i}+1}<\epsilon^{c}_{2k_{i+1}}$.
Thus
$\epsilon_{2k_{1}}\dashrightarrow\epsilon_{2k_{1}+1}<\epsilon_{2k_{2}}\dashrightarrow\ldots<\epsilon_{2k_{1}}$
is a cyclic sequence contradicting _immediacy_ , concluding the proof of the
claim that $\rightsquigarrow$ is acyclic on $T$.

Since $\rightsquigarrow$ is acyclic on $T$, there exists at least one ordering
of $T=\langle\epsilon_{1}^{x_{1}},\ldots,\epsilon_{\ell}^{x_{\ell}}\rangle$
compatible with $\rightsquigarrow$, i.e. such that
$\epsilon_{i}^{x_{i}}\rightsquigarrow\epsilon_{j}^{x_{j}}\Rightarrow i<j$.
Define by induction a system evolution $\mathcal{S}_{i}$ for $i\leq\ell$
translating the elements of $T$ (in order), starting from the empty system
evolution without transitions
$\mathcal{S}_{0}=\langle\emptyset,\emptyset;\emptyset,\emptyset\rangle$.

Consider a step $i\leq\ell$ and let $\delta_{i}=d(\epsilon_{i})$. If $x_{i}=c$
(we are at a _computation_ element of $T$), add the following two transitions
$\mathcal{S}_{i}=\mathcal{S}_{i-1}\xrightarrow{\textit{env}}N^{\prime}\xrightarrow{\delta_{i}+}N^{\prime\prime}$:

  * •

first, an env transition inserting $\delta_{i}$ into the domain of the final
system configuration in $\mathcal{S}_{i-1}$ (if not already present);

  * •

then, a $\delta_{i}+$ transition representing the computation, where the
filter $F$ clears out from the value-tree environment $\Psi(\delta_{i})$ the
value trees corresponding to devices not in
$X=\left\\{d(\epsilon^{\prime})\mid~{}\epsilon^{\prime}\rightsquigarrow\epsilon_{i}\right\\}$.

If $x_{i}=s$ (we are at a _send_ element of $T$), add the following three
transitions to the system
$\mathcal{S}_{i}=\mathcal{S}_{i-1}\xrightarrow{\textit{env}}N^{\prime}\xrightarrow{\delta_{i}-}N^{\prime\prime}\xrightarrow{\textit{env}}N^{\prime\prime\prime}$:

  * •

first, an env transition setting $\tau(\delta_{i})$ to
$Y=\left\\{d(\epsilon^{\prime})\mid~{}\epsilon_{i}\rightsquigarrow\epsilon^{\prime}\right\\}$,
possibly adding devices in $Y$ to the domain of the system configuration if
not already present;

  * •

secondly, a $\delta_{i}-$ transition;

  * •

finally, another env transition, which removes $\delta_{i}$ from the domain of
the system configuration if $\operatorname{next}(\epsilon_{i})$ does not
exist, or it does nothing if $\operatorname{next}(\epsilon_{i})$ exists.

Then, the system evolution $\mathcal{S}_{\ell}$ follows $\mathbf{E}$ (c.f.
Definition 3.2). Notice that many system evolutions may follow $\mathbf{E}$:
besides the existence of many different linearisations of $T$ according to
$\rightsquigarrow$, env transitions can be added in an unbounded number of
ways.

##  Appendix B Proof of Self-Stabilisation

In this section, we prove Theorem 8. First, we prove the result for the
minimising pattern (Lemma 9), since it is technically more involved than the
proof for the remainder of the fragment. We then prove a stronger form of the
desired result (Lemma 10) more suited for inductive reasoning, which in turn
implies Theorem 8.

Given a closed self-stabilising expression $\mathtt{s}$, we denote with
$\mathcal{}\llbracket\mathtt{s}\rrbracket=\mathrm{\Psi}=\overline{\delta}\mapsto\overline{\mathtt{v}}$
the self-stabilising limit value of this expression in a given network graph
$\mathbf{G}$ (c.f. Definition 4.5), attained for every system evolution
$\mathcal{S}$ of a network following an $\mathbf{E}$ with limit $\mathbf{G}$.
Let:

$\displaystyle\mathtt{s}^{r}_{\text{min}}=\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})$
$\displaystyle\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{R}}(\mathtt{minHoodLoc}(\mathtt{f}^{\mathsf{MP}}(\mathtt{nbr}\\{\mathtt{x}\\},\overline{\mathtt{s}}^{r}),\mathtt{s}^{r}),\mathtt{x},\overline{\mathtt{e}})\\}$
$\displaystyle\mathtt{s}^{s}_{\text{min}}=\mathtt{share}(\mathtt{e})\\{(\mathtt{x})$
$\displaystyle\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{R}}(\mathtt{minHoodLoc}(\mathtt{f}^{\mathsf{MP}}(\mathtt{x},\overline{\mathtt{s}}^{s}),\mathtt{s}^{s}),\mathtt{localHood}(\mathtt{x}),\overline{\mathtt{e}})\\}$

be corresponding minimising patterns such that
$\mathcal{}\llbracket\overline{\mathtt{s}}^{r}\rrbracket=\mathcal{}\llbracket\overline{\mathtt{s}}^{s}\rrbracket=\overline{\mathrm{\Psi}}$,
$\mathcal{}\llbracket\mathtt{s}^{r}\rrbracket=\mathcal{}\llbracket\mathtt{s}^{s}\rrbracket=\mathrm{\Psi}$.
Let $P=\overline{\delta}$ be a path in the network (a sequence of pairwise
connected devices), and define its _weight_ as the result of picking the
eventual value $\ell_{1}=\mathrm{\Psi}(\delta_{1})$ of $\mathtt{s}^{r}$ in the
first device $\delta_{1}$, and repeatedly passing it to subsequent devices
through the monotonic progressive function, so that
$\ell_{i+1}=\mathtt{f}^{\mathsf{MP}}(\ell_{i},\overline{\mathtt{v}})$ where
$\overline{\mathtt{v}}$ is the result of projecting fields in
$\overline{\mathrm{\Psi}}(\delta_{i+1})$ to their $\delta_{i}$ component
(leaving local values untouched). Notice that the weight is well-defined since
function $\mathtt{f}^{\mathsf{MP}}$ is required to be stateless. Finally, let
$\mathrm{\Psi}_{\text{out}}$ be such that
$\mathrm{\Psi}_{\text{out}}(\delta)=\ell_{\delta}$ is the minimum weight for a
path $P$ ending in $\delta$.

######  Lemma 9.

Let $\mathtt{s}^{r}_{\text{min}}$, $\mathtt{s}^{s}_{\text{min}}$ be
corresponding minimising patterns, whose sub-expressions stabilise within
$n^{r}$, $n^{s}$ full rounds of execution (respectively) with $n^{r}\geq
n^{s}$. Then they both stabilise to $\mathrm{\Psi}_{\text{out}}$, with a bound
on the number of full rounds of execution which is greater for
$\mathtt{s}^{r}_{\text{min}}$ than for $\mathtt{s}^{s}_{\text{min}}$.

######  Proof B.1.

Let $\ell_{\delta}$ be the minimal weight for a path $P$ ending in $\delta$,
and let $\delta^{0},\delta^{1},\ldots$ be the list of all devices $\delta$
ordered by increasing $\ell_{\delta}$. Notice that the path $P$ of minimal
weight $\ell_{\delta^{i}}$ for device $i$ can only pass through nodes such
that $\ell_{\delta^{j}}\leq\ell_{\delta^{i}}$ (thus s.t. $j<i$). In fact,
whenever a path $P$ contains a node $j$ the weight of its prefix until $j$ is
at least $\ell_{\delta^{j}}$; thus any longer prefix has weight strictly
greater than $\ell_{\delta^{j}}$ since $\mathtt{f}^{\mathsf{MP}}$ is
progressive.

Let $\mathcal{S}$ be a system evolution following $\mathbf{E}=\langle
E,\rightsquigarrow,<,d\rangle$ with limit $\mathbf{G}$. We now prove by
complete induction on $i$ that after a certain number of full rounds of
execution $n{}^{r}_{i}$, $n{}^{s}_{i}$ expressions
$\mathtt{s}^{r}_{\text{min}}$, $\mathtt{s}^{s}_{\text{min}}$ stabilise to
$\ell_{\delta^{i}}$ in device $\delta^{i}$ and assume values
$\geq\ell_{\delta^{i}}$ in devices $\delta^{j}$ with $j\geq i$.

By inductive hypothesis, assume that devices $\delta^{j}$ with $j<i$ are all
self-stabilised from a certain number of full rounds of execution
$n{}^{r}_{i-1}$, $n{}^{s}_{i-1}$. Thus, their limit values are available to
neighbours after $n^{r}_{i-1}+2$, $n^{s}_{i-1}+1$ full rounds of execution
respectively. Consider the evaluation of the expressions
$\mathtt{s}^{r}_{\text{min}}$, $\mathtt{s}^{s}_{\text{min}}$ in a device
$\delta^{k}$ with $k\geq i$. Since the local argument $\ell$ of minHoodLoc is
also the weight of the single-node path $P=\delta^{k}$, it has to be at least
$\ell\geq\ell_{\delta^{k}}\geq\ell_{\delta^{i}}$. Similarly, the restriction
$\phi^{\prime}$ of the field argument $\phi$ of minHoodLoc to devices
$\delta^{j}$ with $j<i$ has to be at least
$\phi^{\prime}\geq\ell_{\delta^{k}}\geq\ell_{\delta^{i}}$ since it corresponds
to weights of (not necessarily minimal) paths $P$ ending in $\delta^{k}$
(obtained by extending a minimal path for a device $\delta^{j}$ with $j<i$
with the additional node $\delta^{k}$). Finally, the complementary restriction
$\phi^{\prime\prime}$ of $\phi$ to devices $\delta^{j}$ with $j\geq i$ is
strictly greater than the minimum value for whole
$\mathtt{s}^{r}_{\text{min}}$, $\mathtt{s}^{s}_{\text{min}}$ expression among
all devices $\delta^{j}$ with $j\geq i$ (delayed by one round for
$\mathtt{rep}+\mathtt{share}$), since $\mathtt{f}^{\mathsf{MP}}$ is
progressive.

It follows that as long as the minimum value for the whole expressions among
non-stable devices is lower than $\ell_{\delta^{i}}$, the result of the
minHoodLoc subexpression is _strictly greater_ than this minimum value. The
same holds for the overall value, since it is obtained by combining the output
of minHoodLoc with the previous value for $\mathtt{x}$ through the rising
function $\mathtt{f}^{\mathsf{R}}$, and a rising function has to be equal to
the first argument (the minHoodLoc result strictly greater than the minimum),
or $\vartriangleright$ than the second. In the latter case, it also needs to
be greater or equal to the first argument (again, strictly greater than the
minimum) or strictly greater than the second argument131313It cannot be equal
to the second argument, as it is $\vartriangleright$-greater than it. (not
below the minimum value).

Thus, every full round of execution (two full rounds for
$\mathtt{rep}+\mathtt{nbr}$, in order to allow value changes to be received)
the minimum value among non-stable devices has to increase, until it
eventually surpasses $\ell_{\delta^{i}}$ since $<$ is noetherian. This happens
within at most $n^{r}_{i-1}+2x$, $n^{s}_{i-1}+x$ full rounds of execution
respectively, where $x$ is the length of the longest increasing sequence
between $\ell_{\delta^{i-1}}$ and $\ell_{\delta^{i}}$ (longest sequence up to
$\ell_{\delta^{i}}$ if $i=0$). From that point on, that minimum cannot drop
below $\ell_{\delta^{i}}$, and the output of minHoodLoc in $\delta^{i}$
stabilises to $\ell_{\delta^{i}}$. In fact, if $P$ is a path of minimum weight
for $\delta^{i}$, then either:

  * •

$P=\delta^{i}$, so that $\ell_{\delta^{i}}$ is exactly the local argument of
the minHoodLoc operator, hence also the output of it (since the field argument
is greater than $\ell_{\delta^{i}}$).

  * •

$P=Q,\delta^{i}$ where $Q$ ends in $\delta^{j}$ with $j<i$. Since
$\mathtt{f}^{\mathsf{MP}}$ is monotonic non-decreasing, the weight of
$Q^{\prime},\delta^{i}$ (where $Q^{\prime}$ is minimal for $\delta^{j}$) is
not greater than that of $P$; in other words,
$P^{\prime}=Q^{\prime},\delta^{i}$ is also a path of minimum weight. It
follows that $\phi(\delta^{j})$ (where $\phi$ is the field argument of the
minHoodLoc operator) is exactly $\ell_{\delta^{i}}$.

Since the order $\vartriangleleft$ is noetherian, the rising function on
$\delta^{i}$ has to select its first argument in a number of rounds $y$ at
most equal to the longest increasing sequence from $\ell_{\delta^{i}}$. Thus,
it will select the output of the minHoodLoc subexpression, which is
$\ell_{\delta^{i}}$, after $n^{r}_{i-1}+2x+y$, $n^{s}_{i-1}+x+y$ full rounds
of execution. From that point on, the minimising expression will have self-
stabilised on device $\delta^{i}$ to $\ell_{\delta^{i}}$, and every device
$\delta^{j}$ with $j\geq i$ will attain values $\geq\ell_{\delta^{i}}$,
concluding the inductive step and the proof.

Let $\mathrm{\Psi}$ be a computational field. We write
$\mathtt{s}[\mathtt{x}:=\mathrm{\Psi}]$ to indicate an aggregate process in
which each device is computing a possibly different substitution
$\mathtt{s}[\mathtt{x}:=\mathrm{\Psi}(\delta)]$ of the same expression.

######  Lemma 10.

Assume that every built-in operator is self-stabilising. Let $\mathtt{s}^{r}$
be an expression in the self-stabilising fragment of [VAB+18],
$\mathtt{s}^{s}$ its non-equivalent translation with $\mathtt{share}$, and
$\overline{\mathrm{\Psi}}$ be a sequence of computational fields on
$\mathbf{G}$ of the same length as the free variables $\overline{\mathtt{x}}$
occurring in $\mathtt{s}^{r}$, $\mathtt{s}^{s}$. Then
$\mathtt{s}^{r}[\overline{\mathtt{x}}:=\overline{\mathrm{\Psi}}]$,
$\mathtt{s}^{s}[\overline{\mathtt{x}}:=\overline{\mathrm{\Psi}}]$ self-
stabilise to the same limit, and the second does so with a smaller bound on
the number of full rounds of execution.

######  Proof B.2.

Let $\mathcal{S}$ be a system evolution following $\mathbf{E}=\langle
E,\rightsquigarrow,<,d\rangle$ with limit $\mathbf{G}$. The proof proceeds by
induction on the syntax of expressions and programs. The given expressions
$\mathtt{s}^{r}$, $\mathtt{s}^{s}$ could be:

  * •

A variable $\mathtt{x}_{i}$, so that
$\mathtt{s}^{r}[\overline{\mathtt{x}}:=\overline{\mathrm{\Psi}}]=\mathtt{s}^{s}[\overline{\mathtt{x}}:=\overline{\mathrm{\Psi}}]=\mathrm{\Psi}_{i}$
are already self-stabilised and identical.

  * •

A value $\mathtt{v}$, so that
$\mathtt{s}^{r}[\overline{\mathtt{x}}:=\overline{\mathrm{\Psi}}]=\mathtt{s}^{s}[\overline{\mathtt{x}}:=\overline{\mathrm{\Psi}}]=\mathtt{v}$
are already self-stabilised and identical.

  * •

A $\mathtt{let}$-expression
$\mathtt{let}\;\mathtt{x}=\mathtt{s}^{r}_{1}\;\mathtt{in}\;\mathtt{s}^{r}_{2}$,
$\mathtt{let}\;\mathtt{x}=\mathtt{s}^{s}_{1}\;\mathtt{in}\;\mathtt{s}^{s}_{2}$.
By inductive hypothesis, the sub-expressions $\mathtt{s}^{r}_{1}$,
$\mathtt{s}^{s}_{1}$ stabilise to $\mathrm{\Psi}$ within $n^{r}_{1}\geq
n^{s}_{1}$ full rounds of execution. After that,
$\mathtt{let}\;\mathtt{x}=\mathtt{s}_{1}\;\mathtt{in}\;\mathtt{s}_{2}$
evaluates to the same value as the expression
$\mathtt{s}_{2}[\mathtt{x}:=\mathrm{\Psi}]$ which is self-stabilising by
inductive hypothesis in a number of full rounds of execution $n^{r}_{2}\geq
n^{s}_{2}$. Thus, the whole $\mathtt{let}$-expression stabilises within
$n^{r}_{1}+n^{r}_{2}\geq n^{s}_{1}+n^{s}_{2}$ full rounds of execution.

  * •

A functional application $\mathtt{f}^{r}(\overline{\mathtt{s}}^{r})$,
$\mathtt{f}^{s}(\overline{\mathtt{s}}^{s})$. By inductive hypothesis, all
expressions $\overline{\mathtt{s}}^{r}$, $\overline{\mathtt{s}}^{s}$ self-
stabilise to $\overline{\mathrm{\Psi}}$ after a certain amount of full rounds
of execution (lower for $\overline{\mathtt{s}}^{s}$). After stabilisation of
the arguments, if $\mathtt{f}^{r}=\mathtt{f}^{s}=\mathtt{f}$ is a built-in
function then $\mathtt{f}(\overline{\mathtt{s}}^{r})$,
$\mathtt{f}(\overline{\mathtt{s}}^{s})$ stabilises by the assumption on built-
ins with the same number of additional full rounds of execution. Otherwise,
$\mathtt{f}^{r}(\overline{\mathtt{s}}^{r})$,
$\mathtt{f}^{s}(\overline{\mathtt{s}}^{r})$ evaluate to the same value of the
expression
$\textit{body}(\mathtt{f}^{r})[\textit{args}(\mathtt{f}^{r}):=\overline{\mathrm{\Psi}}]$
(resp. with $\mathtt{f}^{s}$) which are self-stabilising in a number of full
rounds of executions lower for $\mathtt{f}^{s}$ by inductive hypothesis.

  * •

A conditional
$\mathtt{s}^{r}=\mathtt{if}(\mathtt{s}^{r}_{1})\\{\mathtt{s}^{r}_{2}\\}\\{\mathtt{s}^{r}_{3}\\}$,
$\mathtt{s}^{s}=\mathtt{if}(\mathtt{s}^{s}_{1})\\{\mathtt{s}^{s}_{2}\\}\\{\mathtt{s}^{s}_{3}\\}$.
By inductive hypothesis, expressions $\mathtt{s}^{r}_{1}$,
$\mathtt{s}^{s}_{1}$ self-stabilise to $\mathrm{\Psi}_{\textit{guard}}$ (with
fewer rounds for share). Let $\mathbf{G}{}_{\mathtt{true}}$ be the sub-graph
consisting of devices $\delta$ such that
$\mathrm{\Psi}_{\textit{guard}}(\delta)=\mathtt{true}$, and analogously
$\mathbf{G}{}_{\mathtt{false}}$. Assume that $\mathtt{s}^{r}_{2}$,
$\mathtt{s}^{s}_{2}$ self-stabilise to $\mathrm{\Psi}_{\mathtt{true}}$ in
$\mathbf{G}{}_{\mathtt{true}}$ and $\mathtt{s}^{r}_{3}$, $\mathtt{s}^{s}_{3}$
to $\mathrm{\Psi}_{\mathtt{false}}$ in $\mathbf{G}{}_{\mathtt{false}}$ (with
fewer rounds for share). Since a conditional is computed in isolation in the
above defined sub-environments, $\mathtt{s}^{r}$, $\mathtt{s}^{s}$ self-
stabilise to
$\mathrm{\Psi}=\mathrm{\Psi}_{\mathtt{true}}\cup\mathrm{\Psi}_{\mathtt{false}}$
(with fewer rounds for share).

  * •

A neighbourhood field construction $\mathtt{nbr}\\{\mathtt{s}^{r}\\}$,
$\mathtt{nbr}\\{\mathtt{s}^{s}\\}$. By inductive hypothesis, expressions
$\mathtt{s}^{r}$, $\mathtt{s}^{s}$ self-stabilise to $\mathrm{\Psi}$ after
some rounds of computation (fewer for share). Then
$\mathtt{nbr}\\{\mathtt{s}^{r}\\}$, $\mathtt{nbr}\\{\mathtt{s}^{s}\\}$ self-
stabilise to the corresponding $\mathrm{\Psi}^{\prime}$ after one additional
full round of execution, where $\mathrm{\Psi}^{\prime}(\delta)$ is
$\mathrm{\Psi}$ restricted to $\mathcal{N}(\delta)$.

  * •

A converging pattern $\mathtt{s}^{r}_{c}$, $\mathtt{s}^{s}_{c}$:

$\displaystyle\mathtt{s}^{r}_{c}=\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})$
$\displaystyle\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{C}}(\mathtt{nbr}\\{\mathtt{x}\\},\mathtt{nbr}\\{\mathtt{s}^{r}\\},\overline{\mathtt{e}})\\}$
$\displaystyle\mathtt{s}^{s}_{c}=\mathtt{share}(\mathtt{e})\\{(\mathtt{x})$
$\displaystyle\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{\mathsf{C}}(\mathtt{x},\mathtt{nbr}\\{\mathtt{s}^{s}\\},\overline{\mathtt{e}})\\}$

By inductive hypothesis, $\mathtt{s}^{r}$, $\mathtt{s}^{s}$ self-stabilise
(the latter with fewer rounds) to a same $\mathrm{\Psi}$. Given any index
$n{}$, let $d^{r}_{n{}}$, $d^{s}_{n{}}$ be the maximum distances
$\mathtt{s}^{r}_{c}-\mathrm{\Psi}(d(\epsilon){})$,
$\mathtt{s}^{s}_{c}-\mathrm{\Psi}(d(\epsilon){})$ realised during events
$\epsilon$ of the $n$-th full round of execution.

We prove that $d^{s}_{n}$ is strictly decreasing with $n$, while
$d^{r}_{n}\geq d^{r}_{n-1}$, $d^{r}_{n}>d^{r}_{n+2}$ strictly decreases every
two rounds. Since distances are computed on a well-founded set, it will follow
that they will became zero for a sufficiently large $n$ (smaller for share),
thus $\mathtt{s}_{c}^{r}$, $\mathtt{s}_{c}^{s}$ stabilise as well to the same
$\mathrm{\Psi}$ (with fewer rounds for share).

Consider an event on the $n$-th full round of execution. Thus, neighbours
events belong to rounds of execution $\geq n-1$, hence their distance with
$\mathrm{\Psi}$ is at most $d^{r}_{n-2}$, $d^{s}_{n-1}$ respectively. It
follows that the output of the converging function $\mathtt{f}^{\mathsf{C}}$
must be strictly closer to $\mathrm{\Psi}$ than $d^{r}_{n-2}$, $d^{s}_{n-1}$
respectively, concluding the proof.

  * •

An acyclic pattern $\mathtt{s}^{r}_{a}$, $\mathtt{s}^{s}_{a}$:

$\displaystyle\mathtt{s}^{r}_{a}=\mathtt{rep}(\mathtt{e})\\{(\mathtt{x})$
$\displaystyle\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{r}(\mathtt{mux}(\mathtt{nbrlt}(\mathtt{s}^{r}_{p}),\mathtt{nbr}\\{\mathtt{x}\\},\mathtt{s}^{r}),\overline{\mathtt{s}}^{r})\\}$
$\displaystyle\mathtt{s}^{s}_{a}=\mathtt{share}(\mathtt{e})\\{(\mathtt{x})$
$\displaystyle\stackrel{{\scriptstyle}}{{\mathrm{\texttt{=>}}}}{}\mathtt{f}^{s}(\mathtt{mux}(\mathtt{nbrlt}(\mathtt{s}^{s}_{p}),\mathtt{x},\mathtt{s}^{s}),\overline{\mathtt{s}}^{s})\\}$

By inductive hypothesis, $\mathtt{s}^{r}$, $\mathtt{s}^{s}$ self-stabilise
(the latter with fewer rounds) to a same $\mathrm{\Psi}$, and similarly for
$\mathtt{s}^{r}_{p}$, $\mathtt{s}^{s}_{p}$ with $\mathrm{\Psi}_{p}$ and
$\overline{\mathtt{s}}^{r}$, $\overline{\mathtt{s}}^{s}$ with
$\overline{\mathrm{\Psi}}$.

Let $\epsilon$ be any firing in the first full round of execution (after
stabilisation of sub-expressions) of the device $\delta_{0}$ of minimal
potential $\mathrm{\Psi}_{p}(\delta_{0})$ in the network. Since
$\mathrm{\Psi}_{p}(\delta_{0})$ is minimal,
$\mathtt{nbrlt}(\mathtt{s}^{r}_{p})$, $\mathtt{nbrlt}(\mathtt{s}^{s}_{p})$ are
false and the $\mathtt{mux}$-expression reduces to $\mathtt{s}^{r}$,
$\mathtt{s}^{s}$ and the whole $\mathtt{s}^{r}_{a}$, $\mathtt{s}^{s}_{a}$ to
$\mathtt{f}^{r}(\mathtt{s}^{r},\overline{\mathtt{s}}^{r})$,
$\mathtt{f}^{s}(\mathtt{s}^{s},\overline{\mathtt{s}}^{s})$, which self-
stabilises by inductive hypothesis (with fewer rounds for share).

Let now $\epsilon$ be any firing in the first (second for $\mathtt{rep}$) full
round of execution after stabilisation of $\delta_{0}$ of the device
$\delta_{1}$ of second minimal potential $\mathrm{\Psi}_{p}(\delta_{1})$. Then
the $\mathtt{mux}$-expression in $\delta_{1}$ only (possibly) depends on the
value of the device of minimal potential, which is already self-stabilised and
available to neighbours. Thus by inductive hypothesis $\mathtt{s}^{r}_{a}$,
$\mathtt{s}^{s}_{a}$ self-stabilises also in $\delta_{1}$ (with fewer rounds
for share). By repeating the same reasoning on all devices in order of
increasing potential, we obtain a final number of rounds (smaller for share)
after which all devices have self-stabilised.

  * •

A minimising $\mathtt{rep}$: this case is proved for closed expressions in
Lemma 9, and its generalisation to open expressions is straightforward.