# Laser excitation of the 229Th nuclear isomeric transition in a solid-state
host

R. Elwell  Department of Physics and Astronomy, University of California, Los
Angeles, CA 90095, USA  Christian Schneider  Department of Physics and
Astronomy, University of California, Los Angeles, CA 90095, USA  Justin Jeet
Department of Physics and Astronomy, University of California, Los Angeles, CA
90095, USA  J. E. S. Terhune  Department of Physics and Astronomy, University
of California, Los Angeles, CA 90095, USA  H. W. T. Morgan  Department of
Chemistry and Biochemistry, University of California, Los Angeles, Los
Angeles, CA 90095, USA  A. N. Alexandrova  Department of Chemistry and
Biochemistry, University of California, Los Angeles, Los Angeles, CA 90095,
USA  H. B. Tran Tan  Department of Physics, University of Nevada, Reno, Nevada
89557, USA  Los Alamos National Laboratory, P.O. Box 1663, Los Alamos, New
Mexico 87545, USA  Andrei Derevianko  Department of Physics, University of
Nevada, Reno, Nevada 89557, USA  Eric R. Hudson  Department of Physics and
Astronomy, University of California, Los Angeles, CA 90095, USA  Challenge
Institute for Quantum Computation, University of California Los Angeles, Los
Angeles, CA, USA  Center for Quantum Science and Engineering, University of
California Los Angeles, Los Angeles, CA, USA

###### Abstract

LiSrAlF6 crystals doped with 229Th are used in a laser-based search for the
nuclear isomeric transition. Two spectroscopic features near the nuclear
transition energy are observed. The first is a broad excitation feature that
produces red-shifted fluorescence that decays with a timescale of a few
seconds. The second is a narrow, laser-linewidth-limited spectral feature at
$148.38219(4)_{\textrm{stat}}(20)_{\textrm{sys}}$ nm
($2020407.3(5)_{\textrm{stat}}(30)_{\textrm{sys}}$ GHz) that decays with a
lifetime of $568(13)_{\textrm{stat}}(20)_{\textrm{sys}}$ s. This feature is
assigned to the excitation of the 229Th nuclear isomeric state, whose energy
is found to be $8.355733(2)_{\textrm{stat}}(10)_{\textrm{sys}}$ eV in
229Th:LiSrAlF6.

The nuclear isomeric state in the 229Th nucleus, described by the Nilsson
quantum numbers $(3/2)^{+}\left[631\right]$ has the lowest energy of all known
nuclear excited states. This extraordinary property, coupled with its expected
long lifetime, should allow access to a number of novel applications,
including construction of an optical nuclear clock that may be more robust [1]
than and/or outperform [2, 3] current technology. It is also expected to allow
the most sensitive test to date of the variation of the fundamental constants
[1, 4, 5].

While recent work has greatly improved the knowledge of the isomeric state
energy [6, 7, 8], to realize the aforementioned goals requires an energy
measurement with laser spectroscopic precision of the isomeric transition,
$(3/2)^{+}\left[631\right]\leftarrow(5/2)^{+}\left[633\right]$. It was
proposed [1] that due to the optical Mößbauer effect, a high-bandgap crystal
doped with 229Th might provide an attractive platform for performing this
spectroscopy. As a result, considerable effort has been put towards developing
high-quality 229Th-doped crystals, both by traditional methods [9, 10] and
using implantation at a radioactive beamline [11]. This led to an important
experiment at ISOLDE [11], which established that detection of a long-lived
nuclear decay ($\tau\sim 1000$ s) is possible in a crystalline host and that
the wavelength of the isomeric transition was 148.7(4) nm – parentheses
denotes the 68% confidence interval.

Here, we report the results of a laser-based search for the 229Th isomeric
nuclear transition in 229Th-doped LiSrAlF6 crystals. Using a vacuum-
ultraviolet (VUV) laser system [12], we have searched for the transition
between 147.43 nm-182.52 nm (6.793 eV-8.410 eV). We observe wideband
fluorescence from 229Th-doped crystals in the spectral region identified by
the ISOLDE experiment [11], while undoped and 232Th-doped crystals do not
exhibit similar fluorescence. This fluorescence appears to possess multiple
time scales that are of order a few seconds. We also observe a narrow, laser-
linewidth-limited spectral feature at
$148.38219(4)_{\textrm{stat}}(20)_{\textrm{sys}}$ nm, which decays with a
lifetime of $568(13)_{\textrm{stat}}(20)_{\textrm{sys}}$ s. This feature does
not appear in a 232Th-doped LiSrAlF6 crystal.

Very recently, using the approach of Ref. [1], a narrow spectroscopic feature
was observed in the laser spectroscopy of 229Th-doped CaF2 crystals at
148.3821(5) nm [13]. Since this feature did not appear in a 232Th-doped CaF2
crystal it was assigned to the 229Th isomeric transition. Such assignment
relies on the chemical identity of 232Th- and 229Th-doped crystals, which,
given that the radioactivity of 229Th may lead to formation of radiation-
induced color centers in 229Th-doped crystals, is not guaranteed – especially
given the history of the search for the isomeric transition [14, 15]. However,
given that the feature is observed in both 229Th-doped CaF2 and LiSrAlF6
crystals under different experimental conditions, it appears safe to assign it
to the 229Th nuclear isomeric transition.

To interpret these results, we present _ab initio_ crystal structure
calculations that suggest the observed short-time fluorescence could be due to
coupling of the 229Th nucleus to the electronic and phononic degrees of
freedom of the crystal. This coupling may also explain why only a fraction of
the 229Th nuclei doped into the crystal appear to contribute to the observed
narrow, isomeric transition.

The experiments reported here were conducted via monitoring the resulting
fluorescence from crystals following illumination with a VUV laser. Four
different VUV transparent LiSrAlF6 crystals were used in these experiments,
all with dimensions $\approx$ 3 mm $\times$ 3 mm $\times$ 10 mm. Two were
doped with 229Th (crystal 2.2 with 229Th density $\rho_{229}\approx
5(10^{16})$ cm-3 and crystal 3.1 with $\rho_{229}\approx 5(10^{15})$ cm-3),
one was doped with 232Th ($\rho_{232}\approx 1(10^{16})$ cm-3) to understand
any fluorescence resulting from the chemistry of Th in LiSrAlF6, and one was
an undoped LiSrAlF6 crystal to understand any fluorescence due to intrinsic
properties of the host material.

Figure 1: (a) Long timescale fluorescence from 229Th:LiSrAlF6 crystal 2.2
normalized by laser power after $\approx~{}2000$ s illumination shown over the
68% confidence interval of the ISOLDE experiment [11]. Dotted black lines
denote the mean ($\mu$) and mean plus multiples of the standard deviation
($\sigma$). Though the expected signal is roughly two-orders of magnitude
larger than what is observed, points above $\mu+2\sigma$ were denoted as
potential detection events and slated for further study. The vertical blue
dashed line denotes the location of the narrow feature observed in Fig. 3(a).
(b) Short timescale fluorescence normalized by laser power vs. excitation
energy in 229Th (2.2 in blue, 3.1 in black) and 232Th (red) LiSrAlF6 crystals.
The inset shows the region near the ISOLDE 68% confidence region (shaded).
Each of the blue data points required roughly 1 hr to collect. The drop in
signal near 8.37 eV is due to a resonance in the Xe gas used for generating
the VUV. (c) Time binned histogram of the short time fluorescence from 229Th
crystal 2.2 fitted with a two timescale exponential decay model. (d) The
likelihood contours of the two timescales found from the data in (c). Each
contour represents the [68%, 95%, 99.7%] confidence regions around
$\chi^{2}_{min}$.

VUV radiation was produced via resonance-enhanced four-wave mixing of two
pulsed dye lasers in Xe gas [12, 16]. The frequency of the first pulsed dye
laser, $\omega_{u}$, was locked to the
$5p^{6~{}1}S_{0}~{}\rightarrow~{}5p^{5}\left({}^{2}P^{\circ}_{3/2}\right)6p~{}^{2}\left[1/2\right]_{0}$
two-photon transition of Xe. The frequency of the second pulsed dye laser,
$\omega_{v}$, was scanned to produce VUV radiation in the Xe cell given by the
difference mixing relation $\omega=2\omega_{u}-\omega_{v}$. All three laser
beams then impinge on an off-axis MgF2 lens, whose chromatic dispersion is
used with downstream pinholes to spatially filter the VUV beam and pass it
towards the crystal chamber. The laser system deliveries 30 pulses per second
to the crystal with a typical VUV pulse energy of $\sim 1$ $\mu$J/pulse (see
Ref. [9, 12] for details).

The crystal under study is held in a vacuum chamber consisting of a crystal
mount, two VUV-sensitive photo-multiplier tubes (Hamamatsu R6835/R6836), and a
pneumatic shutter system to protect the PMTs from direct exposure to the VUV
laser. The PMTs are operated in a cathode-grounded configuration, and their
output waveforms recorded by a 1 Gs/s waveform digitizer (CAEN DT5751) for
subsequent post-processing. The VUV laser beam terminates on a custom VUV
energy detector. The crystal chamber is maintained with an Ar atmosphere at a
pressure of $\sim$10-2 mbar to provide high VUV transmission while minimizing
browning of optics due to hydrocarbon deposition [12].

Using this system, an experiment was performed from May 2016 to July 2019 that
was designed to search for crystal fluorescence with a lifetime of $\approx
1000$ s, as would be expected for radiative relaxation of the isomeric level
in a 229Th:LiSrAlF6 crystals [17]. For this experiment, crystal 2.2 was
illuminated by VUV radiation for roughly 2000 s, the shutters were opened
within 0.5 s, and any resulting fluorescence collected by the PMTs for roughly
1000 s.

For each data point constituting 2000 s of illumination, the VUV laser
frequency was swept 8 times over $\sim$160 GHz. Each subsequent data point was
then overlapped in frequency by $\sim$40 GHz with the previous one. This
procedure was employed to minimize the probability of failing to illuminate
the isomeric transition due to, e.g., multi-mode behavior of the pulsed dye
lasers without requiring impractical data collection times.

Figure 1(a) shows the number of detected photons after background correction
($N_{\gamma}$) normalized by the VUV laser power ($P_{L}$) over the ISOLDE-
identified 68% confidence interval [11]. The expected signal, assuming that
all doped 229Th nuclei are optically addressable, is roughly two orders of
magnitude higher than the observed level. However, by analyzing the
distribution of the detected photons, points deviating from the mean by more
than two standard deviations were flagged for further study, as described
later.

In contrast, a clear excess of detected photons can be seen in Fig. 1(b),
which shows $N_{\gamma}/P_{L}$ in the first 50 s after the laser is
extinguished as a function of excitation wavelength. This fluorescence appears
largest near the spectral region identified by the ISOLDE experiment [11].
Analysis suggests that this fluorescence possesses multiple timescales and is
reasonably fit by a two-lifetime model as shown in Fig. 1(c); the likelihood
contours for these two lifetimes are shown in Fig. 1(d).

Following this observation, several additional experiments were performed to
ascertain the origin of the short-timescale fluorescence. For these
experiments, the crystals were illuminated by the VUV laser for 60 s, the
shutters opened in 100 ms, and the resulting fluorescence observed for roughly
60 s. First, a second 229Th:LiSrAlF6 crystal (batch 3.1) was investigated to
confirm the existence of the spectral feature. The resulting fluorescence is
shown as the black line in Fig. 1(b) and follows closely the observed
fluorescence in crystal 2.2; the fluorescence exhibits a two-timescale
behavior that is indistinguishable from that of crystal 2.2. Following these
measurements, the experiment was repeated with a 232Th:LiSrAlF6 crystal (red
line). As can be seen in Fig. 1(b), the 232Th:LiSrAlF6 and 229Th:LiSrAlF6
crystals yield a similar spectroscopic feature around 8 eV, but only the
229Th:LiSrAlF6 crystals yield a significant signal near the nuclear
transition. Assuming this feature arises from nuclear excitation, we estimate
from the known 229Th density in these crystals [9] and the detection
efficiency of the system that only a portion of order 1 ppm of the doped 229Th
atoms participate in this short-timescale process. Other explanations, such a
radiation-induced color centers cannot be ruled out.

This data suggests the observed short-timescale fluorescence could have a
nuclear origin and it is therefore interesting to determine the wavelength of
emission. However, the number of emitted photons was sufficiently small ($\sim
10^{4}$ photons into $4\pi$) that it could not be analyzed with available
monochromators. Therefore, in order to determine the spectrum of the
fluorescence emitted from the highest activity 229Th:LiSrAlF6 crystal (crystal
2.2), the transmission of the fluorescence was measured through a set of band-
pass filters. An imaging system was used to collimate the collected light
before passing through the filters in order to eliminate angle effects [18].
The filtered light was then focused onto a photomultiplier tube for detection.
The VUV laser wavelength was chosen to be $\approx 147.4$ nm to maximize the
amount of fluorescence. The resulting fluorescence through various filter
configurations is plotted in Fig. 2, where the horizontal axis is the central
transmission wavelength of each configuration and the horizontal ‘error bar’
denotes the FWHM of the filter transmission (see SI). As can be seen, the
fluorescence is clearly in the VUV region as it primarily transmits through
only two filters nominally centered at 154 nm and 180 nm. To better determine
the wavelength of the emitted light, a Gaussian deconvolution procedure [19]
was used to fit a model spectrum to the data (see SI). This analysis is most
consistent with a narrow emission at $\approx 182$ nm with a long-tailed
background centered red of $280$ nm. The long-tail in the UV is expected and
has previously been understood as due to fluorescence induced by radioactive
decay of the 229Th in the crystal (see Fig. 2(b) of Ref. [9]). As will be
discussed later, the narrow VUV emission could be attributed to the isomeric
state quenched by excitation of a defect electron-hole pair in the crystal.

Figure 2: Fitted spectrum for the fluorescence from crystal 2.2 under
excitation at 147.4 nm using a Gaussian deconvultion (see SI). The black
points represent the recorded photon numbers; the vertical line represents the
statistical uncertainty while the horizontal line represents the full width at
half maximum (FWHM) of the transfer function of that particular filter
configuration. Each point is centered at the peak of the transfer function.

Following this study of the short-timescale fluorescence, we returned to the
study of the long-timescale fluorescence. The ISOLDE experiment had found that
only a few percent of the 229Th atoms implanted into the crystal contributed
to the radiative signal [11]. This suggests that some lattice sites are
quenched by coupling to the electronic structure of the crystal. Therefore, we
began a new search, optimized for detection of the isomeric transition,
assuming only a few percent of the doped 229Th atoms contributed. This search
was performed over the spectral regions within the ISOLDE region that showed
an excess of photon counts relative to their neighbors (see Fig. 1(a)). The
results of that optimized search near a region of excess photons counts in our
2019 data (see dashed blue line in Fig. 1(a)), are shown in Fig 3(a). The
total power-normalized, long-timescale fluorescence observed in this region
reveals a narrow spectral feature at
$148.38219(4)_{\textrm{stat}}(20)_{\textrm{sys}}$ nm in both crystals 2.2 and
3.1; the primary source of systematic uncertainty is wavemeter calibration
(see SI). The full width at half maximum (FWHM) of this feature is roughly 15
GHz and in agreement with a measurement of the laser linewidth. The central
wavelength of this feature is identical, within error, in both crystals 2.2
and 3.1 and to that observed in Ref. [13]. It is, thus, attributed to the
excitation of the 229Th isomeric state. From this data, we estimate that
approximately 1% (50%) of the doped 229Th nuclei in crystal 2.2 (3.1) are able
to be excited on the nuclear isomeric transition.

The measured isomeric decay lifetime is
$\tau=568(13)_{\textrm{stat}}(20)_{\textrm{sys}}$ s as shown in Fig.3(b),
where the systematic error is estimated based on long-term drifts in the PMTs
background count rates. The LiSrAlF6 index of refraction is not well-
characterized in the VUV but can be estimated as 1.485 [12], leading to an
estimate of the isomeric lifetime in vacuum of $\tau_{is}\approx
1860(43)_{\textrm{stat}}(66)_{\textrm{sys}}$ s. This inferred lifetime is
similar to that observed in 229Th:CaF2 [13] (1740(50) s), especially given
uncertainty in the indices of refraction of these crystals in the VUV, and in
agreement with that predicted in Ref. [17].

Figure 3: (a) Spectrum of the 229Th isomeric transition. The total power-
normalized photon count in 1800 s following illumination is plotted versus
excitation wavelength for crystal 2.2 (blue), 3.1 (black) and a 232Th:LiSrAlF6
crystal (red). The solid lines represent fits of a Lorentzian lineshape, which
result in statistically identical center frequencies. The linewidth of the
fitted Lorentzians are also statistically identical and consistent with the
linewidth of the VUV laser system, indicating a narrow line. (b) Observed
photon count rate versus time from crystal 3.1 alongside an decaying
exponential fit which determines the isomeric state lifetime within the
crystal to be $\tau=568(13)_{\textrm{stat}}(20)_{\textrm{sys}}$ s. A
statistically identical lifetime is observed in crystal 2.2.

To better understand these results, we performed density functional theory
(DFT) calculations using the modified Becke-Johnson [20, 21] functional to
estimate the electronic properties of the 229Th-doped crystals (see SI). Fig.
4 shows the projected density of states (PDOS) for Th in Th:LiSrAlF6, in a
$3\times 3\times 2$ supercell containing one Th atom and 2 interstitial F
atoms for charge balancing; this is the lowest-energy configuration in our
calculations (see SI). We find a manifold of the Th $5f$ states at 6.8 eV (182
nm) inside the insulator bandgap ($d_{i}$ states). This is consistent with the
observed fluorescence wavelength in Fig. 2, indicating the possibility of
nuclear decay via excitation of a valence-band electron to a $d_{i}$ state.
Subsequent photon emission via the recombination of the $d_{i}$ state with the
hole, which has moved to the top of the valence band on ps timescales typical
for non-radiative relaxation of hot holes [22], would produce the observed,
red-shifted 182 nm photons.

Such coupling of the electron and nuclear sub-systems is mediated by the
hyperfine interaction (HFI). In the absence of the HFI, the eigenstates of the
system are the product states $|\mathrm{el}\rangle|\mathrm{nuc}\rangle$; the
HFI leads to admixtures of the excited nuclear state $|e\rangle$ with the
product states involving the ground $|g\rangle$ nuclear state. In the first
part of the process, the laser excites the occupied valence band state
$\approx|\Omega\rangle|g\rangle$ to a particle-hole eigenstate
$|\Psi_{L}\rangle=a_{d_{i}}^{\dagger}a_{h}|\Omega\rangle|g\rangle+|\delta\Phi_{\mathrm{el}}\rangle|e\rangle$
resonant with the laser frequency (here we use the creation and annihilation
operators $a^{\dagger}$ and $a$; $|\Omega\rangle$ is the valence band quasi-
vacuum state). The HFI-mediated admixture
$|\delta\Phi_{\mathrm{el}}\rangle|e\rangle$ can be substantial due to a
contribution of the $a_{d_{i}}^{\dagger}a_{h_{r}}|\Omega\rangle$ states
resonant with the nuclear transition. It also contains the
$|\Omega\rangle|e\rangle$ state. Such laser excitation exhibits a step-like
character of Fig. 1(b). The components of this coherently excited state decay
due to a combination of vibronic couplings to the crystal on a ps timescale
and radiative particle-hole recombination on a ns timescale. While the
majority of the decays result in a photon emission on the ns timescale, some
population may evolve into the state $|\Omega\rangle|e\rangle$. The resulting
$|\Omega\rangle|e\rangle$ state is embedded into the continuum of particle-
hole states $a_{d_{i}}^{\dagger}a_{h}|\Omega\rangle|g\rangle$ and can thereby
decay into this continuum with the rate $\Gamma=2\pi\rho|\langle
e|\langle\Omega|V_{\mathrm{HFI}}|a_{d_{i}}^{\dagger}a_{h_{r}}|\Omega\rangle|g\rangle|^{2}$.
Here the hole $h_{r}$ is such that the energy difference
$\varepsilon_{d_{i}}-\varepsilon_{h_{r}}$ matches the nuclear excitation
energy $\omega_{\mathrm{nuc}}$ and $\rho$ is the valence band density of
states. The rate has to be summed over all allowed final states, including
phonon degrees of freedom which bring in Frank-Condon factors in the rate
evaluation. This internal conversion process quenches the nuclear transition.
The vibronic couplings further “float” the hot resonant hole state $h_{r}$ to
the top of the valence band. Finally, a radiative particle-hole recombination
emits a fluorescence photon that is red-shifted compared to
$\omega_{\mathrm{nuc}}$. We find that this model semi-quantitatively explains
the observed short-timescale fluorescence spectrum of Fig. 1(b-d) and Fig. 2;
full numerical simulations will be reported elsewhere.

Figure 4: Thorium PDOS for 229Th:LiSrAlF6. The dashed black line represents
the energy of the 229Th nuclear excited state relative to the top of the
valence band.

This mechanism relies on the energy of the $5f$ defect states
$\varepsilon_{d_{i}}$ being lower than $\omega_{\mathrm{nuc}}$. Thus, the
long-timescale signal observed from the nuclear isomeric transition is
potentially due to 229Th atoms that are substituted into the crystal in
arrangements that have $\varepsilon_{d_{i}}>\omega_{\mathrm{nuc}}$ or
vanishing $\rho$ near the isomeric energy. Finally, even without coupling to
defect states, the nuclear radiative lifetime may still be shortened by
effects of the crystal electric field, which mix Th electronic states of
opposite parity. The hyperfine interaction couples the nuclear degree of
freedom to these mixed-parity states, allowing for a competing $E1$ decay
channel for the isomeric state. Such effects may complicate efforts to
determine the radiative lifetime of the bare 229Th isomeric state from that
observed in crystalline hosts.

Given these results and those of Ref. [13], it is clear that the 229Th
isomeric transition is now measured with laser spectroscopic precision,
completing the journey started by Kroger and Reich [23] nearly 50 years ago.
With a narrow feature identified in two separate crystalline hosts, a number
of exciting experiments and applications can be explored. These include
studying the variation of the transition properties (frequency and linewidth)
with chemical environment [24], cooperative nuclear spontaneous emission [25],
and the construction of what may prove to be the ultimate time keeping device,
the nuclear clock [1, 3].

##  I Acknowledgement

The authors thank Yafis Barlas, Arlete Cassanho, Yih-Chung Chang, Hans
Jenssen, Saed Mirzadeh, and Cheuk Ng for valuable discussions. This work was
supported by NSF awards PHYS-2013011 and PHY-2207546, and ARO award
W911NF-11-1-0369. ERH acknowledges institutional support by the NSF QLCI Award
OMA-2016245. This work used Bridges-2 at Pittsburgh Supercomputing Center
through allocation PHY230110 from the Advanced Cyberinfrastructure
Coordination Ecosystem: Services & Support (ACCESS) program, which is
supported by National Science Foundation grants #2138259, #2138286, #2138307,
#2137603, and #2138296.

## References

  * Rellergert  _et al._ [2010] W. G. Rellergert, D. DeMille, R. R. Greco, M. P. Hehlen, J. R. Torgerson, and E. R. Hudson, Phys. Rev. Lett. 104, 200802 (2010).
  * Peik and Tamm [2003] E. Peik and C. Tamm, EPL 61, 181 (2003).
  * Campbell  _et al._ [2012] C. J. Campbell, A. G. Radnaev, A. Kuzmich, V. A. Dzuba, V. V. Flambaum, and A. Derevianko, Phys. Rev. Lett. 108, 120802 (2012).
  * Flambaum [2006] V. V. Flambaum, Phys. Rev. Lett. 97, 092502 (2006).
  * Litvinova  _et al._ [2009] E. Litvinova, H. Feldmeier, J. Dobaczewski, and V. Flambaum, Phys. Rev. C 79, 064303 (2009).
  * 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, _et al._ , Nature 533, 47 (2016).
  * 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, _et al._ , Phys. Rev. Lett. 125, 142503 (2020).
  * Jeet  _et al._ [2015] J. Jeet, C. Schneider, S. T. Sullivan, W. G. Rellergert, S. Mirzadeh, A. Cassanho, H. P. Jenssen, E. V. Tkalya, and E. R. Hudson, Phys. Rev. Lett. 114, 253001 (2015).
  * Beeks  _et al._ [2023] K. Beeks, T. Sikorsky, V. Rosecker, M. Pressler, F. Schaden, D. Werban, N. Hosseini, L. Rudischer, F. Schneider, P. Berwian, _et al._ , Sci. Rep. 13, 3897 (2023).
  * 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, _et al._ , Nature 617, 706 (2023).
  * Jeet [2018] J. Jeet,  _Search for the low lying transition in the 229Th Nucleus_, Ph.D. thesis, University of California, Los Angeles (2018).
  * [13] J. Tiedau, M. V. Okhapkin, K. Zhang, J. Thielking, G. Zitzer, E. Peik, F. Schaden, T. Pronebner, I. Morawetz, L. Toscani De Col, _et al._ , Phys. Rev. Lett., accepted, March 14 (2024) .
  * Irwin and Kim [1997] G. M. Irwin and K. H. Kim, Phys. Rev. Lett. 79, 990 (1997).
  * Shaw  _et al._ [1999] R. W. Shaw, J. P. Young, S. P. Cooper, and O. F. Webb, Physical Review Letters 82, 1109 (1999).
  * Berdah  _et al._ [1996] M. Berdah, J. Visticot, C. Dedonder-Lardeux, D. Solgadi, and B. Soep, Opt. Commun. 124, 118 (1996).
  * Tkalya  _et al._ [2015] E. V. Tkalya, C. Schneider, J. Jeet, and E. R. Hudson, Phys. Rev. C 92, 054324 (2015).
  * Lödahl  _et al._ [2011] M. Lödahl, V. M. J. Henriques, and D. Kiselman, A&A 533, A82 (2011).
  * Major  _et al._ [2020] G. H. Major, N. Fairley, P. M. A. Sherwood, M. R. Linford, J. Terry, V. Fernandez, and K. Artyushkova, J. Vac. Sci. Technol. A 38, 061203 (2020).
  * Tran and Blaha [2009] F. Tran and P. Blaha, Phys. Rev. Lett. 102, 226401 (2009).
  * Becke and Johnson [2006] A. D. Becke and E. R. Johnson, J. Chem. Phys. 124, 221101 (2006).
  * Woerner  _et al._ [1992] M. Woerner, T. Elsaesser, and W. Kaiser, Physical Review B 45, 8378 (1992).
  * Kroger and Reich [1976] L. Kroger and C. Reich, Nuc. Phys. A 259, 29 (1976).
  * Tkalya  _et al._ [1996] E. V. Tkalya, V. O. Varlamov, V. V. Lomonosov, and S. A. Nikulin, Phys. Scr. 53, 296 (1996).
  * Tkalya [2011] E. V. Tkalya, Phys. Rev. Lett. 106, 162501 (2011).
  * Kresse and Furthmuller [1996] G. Kresse and J. Furthmuller, Physical Review B 54, 11169 (1996).
  * Blochl [1994] P. E. Blochl, Physical Review B 50, 17953 (1994).
  * Perdew  _et al._ [1996] J. P. Perdew, K. Burke, and M. Ernzerhof, Physical Review Letters 77, 3865 (1996).
  * Pimon  _et al._ [2022] M. Pimon, P. Mohn, and T. Schumm, Advanced Theory and Simulations 5, 10.1002/adts.202200185 (2022).
  * Larsen  _et al._ [2017] A. H. Larsen, J. J. Mortensen, J. Blomqvist, I. E. Castelli, R. Christensen, M. Dulak, J. Friis, M. N. Groves, B. Hammer, C. Hargus, E. D. Hermes, P. C. Jennings, P. B. Jensen, J. Kermode, J. R. Kitchin, E. L. Kolsbjerg, J. Kubal, K. Kaasbjerg, S. Lysgaard, J. B. Maronsson, T. Maxson, T. Olsen, L. Pastewka, A. Peterson, C. Rostgaard, J. Schiotz, O. Sch¸tt, M. Strange, K. S. Thygesen, T. Vegge, L. Vilhelmsen, M. Walter, Z. H. Zeng, and K. W. Jacobsen, Journal of Physics-Condensed Matter 29, 10.1088/1361-648X/aa680e (2017).
  * Nickerson  _et al._ [2020] B. S. Nickerson, M. Pimon, P. V. Bilous, J. Gugler, K. Beeks, T. Sikorsky, P. Mohn, T. Schumm, and A. P·lffy, Physical Review Letters 125, 10.1103/PhysRevLett.125.032501 (2020).
  * Nickerson  _et al._ [2021] B. S. Nickerson, M. Pimon, P. V. Bilous, J. Gugler, G. A. Kazakov, T. Sikorsky, K. Beeks, A. Gr¸neis, T. Schumm, and A. P·lffy, Physical Review A 103, 10.1103/PhysRevA.103.053120 (2021).
  * Gaiduk and Staroverov [2009] A. P. Gaiduk and V. N. Staroverov, Journal of Chemical Physics 131, 10.1063/1.3176515 (2009).

##  II Supplementary Information

##  III Obtaining the Fluorescence Spectrum via Gauassian Deconvolution

The spectrum of the fluorescence was obtained by measuring its transmission
through various filter configurations. The number of fluorescent photons
(normalized to the amount of excitation photons), $Y_{i}$ that make it through
a particular filter configuration is given by

$Y_{i}=\int\rho(\lambda)~{}T_{i}(\lambda)~{}\eta_{i}(\lambda)~{}d\lambda~{},$
(1)

where $\rho(\lambda)$ is the spectrum of the fluorescence, $T_{i}$ are the
filter transmission functions (provided by the manufacturer and measured when
possible), and $\eta$ captures the remaining quantum efficiencies of the
detector and geometric acceptance of the lens system.

In order to determine $\rho$, a functional form for the spectrum was chosen,
$\rho^{*}(\lambda,\vec{\xi})$, which is determined by a set of parameters
$\vec{\xi}$. For a particular value of $\vec{\xi}$ we may then compute the
following

$Y^{*}_{i}(\vec{\xi})=\int\rho^{*}(\lambda,\vec{\xi})~{}T_{i}(\lambda)~{}\eta_{i}(\lambda)~{}d\lambda~{},$
(2)

and from that compute

$\chi^{2}=\sum_{i}\frac{\left(Y_{i}-Y^{*}_{i}(\vec{\xi})\right)^{2}}{\sigma_{i}^{2}}~{},$
(3)

where the sum runs over all filter configurations, and $\sigma_{i}$ are the
uncertainties in the normalized fluorescence counts. Minimizing $\chi^{2}$
with respect to the parameters $\vec{\xi}$ will converge to the true spectrum
if $\rho$ is of a functional form described by $\rho^{*}(\lambda,\vec{\xi})$.

Given the observed filter data, it was clear that a major contribution to the
signal was a sharply peaked component in the region of 150 nm to 200 nm, with
a ‘redder’ background component. This was reflected in the improvement of
$\chi^{2}$ from $\approx 600$ with one Gaussian function to $\approx 8$ with
the addition of another Gaussian. Adding more Gaussians did little to improve
the value of $\chi^{2}$. The choice of Gaussians to describe the spectrum is
only reflective of their simplicity as peaked functions. It is likely the true
spectrum is not exactly described by our parameterization, and the value
quoted by our fit for the ”sharp” part of the spectrum should only be seen as
a rough estimate.

##  IV Isomeric Transition Frequency Systematic Uncertainty

The chief source of systematic uncertainty in the determination of the
isomeric transition frequency is the calibration of the VUV laser frequency.
The VUV frequency is given by the difference mixing relation
$\omega=2\omega_{u}-\omega_{v}$ and therefore depends on the measurement of
$\omega_{u}$ and $\omega_{v}$, the UV and visible laser frequency,
respectively. These frequencies are measured using a Bristol 871B wavemeter
and augmented with a calibration via a Xe reference line. Specifically, the
wavelength of the doubled pulsed dye laser (UV PDL) is calibrated by scanning
the two-photon
$5p^{6~{}1}S_{0}~{}\rightarrow~{}5p^{5}\left({}^{2}P^{\circ}_{3/2}\right)6p~{}^{2}\left[1/2\right]_{0}$
transition in Xenon and comparing to the value on the NIST Database. The peak
was always within 0.5 pm of the expected value (499.2576 nm for the
fundamental). Thus, the UV PDL wavelength was accurate to within $\approx$ 1.2
GHz. The the visible dye laser (VIS PDL) wavelength was measured by the same
wavemeter, whose stated calibration uncertainty is 1 pm, or $\approx$ 500 MHz
at $785.7$ nm. If we assume the worst case that the errors are anti-correlated
then $\sigma_{VUV}=2\sigma_{u}+\sigma_{v}=3$ GHz. radiatively of accompanied
by the emission of phonons.

Figure 5: Structures used to model Th:LiSrAlF6 labelled as $a\times b\times c$
supercells of LiSrAlF6. Li is shown in dark green, Sr in light green, Al in
blue, F in grey, and Th in red.

##  V Density functional theory calculations

Density Functional Theory (DFT) calculations were used to study the electronic
states and energy levels of the thorium atoms in LiSrAlF6. DFT calculations on
were performed with VASP[26], version 6.3, using the PAW[27] method with a
plane-wave cutoff of 500 eV and a spin-restricted formalism. The PBE[28]
functional was used for all structural optimizations, and the modified Becke-
Johnson (MBJ)[20, 21] functional was used for electronic properties.
Optimizations of $2\times 2\times 1$ supercells were done with a 4-4-4
$k$-point grid.

###  V.1 Defect structures

The lowest-energy thorium defects were identified following a procedure
developed in a previous study of Th:LiCaAlF6 [29]. Thorium strongly favors the
+4 oxidation state, but LiSrAlF6 contains no +4 cations, exchanging Th for any
other atom causes a change in the overall charge. Charge balancing therefore
requires more complex defects, such as Th^4+ replacing Al^3+ with an Li+
vacancy or Th^4+ replacing Ca^2+ with addition of two interstitial F-. These
charges are based on simple chemical considerations and are not imposed in the
electronic structure calculations. The defect structure search in Th:LiCaAlF6
began by generating all possible symmetry-inequivalent charge-neutral defects,
constrained by a maximum number of atoms which can be added or removed to the
structure. This created 1625 distinct defects in a $2\times 2\times 1$
supercell of the host material, 1566 of which were successfully structurally
optimized. For our study of Th:LiSrAlF6 we took these 1566 optimized
structures of Th:LiCaAlF6, replaced Ca by Sr and set the lattice parameters to
those of LiSrAlF6, and reoptimized them. 1534 of these optimizations converged
successfully.

The resulting structures do not all have the same stoichiometries, and so
their energies must be corrected to account for the additional/missing atoms.
We do this by adding or subtracting the energies of side products required to
balance any atoms lost or gained from the Th:LiSrAlF6. These may be the binary
fluorides LiF, SrF2, and AlF3, or the ternary products Li3AlF6 and SrAlF5
because these are more stable than the relevant combinations of binary
fluorides. With these corrected energies we can compare the stabilities of
defects with different stoichiometries.

The lowest-energy defect is thorium replacing a strontium atom with two
interstitial fluorine atoms, which is written in Kroger-Vink notation as
Th^.._Sr + 2F_i′. This contrasts with Th:LiCaAlF6 in which the lowest energy
defect was found to be Th replacing Al with a neighbouring Li vacancy (Th^._Al
+ V_Li′) [29]. The difference may be because Sr^2+ is larger than Ca^2+ so Sr
can more easily accommodate additional fluorides in its coordination sphere.
In this structure Th is coordinated to 8 fluorides in a low-symmetry geometry
which may be described as a distorted bicapped octahedron. The lowest-energy
$2\times 2\times 1$ structure found by the screening procedure is shown in
Figure 5.

In fact, the screening of defects produces 30 structures within 0.015 eV of
the lowest energy structure, all with the same stoichiometry. Automatic
symmetry detection, using the Atomic Simulation Environment (ase) python
package,[30] finds that only 7 of these are symmetry-unique. Visual inspection
of these structures and calculation of the average Th-F bond lengths suggest
that they are in fact all identical, consistent with their very similar
energies. We therefore use only one of them for further structural and
electronic analysis.

A $2\times 2\times 1$ supercell may be too small for computation of accurate
electronic properties because the effective thorium concentration is
$1.05\times 10^{21}\text{ cm}^{-3}$ and the minimum distance between periodic
images of Th is 10.3 Å. To reduce unphysical Th-Th interactions, we performed
electronic structure calculations on $3\times 3\times 2$ and $4\times 4\times
2$ supercells, with effective Th concentrations of $2.33\times 10^{20}\text{
cm}^{-3}$ and $1.31\times 10^{20}\text{ cm}^{-3}$, respectively, and minimum
Th-Th distances of 15.5 Å and 20.6 Å, respectively. These supercells are shown
in Figure 5.

###  V.2 Defect electronic states

The reason for studying the electronic states of the thorium defects is to
determine whether the excited nuclear state of ^229Th can be excited or decay
by coupling to an excited electronic state. DFT typically underestimates band
gaps; in pure LiSrAlF6 the band gap computed by our PBE method is 7.88 eV,
significantly below the experimental value of 10.69 eV. This is a problem
because the nuclear excited state lies at approximately 8.35 eV, so PBE
predicts that the excited state lies within the conduction band. This is
qualitatively wrong, and prevents understanding of the electronic defect
location relative to the conduction band. Our solution to this is to use the
mBJ (modified Becke-Johnson) meta-GGA functional [20, 21], which is
exceptionally successful at computing band gaps for a fraction of the cost of
a hybrid functional. mBJ gives a band gap for pure LiSrAlF6 of 11.3 eV, an
overestimation of about 5%, which is important because it is above the nuclear
excitation energy so we can place the defect electronic states in the band gap
without needing to apply an empirical shift of the conduction band, or
“scissor operator”, as has been done for calculations using the PBE and HSE
functionals [31, 32]. The other important aspect of mBJ is its low cost-to-
accuracy ratio which will allow us to calculate the large supercells described
above to minimize spurious Th-Th interactions. For calculations of electronic
properties, such as the density of states and energies of the defect
electronic states, we will therefore use the mBJ functional. Structural
optimizations and determination of the relative energies of different defects
must still be done with PBE because mBJ is a “potential only” functional which
gives accurate electronic properties for a given structure but cannot be used
to compare different structures [33].

Figure 6: Th PDOS in a 3x3x2 supercell computed with different $k$-point
grids. The dashed line denotes the energy of the excited ^229Th nuclear state
relative to the top of the valence band.

Figure 7: (left) Th PDOS in a 4x4x2 cell computed at the $\Gamma$ point. The
dashed line denotes the energy of the excited ^229Th nuclear state relative to
the top of the valence band. (right) Total DOS for the 3x3x2 supercell of
Th:LiSrAlF6.

We tested the convergence of the thorium projected density of states (PDOS) as
a function of the size of the $k$-point grid in the calculation. The results
are shown in Figure 6. In the 2-2-2 grid the Th $5f$ levels appear just above
5 eV, while in the 3-3-2 and 4-4-2 grids these levels appear at 6.8 eV. These
calculations show that a 3-3-2 $k$-point grid is necessary to converge the DOS
in the $3\times 3\times 2$ supercell. Figure 7 shows the thorium PDOS computed
in a $4\times 4\times 2$ supercell. The size of this cell meant that we were
only able to do a $\Gamma$ point calculation, i.e. a $k$-mesh with only a
single $k$ point. The PDOS closely matches the non-converged plot in Figure 6
in that the energies of the excited states are underestimated, indicating that
the DOS is not converged in this supercell in a $\Gamma$ point calculation. We
therefore use the $3\times 3\times 2$ supercell with a 4-4-2 $k$-mesh for all
subsequent electronic structure analysis. The total DOS in Figure 7(right)
shows the defect states arond 7 eV and then the bulk conduction band at around
11.5 eV, in good agreement with the value computed for pure LiSrAlF6.


* (68) Nagele, J., van Oostrom, V., Sternagel, C.: A short mechanized proof of the Church-Rosser theorem by the Z-property for the $\lambda$$\beta$-calculus in Nominal Isabelle. CoRR abs/1609.03139 (2016)
  * (69) Nipkow, T.: More church-rosser proofs (in isabelle/hol). In: CADE. pp. 733–747 (1996)
  * (70) Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press (1990)
  * (71) Norrish, M.: Recursive function definition for types with binders. In: TPHOLs. pp. 241–256 (2004)
  * (72) Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3) (1989)
  * (73) Pfenning, F., Elliot, C.: Higher-order abstract syntax. In: PLDI. pp. 199–208 (1988)
  * (74) Pfenning, F.: A proof of the Church-Rosser theorem and its representation in a Logical Framework. Tech. rep., Pittsburgh, PA, USA (1992)
  * (75) Pfenning, F.: Computation and Deduction (2001)
  * (76) Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI. pp. 199–208 (1988)
  * (77) Pfenning, F., Schürmann, C.: System description: Twelf - A meta-logical framework for deductive systems. In: CADE. pp. 202–206 (1999)
  * (78) Pientka, B.: Beluga: Programming with dependent types, contextual data, and contexts. In: FLOPS. pp. 1–12 (2010)
  * (79) Pitts, A.M.: Nominal logic: A first order theory of names and binding. In: TACS. pp. 219–242 (2001)
  * (80) Pitts, A.M.: Alpha-structural recursion and induction. J. ACM 53(3) (2006)
  * (81) Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)
  * (82) Pollack, R.: Closure under alpha-conversion. In: TYPES. pp. 313–332 (1993)
  * (83) Pollack, R., Sato, M., Ricciotti, W.: A canonical locally named representation of binding. J. Autom. Reasoning 49(2), 185–207 (2012)
  * (84) Popescu, A.: Contributions to the theory of syntax with bindings and to process algebra (2010), phD thesis, Univ. of Illinois. Available at andreipopescu.uk/thesis.pdf
  * (85) Popescu, A., Gunter, E.L.: Recursion principles for syntax with bindings and substitution. In: ICFP. pp. 346–358 (2011)
  * (86) Popescu, A., Gunter, E.L., Osborn, C.J.: Strong normalization of System F by HOAS on top of FOAS. In: LICS. pp. 31–40 (2010)
  * (87) Popescu, A., Roşu, G.: Term-generic logic. Theor. Comput. Sci. 577, 1–24 (2015)
  * (88) Poswolsky, A., Schürmann, C.: System description: Delphin—A functional programming language for deductive systems. Electr. Notes Theor. Comput. Sci. 228, 113–120 (2009)
  * (89) Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle/HOL – animating a many-sorted metatheory. In: CPP. pp. 114–130 (2013)
  * (90) Shankar, N.: A mechanical proof of the Church-Rosser theorem. J. ACM 35(3), 475–522 (1988)
  * (91) Takahashi, M.: Parallel reductions in lambda-calculus. Inf. Comput. 118(1), 120–127 (1995)
  * (92) Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In: LICS, pp. 596–605 (2012)
  * (93) Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)
  * (94) Urban, C., Berghofer, S.: A recursion combinator for nominal datatypes implemented in Isabelle/HOL. In: IJCAR. pp. 498–512 (2006)
  * (95) Urban, C., Berghofer, S., Norrish, M.: Barendregt’s variable convention in rule inductions. In: CADE. pp. 35–50 (2007)
  * (96) Urban, C., Cheney, J., Berghofer, S.: Mechanizing the metatheory of lf. In: LICS 2008. pp. 45–56 (2008)
  * (97) Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in Nominal Isabelle. In: ESOP. pp. 480–500 (2011)
  * (98) Urban, C., Tasson, C.: Nominal techniques in Isabelle/HOL. In: CADE. pp. 38–53 (2005)
  * (99) Wenzel, M.: The Isabelle/Isar reference manual (2018), available at http://isabelle.in.tum.de/doc/isar-ref.pdf
  * (100) Wenzel, M.: The Isabelle system manual (2019), https://isabelle.in.tum.de/doc/system.pdf

APPENDIX

The Isabelle theories can be downloaded from the paper’s website lambda-
scripts  and processed with Isabelle 2019. The general framework (applicable
to an arbitrary syntax with bindings and reported in our companion paper
ghepop-2017-jar ) is an entry in the Archive of Formal Proofs
Binding_Syntax_Theory-AFP  and must be imported from there. Our development is
based on that entry and is structured in three sessions (provided with their
customary ROOT files (IsabelleSystemManual, , §2)): Interface,
Instance$\\_$Lambda$\\_$Syntax and Case$\\_$Studies.

### The Interface session

This session pre-instantiates the general framework to several commonly
encountered arities. The development is also syntax-independent, and can be
regarded as being part of the general framework.

### The Instance$\\_$Lambda$\\_$Syntax session

This session fully instantiate the framework to the two particular syntaxes
discussed in this paper: the single-sorted (unsorted) one of
$\lambda$-calculus (used for the CBN calculus) and the two-sorted variation
that distinguishes values from other terms (used for the CBV calculus). It
corresponds to Section 2. The relevant theories in this session are called L,
L$\\_$Inter, LV and LV$\\_$Inter.

The theory L contains a wealth of facts that are made available for the
(unsorted) syntax of $\lambda$-calculus after instantiating our framework
(discussed in Section 2.1). The theory file contains detailed comments to
guide the reader through these facts. They cover properties of the
constructors and the operators (freshness, swapping, unary substitution and
parallel substitution), as well as induction and recursion and semantic-
interpretation principles. The theory LV has a similar structure and content
(though fewer comments), but considers the two-sorted syntax of
$\lambda$-calculus with emphasized values (discussed in Section 2.2).

The theories L$\\_$Inter and LV$\\_$Inter further customize the two syntax
instances with a few abbreviations and re-formulations of facts that we have
deemed more convenient for this particularly simple syntaxes. Notably, they
introduce the Lm constructor, which in L$\\_$Inter has type $\mbox{\bf
var}\rightarrow\mbox{\bf term}\rightarrow\mbox{\bf term}$, by putting together
an abstraction constructor $\mbox{\rm{\normalsize Abs}}:\mbox{\bf
var}\rightarrow\mbox{\bf term}\rightarrow\mbox{\bf abs}$ and a one-binding-
argument constructor, $\mbox{\rm{\normalsize Lam}}:\mbox{\bf
abs}\rightarrow\mbox{\bf term}$. More precisely, $\mbox{\rm{\normalsize
Lm}}\;x\;X$ abbreviates $\mbox{\rm{\normalsize Lam}}\;(\mbox{\rm{\normalsize
Abs}}\;x\;X)$. (Our general framework employs explicit abstractions as a
separate syntactic category, whereas here we preferred to inline abstractions
as part of a single Lm-constructor.)

Here is a map between Section 2.1’s propositions and their formal counterparts
in theory L:111111Note that the paper covers only a small subset of the facts
provided in the formalization. The latter are best explored by reading the
content of theory L, which includes detailed comments and explanations. The
name of the operators and theorems follow a uniform pattern which can be
understood by reading these comments.

  * •

Prop. 1 corresponds to lemmas “Lam inj” and “Abs$\\_$lm$\\_$lm
swap$\\_$vlm$\\_$lm ex”

  * •

Prop. 2 corresponds to lemmas "subst$\\_$vlm$\\_$lm compose 1" and
"subst$\\_$vlm$\\_$lm subst$\\_$vlm$\\_$lm compose 2"

  * •

Prop. 3 corresponds to lemma “induct fresh” (reformulated as lemma “induct
fresh 2” in theory L$\\_$Inter)

  * •

Prop. 4 corresponds to lemma “term$\\_$lm fresh cases” (reformulated as lemma
“term fresh cases” in theory L$\\_$Inter)

  * •

Prop. 7 corresponds to lemmas “wlsFSb rec term$\\_$FSb$\\_$morph” and  “wlsFSw
rec term$\\_$FSw$\\_$morph”

  * •

Prop. 10 corresponds to lemmas “wlsFSb rec refl$\\_$freshAll” and “wlsFSb rec
is$\\_$injAll”

  * •

Prop. 12 corresponds to lemma “wlsSEM semInt comp$\\_$int”

### The Case$\\_$Studies session

This session contains the four case studies described in Sections 3.2–3.5 and
Section 4. The relevant theories of this session are:

  * •

CBN, Henkin, CBN$\\_$CR, CBN$\\_$Std and HOAS for the CBN calculus

  * •

CBV, CBV$\\_$CR and CBV$\\_$Std for the CBV calculus

The theory CBN defines Section 3’s various reduction relations and proves
basic facts about them, including fresh rule induction and fresh inversion
principles. The relations have the following names in the formalization:

  * •

The one-step reduction $\ \rightarrow\ $ (Def. 15) is redn.

  * •

The one-step parallel reduction $\ \Rightarrow\ $ (Def. 19) is rednP.

  * •

The labeled one-step parallel reduction $\\!\\!\mbox{$\ \Rightarrow\
$}_{\\!\\!\\!\\_}\\!$ (Def. 26) is rednPN.

  * •

The one-step left reduction $\ \looparrowright\ $ (Def. 23) is rednL.

  * •

The multi-step versions of the relations have an “M” prefixing their name:
Mredn, MrednP, MrednPN and MrednL.

Each of these relations also has infix notations. redn, rednP, rednP and
rednPN are defined using Isabelle’s inductive command, and their multi-step
counterparts are defined by applying the reflexive-transitive closure operator
from the Isabelle library.

The other mentioned theories have self-explanatory names:

  * •

Henkin handles the soundness theorem for Henkin-style models (Section 3.2)

  * •

CBN$\\_$CR handles the Church-Rosser theorem (Section 3.3)

  * •

CBN$\\_$Std handles the standardization theorem (Section 3.4)

  * •

HOAS handles the HOAS development (Section 3.5)

These theories also define the following recursive functions presented in this
paper. In all cases, the end-product formal facts are obtained after expanding
the definition of FSb or FSw model morphisms.

  * •

Section 2.1’s number of free occurrences operator, no, using substitution-
aware recursion—Def. 8 corresponds to CBN’s lemmas no$\\_$simps, no$\\_$subst
and no$\\_$fresh.

  * •

Section 3.3’s complete development operator, cdev, using swapping-aware
recursion—Def. 21 corresponds to theory CBN$\\_$CR’s lemmas “cdev$\\_$simps
1”, cdev$\\_$App$\\_$isDred, cdev$\\_$App$\\_$isLm,
cdev$\\_$App$\\_$not$\\_$isDred$\\_$isLm and cdev$\\_$swap and cdev$\\_$fresh.

  * •

Section 3.5’s HOAS encoding operator enc—Def. 34 corresponds to theory HOAS’s
lemmas  enc$\\_$simps, enc$\\_$subst and enc$\\_$fresh.

Finally, here is the mapping between main theorems presented in Section 3 and
their formal counterparts:

  * •

The Church-Rosser Theorem 18 corresponds to theory CBN$\\_$CR’s theorem
Mredn$\\_$confluent

  * •

The standardization Theorem 25 corresponds to theory CBN$\\_$Std’s theorem
standardization

  * •

The syntactic adequacy theorem represented by clauses (6)–(8) in Def. 34
corresponds to theory HOAS’s lemmas enc$\\_$subst, enc$\\_$fresh and
enc$\\_$inj.

  * •

The $\beta$-reduction adequacy Theorem 36 corresponds to theory HOAS’s
theorems enc$\\_$preserves$\\_$rednL, enc$\\_$reflects$\\_$MrednL and
rednL$\\_$enc$\\_$MrednL.