# Origin of reduced dynamical friction by dark matter halos with net prograde
rotation

Rimpei Chiba1 and Sandeep Kumar Kataria2,3
1Canadian Institute for Theoretical Astrophysics, University of Toronto, 60
St. George Street, Toronto, ON M5S 3H8, Canada
2Department of Astronomy, Shanghai Jiao Tong University, 800 Dongchuan Road,
Shanghai 200240, People’s Republic of China
3Shanghai Key Laboratory for Particle Physics and Cosmology, 6 Shanghai
200240, China E-mail<EMAIL_ADDRESS>
(Accepted XXX. Received YYY; in original form ZZZ)

###### Abstract

We provide an explanation for the reduced dynamical friction on galactic bars
in spinning dark matter halos. Earlier work based on linear theory predicted
an increase in dynamical friction when dark halos have a net forward rotation,
because prograde orbits couple to bars more strongly than retrograde orbits.
Subsequent numerical studies, however, found the opposite trend: dynamical
friction weakens with increasing spin of the halo. We revisit this problem and
demonstrate that linear theory in fact correctly predicts a reduced torque in
forward-rotating halos. We show that shifting the halo mass from retrograde to
prograde phase space generates a positive gradient in the distribution
function near the origin of the $z$-angular momentum ($L_{z}=0$), which
results in a resonant transfer of $L_{z}$ to the bar, making the net dynamical
friction weaker. While this effect is subdominant for the major resonances,
including the corotation resonance, it leads to a significant positive torque
on the bar for the series of direct radial resonances, as these resonances are
strongest at $L_{z}=0$. The overall dynamical friction from spinning halos is
shown to decrease with the halo’s spin, in agreement with the secular behavior
of $N$-body simulations. We validate our linear calculation by computing the
nonlinear torque from individual resonances using the angle-averaged
Hamiltonian.

###### keywords:

Galaxy: kinematics and dynamics – Galaxy: evolution – methods: analytical

††pubyear: 2023††pagerange: Origin of reduced dynamical friction by dark
matter halos with net prograde rotation–C

##  1 Introduction

In the standard model of cosmology, dark matter gravitationally collapses in
the early universe to form dark halos, in which galaxies later form (White &
Rees, 1978). These dark halos are typically rotating, i.e. their net angular
momentum (spin) is non-zero, as they experience mergers (Vitvitska et al.,
2002; Maller et al., 2002) and tidal torques by the surrounding matter
(Peebles, 1969; Doroshkevich, 1970; White, 1984).

The spin of our Galaxy’s dark halo is particularly important for the analysis
of direct detection experiments, which relies on knowledge of the velocity
distribution of dark matter entering the detector (Donato et al., 1998;
Kamionkowski & Kinkhabwala, 1998; Green, 2001). Yet, constraining the dark
halo’s spin has proved challenging because the spin can assume a range of
values without affecting the shape of the gravitational potential (Lynden-
Bell, 1960). The halo’s spin, however, makes noticeable differences in the
evolution of non-axisymmetric structures in galaxies such as bars, spiral arms
and satellites, as the spin changes the strength of dynamical friction
(Weinberg, 1985). Thus the evolutionary history of non-axisymmetric structures
in our Galaxy may serve as a potential probe for the spin of the dark halo.
The Galactic bar is particularly well suited for this purpose since its
evolutionary history has recently been inferred from the current stellar disk
(Chiba et al., 2021; Chiba & Schönrich, 2021). In this context, understanding
the physical mechanism by which the halo’s spin affects dynamical friction is
crucial.

The dependence of dynamical friction on the halo’s spin was first studied by
Weinberg (1985). Using the LBK torque formula (Lynden-Bell & Kalnajs, 1972),
generalized for spherical systems by Tremaine & Weinberg (1984), he predicted
that dynamical friction would increase if the halo has a net rotation in the
same direction as the bar. This argument follows from the fact that spinning
the halo forward increases the fraction of dark matter on prograde orbits,
which contribute to dynamical friction more than retrograde orbits.

This prediction, however, has been found to be in disagreement with the
majority of $N$-body simulations, which predict that dynamical friction in
prograde halos in fact decreases (Athanassoula, 1996; Debattista & Sellwood,
2000; Long et al., 2014; Collier et al., 2018; Fujii et al., 2019; Collier &
Madigan, 2021; Kataria & Shen, 2022). The sole exception is the study by Saha
& Naab (2013), who found that bars in prograde halos form more rapidly,
resulting in a higher rate of angular momentum transfer. However, as pointed
out by Long et al. (2014), their simulations were limited to the bar’s growth
epoch. During the secular stage of bar evolution, $N$-body simulations
consistently find that dynamical friction is weakened by the halo’s rotation.
This was recently clarified by Kataria & Shen (2022), who demonstrated that
the dependence of dynamical friction on the halo’s spin reverses in the course
of bar evolution. It has therefore been conjectured that the LBK formula
explains the bar’s early-time behavior, while its secular behavior is beyond
the scope of the theory (Long et al., 2014).

The LBK formula, however, is designed to describe the secular evolution of
galaxies: it is derived under the assumption that the perturber has emerged in
the distant past, i.e. the time-asymptotic limit (Weinberg, 2004, see also
Banik & van den Bosch, 2021). Hence, the formula is expected to predict the
behavior of the simulations at late times, not early times.

In this paper, we recompute the LBK formula and show that the formula in fact
correctly predicts a reduced dynamical friction in prograde halos in agreement
with the secular behavior of $N$-body simulations. The key is that dynamical
friction depends less on the relative population of prograde ($L_{z}>0$) and
retrograde ($L_{z}<0$) orbits but more on the gradient of the distribution
function near $L_{z}=0$ caused by the differences in the number of prograde
and retrograde orbits. Weinberg (1985) was aware of the latter effect,
although its significance was underestimated. The effect is particularly
profound for the direct-radial resonances (Weinberg & Katz, 2007), where the
radial motion of the orbit directly resonates with the bar’s rotation. These
resonances are strongest when the orbits are perpendicular to the galactic
plane ($L_{z}=0$) and hence most sensitive to changes in the gradient of the
distribution function near $L_{z}=0$. We show that, in prograde halos,
dynamical friction by these resonances is considerably weakened and that the
total reduction outweighs the amplification of dynamical friction by the other
main resonances (e.g. corotation resonance, outer Lindblad resonance).

This paper is organized as follows: We first describe our model of spinning
halos in Section 2. We then introduce the LBK torque formula in Section 3,
before applying it to spinning halos in Section 4. We summarize in Section 5.

##  2 Model of spinning dark halos

The computation of the LBK torque formula requires a model for the
distribution function (DF) $f$ of spinning dark halos. We construct the DF of
spinning halos mostly following the procedure by Binney (2014). Throughout the
paper, we adopt the normalization
$\int\mathrm{d}^{3}{\bm{x}}\mathrm{d}^{3}{\bm{v}}f=1$.

We assume the halo is in dynamical equilibrium prior to bar formation and that
its potential is integrable (in particular, spherical111Simulations by Collier
et al. (2018) indicate that dynamical friction by spherical, oblate, and
prolate halos responds similarly to changes in the halo’s spin.) such that, by
Jeans’ theorem, the DF is only a function of the actions $f({\bm{J}})$.
Actions ${\bm{J}}$ are integrals of motion and constitute canonical
coordinates together with the angles ${\bm{\theta}}$, which specify the phase
of the orbital motions (Binney & Tremaine, 2008). Specifically, we adopt
${\bm{J}}=(J_{r},L,L_{z})$, where $J_{r}$ is the radial action, $L$ is the
magnitude of the angular momentum vector, and $L_{z}$ is its $z$-component,
which determines the orbital inclination $\beta\equiv\cos^{-1}(L_{z}/L)$. The
conjugate angles ${\bm{\theta}}=(\theta_{r},\theta_{\psi},\theta_{\varphi})$
specify the phase of the radial motion, the phase of the azimuthal motion in
the two dimensional orbital plane, and the longitude of the ascending node,
which is fixed. We denote the corresponding orbital frequencies by
$\mathbf{\Omega}\equiv\dot{{\bm{\theta}}}=(\Omega_{r},\Omega_{\psi},\Omega_{\varphi})$,
where $\Omega_{\varphi}=0$.

In general, a DF can be split into parts that are even and odd in $L_{z}$
(Lynden-Bell, 1960)

$\displaystyle f({\bm{J}})=f_{+}({\bm{J}})+f_{-}({\bm{J}}),$ (1)

where $f_{\pm}({\bm{J}})\equiv[f(J_{r},L,L_{z})\pm f(J_{r},L,-L_{z})]/2$. The
density distribution is solely determined by the even part $f_{+}$, while only
the odd part $f_{-}$ contributes to the net rotation $\langle L_{z}\rangle$.

For the even DF, we adopt an isotropic distribution $f_{+}=f_{+}(E)$ with an
Hernquist (1990) density profile: $\rho(r)=Mr_{\rm s}/[2\pi r(r_{\rm
s}+r)^{3}]$, where $M=1.5\times 10^{12}\,{\rm M}_{\odot}$ and $r_{\rm
s}=20\,{\rm kpc}$ are the total mass and scale radius. We have also explored
other density profiles but found qualitatively similar results with
differences only in the relative contributions from each resonance. For
comparison with the study by Weinberg (1985), we report results using the
singular isothermal sphere in Appendix B.

Figure 1: The function $g$ prescribing the redistribution of mass in $L_{z}$
(equation 4).

The odd component of the DF $f_{-}$ can take an arbitrary form so long as the
total DF $f$ is nowhere negative. Since our $f_{+}$ is everywhere positive, we
may write

$\displaystyle f_{-}({\bm{J}})=g({\bm{J}})f_{+}({\bm{J}}),$ (2)

where $g$ is an odd function of $L_{z}$ that is bounded $|g|\leq 1$. The total
DF is then $f=(1+g)f_{+}$.

It has been common in the past to construct spinning halos by randomly
reversing the direction of motion of a certain fraction of retrograde
particles (Widrow & Dubinski, 2005; Saha & Naab, 2013; Long et al., 2014;
Collier et al., 2018; Fujii et al., 2019). This corresponds to setting

$\displaystyle g(L_{z})=$ $\displaystyle\Lambda\,{\rm sgn}\left(L_{z}\right),$
(3)

where the parameter $\Lambda\in[-1,1]$ controls the degree of the halo’s spin
with positive (negative) values for prograde (retrograde) halos. At the
maximal rotation $\Lambda=\pm 1$, the halo consists entirely of prograde or
retrograde orbits.

The function (3) bears a discontinuity at the origin, which is unrealistic. We
smooth the DF by setting

$\displaystyle g(L,L_{z})=\Lambda\tanh\left(\frac{\chi
L_{z}}{L}\right)=\Lambda\tanh\left[\chi\cos\left(\beta\right)\right],$ (4)

where the parameter $\chi$ determines how steeply the DF varies with $L_{z}$
near the origin. Fig. 1 plots equation (4). As $\chi$ increases, the variation
in $L_{z}$ becomes steeper, and in the limit $\chi\rightarrow\infty$, the DF
becomes discontinuous, reducing to equation (3). By default, we set $\chi=3$
although our conclusion is independent of $\chi$, as we shall see in Section
4.2.

Figure 2: The angular momentum of spinning halos averaged over spherical
shells as a function of radius. The solid curves are our models with
$g=\Lambda\tanh(\chi L_{z}/L)$ (equation 4), while the dashed curves are
models with $g=\Lambda\tanh(\chi L_{z}/L_{\rm s})$, where $L_{\rm s}$ is a
constant (equation 5). Cosmological simulations predict $\bar{L}_{z}\propto
r^{1.1}$.

An alternative model would be

$\displaystyle g(L_{z})=\Lambda\tanh\left(\frac{\chi L_{z}}{L_{\rm
s}}\right),$ (5)

where $L_{\rm s}$ is a constant. This functional form is commonly used in
modeling the DF of rotating stellar halos (e.g. Deason et al., 2011; Fermani &
Schönrich, 2013; Binney, 2014; Gherghinescu et al., 2023). This form has a
universal scale $L_{\rm s}$ for the spinning curve $g$, so the halo’s rotation
becomes increasingly small towards small $L$ (i.e. towards the inner halo).
Fig. 2 plots the $z$-angular momentum averaged over spherical shells as a
function of radius, $\bar{L}_{z}(r)$, where the average is performed by Monte
Carlo integration. Cosmological simulations predict that this relation
approximately follows a single power law $\bar{L}_{z}\propto r^{\alpha}$ with
$\alpha=1.1\pm 0.3$ (Barnes & Efstathiou, 1987; Bullock et al., 2001). The
blue solid curves are the $\bar{L}_{z}$ of our spinning models (4), which
approximately follow this scaling relation apart from large radii, where
$\alpha\sim 0.7$. The dashed curves are the spinning models with a universal
scale $L_{\rm s}$ (5). The net rotation rapidly decays towards small radii
($\alpha\sim 2.6$), deviating significantly from predictions by cosmological
simulations. Here we set $\Lambda=1$ and $L_{\rm s}=\sqrt{GMr_{\rm s}}$,
though the index $\alpha$ is independent of these parameters. The more
detailed distribution of $L_{z}$ in the meridian plane also favors our
functional form (4) over (5) (Appendix A). Hence, we adopt the former
throughout the paper. We have also explored models of $g$ in which the
gradient does not peak at $L_{z}=0$ although the results were qualitatively
the same (Appendix C).

Figure 3: The ratio between the spin parameters $\Lambda$ (equation 2) and
$\lambda$ (equation 6) as a function of the steepness $\chi$ of the
distribution near $L_{z}=0$.

The rotation of the dark halo is commonly characterized by the dimensionless
total angular momentum (Peebles, 1971):

$\displaystyle\lambda=\frac{|\langle\bm{L}\rangle||\langle
E\rangle|^{1/2}}{GM},$ (6)

where $\langle{\bm{L}}\rangle$ and $\langle E\rangle$ are the specific angular
momentum vector and specific energy of the halo, i.e. total angular
momentum/energy divided by the total halo mass $M$. (Note that Peebles’
equation reads $M^{2.5}$ instead of $M$ since it uses the total angular
momentum and energy.) In this paper, we always take the axis of rotation to be
the $z$ axis, so $|\langle{\bm{L}}\rangle|=|\langle L_{z}\rangle|$. The two
spin parameters $\lambda$ and $\Lambda$ scale linearly since only $f_{-}$
contributes to $\langle L_{z}\rangle$:

$\displaystyle\langle
L_{z}\rangle=\\!\\!\int\\!\\!\mathrm{d}^{3}{\bm{\theta}}\mathrm{d}^{3}{\bm{J}}f({\bm{J}})L_{z}=\Lambda(2\pi)^{3}\\!\\!\int\\!\\!\mathrm{d}^{3}{\bm{J}}\tanh\left(\frac{\chi
L_{z}}{L}\right)f_{+}({\bm{J}})L_{z}.$ (7)

Fig. 3 shows the ratio between the two spin parameters as a function of $\chi$
in our standard model with an isotropic Hernquist halo. The ratio increases
with $\chi$ since more orbits at small $L_{z}$ are converted from retrograde
to prograde (cf. Fig. 1). The value converges to $\lambda/\Lambda\simeq 0.243$
in the discontinuous limit $\chi\rightarrow\infty$. Cosmological simulations
predict that $\lambda$ follows a log-normal distribution with median
$\bar{\lambda}\sim 0.03-0.05$ (e.g. Barnes & Efstathiou, 1987; Cole & Lacey,
1996; Bullock et al., 2001; Bett et al., 2007; Zjupa & Springel, 2017; Jiang
et al., 2019), corresponding to $|\bar{\Lambda}|\sim 0.14-0.23$ for $\chi=3$.

##  3 LBK torque formula

The Lynden-Bell & Kalnajs (LBK, 1972) torque formula describes dynamical
friction in finite inhomogeneous systems, in contrast to the well-known
Chandrasekhar (1943) formula developed for infinite homogeneous systems. The
analogy between the two was drawn by Tremaine & Weinberg (1984). The LBK
formula reads

$\displaystyle\tau_{\rm
LBK}=\left(2\pi\right)^{3}\sum_{\bm{n}}n_{\varphi}\\!\int\\!\mathrm{d}^{3}{\bm{J}}{\bm{n}}\\!\cdot\\!\frac{{\partial}f}{{\partial}{\bm{J}}}|\hat{\Phi}_{{\bm{n}}}({\bm{J}})|^{2}\pi\delta\\!\left({\bm{n}}\cdot\mathbf{\Omega}-n_{\varphi}\Omega_{\rm
p}\right),$ (8)

where $f$ is the unperturbed distribution function of the field particles
(here, the dark halo), $\Omega_{\rm p}$ is the pattern speed of the perturber
subject to dynamical friction (here, the galactic bar), and
$\hat{\Phi}_{{\bm{n}}}({\bm{J}})$ is the Fourier series coefficient of the
potential perturbation expanded in the angle variables with integer indices
${\bm{n}}=(n_{r},n_{\psi},n_{\varphi})$.

Figure 4: Top panels: Fourier coefficients of the perturbed potential
$|\Phi_{{\bm{n}}}|$ in $(L_{z},L)$ space at $J_{r}=500\,{\rm kpc}^{2}\,{\rm
Gyr}^{-1}$. The black lines mark the orbital inclinations,
$\beta=\cos^{-1}(L_{z},L)$, equally spaced by $\pi/8$. The ${\bm{n}}=(0,2,2)$
corotation resonance (left) is strongest at $\beta=0$, the ${\bm{n}}=(1,0,2)$
direct-radial resonance (middle) is strongest at $\beta=\pi/2$, and the
${\bm{n}}=(2,-2,2)$ resonance (right) is strongest at $\beta=\pi$. Bottom
panels: The LBK torque as a function of the halo’s spin $\Lambda$. The blue
and red lines indicate the torques arising from the gradient in $f_{+}$ and
$g$, respectively (see equation 10), and the black line marks the sum of the
two. The torque by the corotation resonance becomes more negative in prograde
halos ($\Lambda>0$), whereas the torques by the other two resonances increase
with $\Lambda$.

The LBK formula is derived upon a variety of approximations. A summary of its
derivation is given in Chiba & Schönrich (2022). In brief, the formula rests
on the assumptions that (i) the self-gravity of the halo’s response is
neglected, (ii) the perturbation evolves slowly (the slow limit) (iii) and has
already evolved over timescales much longer than the dynamical time (the time-
asymptotic limit), (iv) but shorter than the libration time, which sets the
onset of nonlinearity (the linear approximation)222Alternatively, the linear
approximation can be justified by assuming the fast limit, where the frequency
of the perturber changes rapidly such that the near-resonant orbits have no
time to resonate and become nonlinear (Tremaine & Weinberg, 1984).. Hence, the
LBK formula does not provide an accurate description of dynamical friction
over the full range of evolution. Despite the many approximations, however,
the formula gives a qualitatively correct explanation to the behavior of bars
in $N$-body simulations, as we shall demonstrate.

As a side note, each of the assumptions above can be relaxed independently.
The first approximation (i) can be amended within the linear formalism by
means of the matrix method (e.g. Kalnajs, 1977; Weinberg, 1989; Chavanis,
2012; Heyvaerts et al., 2017). The second and third approximations (ii, iii)
can also be relaxed within the linear formalism, resulting in a general time-
dependent torque formula (Weinberg, 2004; Banik & van den Bosch, 2021), which
can also incorporate collective effects (e.g. Murali, 1999; Rozier et al.,
2022; Dootson & Magorrian, 2022). The last linear approximation (iv) causes an
issue near the resonances, which can be worked around instead by the method of
averaging (Lichtenberg & Lieberman, 1992). Dynamical friction in the nonlinear
regime was studied by Tremaine & Weinberg (1984) in the time-asymptotic limit
and by Chiba & Schönrich (2022); Banik & van den Bosch (2022) in the slow
limit. Both limits were removed in Chiba (2023). Hamilton et al. (2022)
included the effect of diffusion and demonstrated the recovery of the linear
regime in the strongly diffusive limit.

The LBK formula (8) states that dynamical friction arises from the gradient in
the distribution function at the resonances:
${\bm{n}}\cdot\mathbf{\Omega}-n_{\varphi}\Omega_{\rm p}=0$. The physical
picture of this is analogous to Landau damping (Landau, 1946): near a
resonance, particles initially on the lower energy side of the resonance will,
on average, gain energy from the perturber, while those on the higher energy
side of the resonance will give up energy to it. Dynamical friction occurs
when the former outnumbers the latter.

More specifically, the LBK torque (8) depends on the slope of the distribution
function in action space ${\bm{J}}$ in the direction parallel to the resonant
vector ${\bm{n}}$. The reason for this is best understood via the fast-slow
angle-action variables (e.g. Lynden-Bell, 1979; Tremaine & Weinberg, 1984). In
the frame rotating at $\Omega_{\rm p}$, unperturbed orbits precess with the
resonant frequency
$\Omega_{s}\equiv{\bm{n}}\cdot\mathbf{\Omega}-n_{\varphi}\Omega_{\rm p}$ (see
the illustration by Weinberg & Katz, 2007). As the resonance is approached,
this precession frequency becomes much smaller than the individual orbital
frequencies ${\bm{\Omega}}_{\rm f}\equiv(\Omega_{r},\Omega_{\psi})$, so the
dynamics splits into slow and fast components. The orbital phase of the
respective motions is given by the slow angle $\theta_{\rm
s}\equiv{\bm{n}}\cdot{\bm{\theta}}-n_{\varphi}\Omega_{\rm p}$ and the fast
angles ${\bm{\theta}}_{\rm f}\equiv(\theta_{r},\theta_{\psi})$. Making a
canonical transformation to these new angles, one finds that their conjugate
slow-fast actions are $(J_{\rm s},J_{{\rm f}_{1}},J_{{\rm
f}_{2}})\equiv(L_{z}/n_{\varphi},J_{r}-n_{r}L_{z}/n_{\varphi},~{}L-n_{\psi}L_{z}/n_{\varphi})$.
Because actions are adiabatic invariants, when averaged over time longer than
the periods of the fast motions ${\bm{\Omega}}_{\rm f}^{-1}$, only the slow
action may change, while the fast actions are effectively constant. It is
easily verified that these fast actions constitute vectors perpendicular to
${\bm{n}}$,

$\displaystyle{\bm{J}}\times{\bm{n}}=(n_{\varphi}J_{{\rm
f}_{1}},~{}n_{\varphi}J_{{\rm f}_{2}},~{}n_{\psi}J_{{\rm f}_{1}}-n_{r}J_{{\rm
f}_{2}}).$ (9)

Since fast actions are conserved, it follows that secular evolution in action
space occurs only in the direction parallel to ${\bm{n}}$. The factor
${\bm{n}}\\!\cdot\\!{\partial}f/{\partial}{\bm{J}}$ in the LBK formula
represents the fact that dynamical friction is caused by this slow rectilinear
evolution of the particle’s distribution along the resonant vectors ${\bm{n}}$
(see related discussion by Fouvry & Pichon, 2015).

##  4 Results

Using the spinning dark halo introduced in Section 2, we now compute the
torque on galactic bars and investigate its dependence on the halo’s rotation.
The potential perturbation by the bar is modeled by a simple quadrupole (see
Chiba & Schönrich, 2022). In this model, the Fourier coefficients
$\hat{\Phi}_{{\bm{n}}}$ are non-zero only for $n_{\varphi}=2$ and
$n_{\psi}=2,0,-2$. The possible values of $n_{r}$ in our standard Hernquist
potential are $n_{r}\geq-1$ for $n_{\psi}=2$, $n_{r}\geq 1$ for $n_{\psi}=0$,
and $n_{r}\geq 2$ for $n_{\psi}=-2$ (Chiba & Schönrich, 2022).

###  4.1 LBK torque by spinning dark halos

The LBK torque (8) by a spinning halo (1) is

$\displaystyle\tau_{\rm LBK}=$
$\displaystyle\left(2\pi\right)^{3}\sum_{\bm{n}}n_{\varphi}\\!\int\\!\mathrm{d}^{3}{\bm{J}}{\bm{n}}\\!\cdot\\!\left[\left(1+g\right)\frac{{\partial}f_{+}}{{\partial}{\bm{J}}}+f_{+}\frac{{\partial}g}{{\partial}{\bm{J}}}\right]$
$\displaystyle\times|\hat{\Phi}_{{\bm{n}}}({\bm{J}})|^{2}\pi\delta\\!\left({\bm{n}}\cdot\mathbf{\Omega}-n_{\varphi}\Omega_{\rm
p}\right).$ (10)

The first term in the square bracket describes the gradient in the original
non-rotating DF $f_{+}$ weighted by $(1+g)$, i.e. the redistribution of mass
in $L_{z}$. We denote the torque arising from this term as $\tau_{f_{+}}$. The
second term describes the gradient in the DF due to the reweighting itself. We
refer to the torque resulting from this term as $\tau_{g}$. To clarify the
origin of dynamical friction, we present the two torques separately. Note that
the LBK torque is linear in $\Lambda$, so in practice one only needs to
compute the torque at $\Lambda=0$ and its derivative with respect to
$\Lambda$.

Fig. 4 plots the LBK torque as a function of the halo’s spin $\Lambda$
(bottom) along with the amplitude of the perturbation
$|\hat{\Phi}_{{\bm{n}}}|$ (top) for three different resonances. The left
column plots the corotation resonance ${\bm{n}}=(0,2,2)$. This resonance
represents the series of resonances with $n_{\psi}=2$, including the Lindblad
resonances ${\bm{n}}=(\pm 1,2,2)$. As shown in the top panel, the amplitude of
these resonances increases monotonically with $L_{z}$.333It is important to
note that, in spherical systems, the orbital frequencies
$(\Omega_{r},\Omega_{\psi})$, and thus the resonance condition, only depend on
$J_{r}$ and $L$, but not $L_{z}$. Hence, strange as it may sound, retrograde
orbits ($L_{z}<0$) may well be trapped into the “corotation” resonance of the
bar ($\Omega_{\psi}=\Omega_{\rm p}$), even though they are not corotating in
the azimuthal angle! The volume of phase space trapped in the corotation
resonance declines monotonically towards negative $L_{z}$ but only vanishes at
$L_{z}=-L$ (Fig. 4). Hence, increasing the prograde population at the expense
of retrograde orbits enhances the net dynamical friction. This is represented
by the decrease in $\tau_{f_{+}}$ with the halo’s spin $\Lambda$. (Note that
dynamical friction is a negative torque, so a decrease in the torque means an
increase in friction.) In contrast, $\tau_{g}$ increases with $\Lambda$:
spinning the halo forward results in a positive gradient with respect to
$L_{z}$ near $L_{z}=0$, which in turn generates a positive torque. Since the
change in $\tau_{f_{+}}$ outweighs the change in $\tau_{g}$, the total
dynamical friction increases with $\Lambda$444This holds for all resonances
with $n_{\psi}=2$ except for the inner Lindblad resonance, in which the change
in $\tau_{g}$ surpass the change in $\tau_{f_{+}}$ (see Fig. 5).. This
conclusion agrees with Weinberg (1985).

For other resonances, however, the consequences are different. The middle
column shows the case for the direct-radial resonance ${\bm{n}}=(1,0,2)$,
where an orbit completes two radial oscillations during a bar period,
$\Omega_{r}-2\Omega_{\rm p}=0$ (Weinberg & Katz, 2007). This resonance
represents the series of resonances with $n_{\psi}=0$, and is not to be
confused with the outer Lindblad resonance, in which
$\Omega_{r}+2(\Omega_{\psi}-\Omega_{\rm p})=0$. The amplitude of the direct
radial resonance peaks at $L_{z}=0$ and decays symmetrically towards
$L_{z}=\pm L$ where it vanishes. Hence, this resonance is most relevant for
orbits perpendicular to the galactic plane but is irrelevant for in-plane disk
orbits. Due to its symmetric amplitude about $L_{z}=0$, transferring mass
between retrograde and prograde phase-space has no effect on $\tau_{f_{+}}$:
prograde and retrograde orbits resonate with the perturber at equal strength,
so varying their mass ratio does not affect the net friction. However, the
gradient at $L_{z}=0$ caused by the rotation generates a large torque because
the resonance is strongest there. Thus, $\tau_{g}$ rises sharply with
$\Lambda$. The net torque from this resonance increases with $\Lambda$ and
even becomes positive beyond $\Lambda\sim 0.35$.

Finally, the right column plots the torque by ${\bm{n}}=(2,-2,2)$, which is
the strongest resonance among those with $n_{\psi}=-2$. These resonances are
strongest when the orbit is counter-rotating with respect to the bar (i.e. the
amplitude shows an increase towards negative $L_{z}$). Hence, both
$\tau_{f_{+}}$ and $\tau_{g}$ increase with $\Lambda$.

Figure 5: LBK torque as a function of halo spin $\Lambda$ in a Hernquist halo.
The total torque (black) is the sum over all resonances $n_{\psi}=2,0,-2$ up
to $n_{r}=10$.

Fig. 5 shows the torque by the main resonances and the total torque, including
all resonances up to $n_{r}=10$. The torques by the corotation resonance
${\bm{n}}=(0,2,2)$, the outer Lindblad resonance ${\bm{n}}=(1,2,2)$, and other
higher order resonances $n_{r}\geq 2$ with $n_{\psi}=2$ not presented in Fig.
5 decrease with the halos’ spin $\Lambda$. Meanwhile, the torques by the inner
Lindblad resonance ${\bm{n}}=(-1,2,2)$555In a potential with a Hernquist halo
alone, the ILR of the current Galactic bar would lie at a very small angular
momentum ($\sim 10\,{\rm kpc}^{2}\,{\rm Gyr}^{-1}$), so its contribution to
dynamical friction is small. The ILR becomes significant in a model with a
much higher concentration of mass at the inner region (see Appendix B)., the
direct radial resonance ${\bm{n}}=(1,0,2)$, the retrograde resonance
${\bm{n}}=(2,-2,2)$, and all other resonances with $n_{\psi}=0,-2$ increase
with $\Lambda$. The impact of the latter exceeds the former, with the result
that the total torque increases (dynamical friction weakens) with $\Lambda$.
The LBK formula thus correctly accounts for the reduced dynamical friction on
bars in spinning halos found in $N$-body simulations at the secular phase
(Long et al., 2014).

###  4.2 Variation with steepness parameter

So far, we have set the halo rotating using equation (4) with the steepness
parameter set to $\chi=3$. We now check that our qualitative conclusion is
independent of our choice of $\chi$.

Figure 6: The dependence of dynamical friction on the halo’s spin $\Lambda$
for various steepness $\chi$ of the rotating distribution function (equation
4). The red dots mark the values of $\Lambda$ for each $\chi$ that yield
$\lambda=0.1$.

Fig. 6 plots the LBK torque as a function of the halo spin $\Lambda$ for a
variety of $\chi$, where $\chi\rightarrow\infty$ corresponds to a
discontinuous DF (equation 3). A reduction in dynamical friction with
$\Lambda$ is observed irrespective of $\chi$, suggesting the $\chi$ is
qualitatively unimportant. Our result also clarifies that the behavior
observed in past simulations using $\chi\rightarrow\infty$ (e.g. Long et al.,
2014) is not an artifact of the discontinuity in the DF.

Quantitatively, a larger $\chi$ causes a larger impact on dynamical friction.
Note however that a larger $\chi$ also implies a larger total angular momentum
$\lambda$ (cf. Fig. 3). To give a fair comparison, we marked with red dots the
torque expected from halos with equal total angular momentum $\lambda=0.1$:
the larger the $\chi$, the smaller the $\Lambda$ must be in order to keep
$\lambda$ constant. We find that, despite the same $\lambda$, the impact of
spinning the halo becomes more prominent for a steeper distribution (larger
$\chi$). Hence, simulations employing a discontinuous DF are likely
overestimating the impact of the halo’s spin, though the effect is small.

Figure 7: Torque on the bar from individual resonances computed numerically
using the angle-averaged Hamiltonian. The dotted lines represent the torque
predicted by the linear LBK formula (Fig. 4). Note the opposite dependence of
the torque on $\Lambda$ for the corotation resonance (top) and the other two
resonances (middle and bottom).

###  4.3 Comparison with test-particle simulations

To verify our linear calculations, we also compute the full nonlinear torque
from each individual resonance using the method described in Weinberg & Katz
(2007) and Chiba (2023). In short, the contribution to the torque from each
resonance is computed by integrating test particles in the slow angle-action
space using the angle-averaged Hamiltonian, which only retains a single
resonant term of the perturbation.

Fig. 7 shows the torque from individual resonances as a function of time for
three halo spins. The bar is introduced instantly at $t=0$ and rotates at a
fixed pattern speed. The simulations (solid curves) agree with the linear LBK
formula (dotted lines) for approximately half a libration period ($\sim
500\,{\rm Myr}$), after which the evolution becomes nonlinear. The simulations
reconfirm that a forward-spinning halo ($\Lambda>0$, blue) strengthens
dynamical friction by the ${\bm{n}}=(0,2,2)$ resonance but weakens friction by
the ${\bm{n}}=(1,0,2)$ and ${\bm{n}}=(2,-2,2)$ resonances.

The nonlinear torque decays at late times because the resonant orbits slowly
phase mix, thereby erasing the gradient in the DF near the resonances (Chiba &
Schönrich, 2022; Banik & van den Bosch, 2022). In a self-consistent simulation
(Section 4.4), the torque remains non-zero because the resonances continuously
move (Chiba, 2023), and also because the original gradient in the DF can be
recovered by orbital diffusion (Hamilton et al., 2022).

Figure 8: Torque on the dark halo measured in $N$-body simulations of a barred
galaxy.

###  4.4 Comparison with $N$-body simulations

Finally, we qualitatively compare the prediction by the LBK theory with a set
of $N$-body simulations of a galaxy consisting of a stellar disk and a live
dark matter halo. The details of the setup can be found in Kataria & Shen
(2022). Since the impact of the halo’s spin is only weakly dependent on the
steepness parameter $\chi$ (Section 4.2), here we adopt the discontinuous DF
($\chi\rightarrow\infty$): we set the halo rotating forward (backward) by
reversing the velocities of a certain fraction of retrograde (prograde)
orbits. The impact of the discontinuity on the formation and evolution of bars
is explored by Kataria & Shen (2023, in prep.).

Fig. 8 shows the torque on the halo, which is a proxy for the dynamical
friction on the bar. During the late secular phase, the torque is stronger in
retrograde halos ($\Lambda<0$) in agreement with the LBK formula. At early
times, however, the torque is stronger in prograde halos ($\Lambda>0$) because
the bar grows more rapidly (Kuijken & Dubinski, 1994; Saha & Naab, 2013; Long
et al., 2014). This implies that the rotation of the halo not only affects the
secular torque but also the bar instability, as suggested by linear response
theory (e.g. Kalnajs, 1977; Weinberg, 1991; Pichon & Cannon, 1997). Rozier et
al. (2019), in particular, analyzed the stability of rotating Plummer spheres
and identified unstable $m=2$ modes. We conjecture that our rotating dark halo
was similarly unstable to $m=2$ modes and hence formed a ‘dark bar’
(Athanassoula, 2007; Petersen et al., 2016; Collier et al., 2019), which
subsequently fostered (or retarded) the formation of the stellar bar.

##  5 Conclusion

This paper revisited the issue of the contradicting predictions made in the
past by linear theory (LBK formula) and $N$-body simulations regarding the
impact of the dark halo’s rotation on dynamical friction. We reevaluated the
LBK formula and demonstrated that, contrary to past studies, it predicts a
reduced dynamical friction by halos with net prograde rotation, in agreement
with $N$-body simulations.

The LBK formula states that dynamical friction on the perturber is caused by
the gradient in the particle’s distribution function near the resonances.
Spinning the dark halo forward modifies the gradient of the distribution
function in two ways: Firstly, it enhances the density gradient in the
prograde phase space by simply increasing the overall prograde population. The
gradient in the retrograde phase space is conversely reduced. This causes a
net increase in dynamical friction, since the main resonances (e.g. corotation
resonance) have larger amplitude in the prograde phase space (see
$\tau_{f_{+}}$ in Fig. 4). Secondly and more importantly, spinning the halo
results in a positive gradient in the distribution function with respect to
$L_{z}$, typically near the origin $L_{z}=0$. This positive gradient generates
a positive torque on the perturber from all resonances, thus weakening
dynamical friction (see $\tau_{g}$ in Fig. 4). The net change in dynamical
friction is determined by the sum of these two opposing effects.

In contrary to the seminal work by Weinberg (1985), we found that the latter
effect outweighs the former with the result that the overall dynamical
friction weakens with the halo’s spin. A key role is played by the direct
radial resonances ($n_{\psi}=0$), where the radial frequency of orbits
directly couples with the pattern speed (Weinberg & Katz, 2007). These
resonances are highly responsive against the halo’s rotation since they are
strongest at $L_{z}=0$, which is where the halo’s distribution typically bears
the largest gradient in $L_{z}$. We found that the total reduction of
dynamical friction by these resonances, together with the $n_{\psi}=-2$
resonances and the inner Lindblad resonance, exceeds the amplification of
dynamical friction by the rest of the $n_{\psi}=2$ resonances, including the
corotation resonance and the outer Lindblad resonance. We verified our linear
calculation with the nonlinear torque computed using the angle-averaged
Hamiltonian (Section 4.3), and confirmed that the conclusion holds for halos
with a variety of density profiles (Appendix B) and $L_{z}$ distribution
(Section 4.2, Appendix C).

In this paper, we have restricted our analysis to spinning halos constructed
based on spherical isotropic models. However, simulations by others have found
similar effect of the halo’s spin even with nonspherical (Collier et al.,
2018) or anisotropic halos (Debattista & Sellwood, 2000). It would
nevertheless be of interest to investigate whether deviation from sphericity
or isotropy can cause any change in the relative contributions of each
resonance.

An important task in the future will be to provide constraints on the spin of
the Galactic dark halo, which is required for calculating the event rate in
direct detection experiments (e.g. Green, 2001). Obreja et al. (2022) recently
estimated the spin of the dark halo from its correlation with the spin of the
stellar components, in particular the stellar halo. We propose another
possibility, utilizing the recent measurement of the bar’s slowing rate (Chiba
et al., 2021). A natural approach would be to quantify the impact of the
halo’s spin using self-consistent dynamical models of our Galaxy fitted to the
observational data (Cole & Binney, 2017; Binney & Vasiliev, 2023). Beyond
modeling dynamical friction, this will also require estimates on (i) the bar’s
moment of inertia, which we may infer from $N$-body simulations (Beane et al.,
2022), and (ii) the rate of angular momentum exchange between the bar and
other baryons, in particular the gas in the disk. Gas typically yields angular
momentum to the bar (Villa-Vargas et al., 2010; Athanassoula et al., 2013;
Beane et al., 2022) and consequently sinks towards the galactic center, where
it forms the nuclear stellar disk (NSD, Launhardt et al., 2002; Matsunaga et
al., 2015; Schönrich et al., 2015). The torque from the gas can be estimated
from the gas infall rate (Sormani & Barnes, 2019), or from the mass of the NSD
(Sormani et al., 2022) together with its age (Sanders et al., 2023), or
possibly from the chemical history of the NSD (Friske & Schönrich, 2023).

## Acknowledgements

R.C. thanks support by the the Natural Sciences and Engineering Research
Council of Canada (NSERC), [funding reference #DIS-2022-568580]. S.K.K. thanks
the support by the National Key R&D Program of China under grant No.
2018YFA0404501; by the National Natural Science Foundation of China under
grant Nos. 12025302, 11773052, 11761131016; by the “111” Project of the
Ministry of Education of China under grant No. B20019; and by the China Manned
Space Project under grant No. CMS-CSST-2021-B03.

## Data availability

The codes used to produce the results are available from the corresponding
author upon request.

## References

  * Athanassoula (1996) Athanassoula E., 1996, in Buta R., Crocker D. A., Elmegreen B. G., eds, Astronomical Society of the Pacific Conference Series Vol. 91, IAU Colloq. 157: Barred Galaxies. p. 309
  * Athanassoula (2007) Athanassoula E., 2007, MNRAS, 377, 1569
  * Athanassoula et al. (2013) Athanassoula E., Machado R. E. G., Rodionov S. A., 2013, MNRAS, 429, 1949
  * Banik & van den Bosch (2021) Banik U., van den Bosch F. C., 2021, ApJ, 912, 43
  * Banik & van den Bosch (2022) Banik U., van den Bosch F. C., 2022, ApJ, 926, 215
  * Barnes & Efstathiou (1987) Barnes J., Efstathiou G., 1987, ApJ, 319, 575
  * Beane et al. (2022) Beane A., et al., 2022, arXiv e-prints, p. arXiv:2209.03364
  * Bett et al. (2007) Bett P., Eke V., Frenk C. S., Jenkins A., Helly J., Navarro J., 2007, MNRAS, 376, 215
  * Binney (2014) Binney J., 2014, MNRAS, 440, 787
  * Binney & Tremaine (2008) Binney J., Tremaine S., 2008, Galactic Dynamics: Second Edition. Princeton University Press
  * Binney & Vasiliev (2023) Binney J., Vasiliev E., 2023, MNRAS, 520, 1832
  * Bullock et al. (2001) Bullock J. S., Dekel A., Kolatt T. S., Kravtsov A. V., Klypin A. A., Porciani C., Primack J. R., 2001, ApJ, 555, 240
  * Chandrasekhar (1943) Chandrasekhar S., 1943, ApJ, 97, 255
  * Chavanis (2012) Chavanis P.-H., 2012, Physica A Statistical Mechanics and its Applications, 391, 3680
  * Chiba (2023) Chiba R., 2023, MNRAS, 525, 3576
  * Chiba & Schönrich (2021) Chiba R., Schönrich R., 2021, MNRAS, 505, 2412–2426
  * Chiba & Schönrich (2022) Chiba R., Schönrich R., 2022, MNRAS, 513, 768
  * Chiba et al. (2021) Chiba R., Friske J. K. S., Schönrich R., 2021, MNRAS, 500, 4710
  * Cole & Binney (2017) Cole D. R., Binney J., 2017, MNRAS, 465, 798
  * Cole & Lacey (1996) Cole S., Lacey C., 1996, MNRAS, 281, 716
  * Collier & Madigan (2021) Collier A., Madigan A.-M., 2021, ApJ, 915, 23
  * Collier et al. (2018) Collier A., Shlosman I., Heller C., 2018, MNRAS, 476, 1331
  * Collier et al. (2019) Collier A., Shlosman I., Heller C., 2019, MNRAS, 488, 5788
  * Deason et al. (2011) Deason A. J., Belokurov V., Evans N. W., 2011, MNRAS, 411, 1480
  * Debattista & Sellwood (2000) Debattista V. P., Sellwood J. A., 2000, ApJ, 543, 704
  * Donato et al. (1998) Donato F., Fornengo N., Scopel S., 1998, Astroparticle Physics, 9, 247
  * Dootson & Magorrian (2022) Dootson D., Magorrian J., 2022, arXiv e-prints, p. arXiv:2205.15725
  * Doroshkevich (1970) Doroshkevich A. G., 1970, Astrophysics, 6, 320
  * Fermani & Schönrich (2013) Fermani F., Schönrich R., 2013, MNRAS, 432, 2402
  * Fouvry & Pichon (2015) Fouvry J.-B., Pichon C., 2015, MNRAS, 449, 1982
  * Friske & Schönrich (2023) Friske J. K. S., Schönrich R., 2023, arXiv e-prints, p. arXiv:2310.01899
  * Fujii et al. (2019) Fujii M. S., Bédorf J., Baba J., Portegies Zwart S., 2019, MNRAS, 482, 1983
  * Gherghinescu et al. (2023) Gherghinescu P., Das P., Grand R. J. J., Orkney M. D. A., 2023, arXiv e-prints, p. arXiv:2307.09963
  * Green (2001) Green A. M., 2001, Phys. Rev. D, 63, 043005
  * Hamilton et al. (2022) Hamilton C., Tolman E. A., Arzamasskiy L., Duarte V. N., 2022, arXiv e-prints, p. arXiv:2208.03855
  * Hernquist (1990) Hernquist L., 1990, ApJ, 356, 359
  * Heyvaerts et al. (2017) Heyvaerts J., Fouvry J.-B., Chavanis P.-H., Pichon C., 2017, MNRAS, 469, 4193
  * Jaffe (1983) Jaffe W., 1983, MNRAS, 202, 995
  * Jiang et al. (2019) Jiang F., et al., 2019, MNRAS, 488, 4801
  * Kalnajs (1977) Kalnajs A. J., 1977, ApJ, 212, 637
  * Kamionkowski & Kinkhabwala (1998) Kamionkowski M., Kinkhabwala A., 1998, Phys. Rev. D, 57, 3256
  * Kataria & Shen (2022) Kataria S. K., Shen J., 2022, ApJ, 940, 175
  * Klypin et al. (2011) Klypin A. A., Trujillo-Gomez S., Primack J., 2011, ApJ, 740, 102
  * Kuijken & Dubinski (1994) Kuijken K., Dubinski J., 1994, MNRAS, 269, 13
  * Landau (1946) Landau L. D., 1946, J. Phys. USSR, 10
  * Launhardt et al. (2002) Launhardt R., Zylka R., Mezger P. G., 2002, A&A, 384, 112
  * Liao et al. (2017) Liao S., Chen J., Chu M. C., 2017, ApJ, 844, 86
  * Lichtenberg & Lieberman (1992) Lichtenberg A., Lieberman M., 1992, Regular and Chaotic Dynamics. Springer-Verlag
  * Long et al. (2014) Long S., Shlosman I., Heller C., 2014, ApJ, 783, L18
  * Lynden-Bell (1960) Lynden-Bell D., 1960, MNRAS, 120, 204
  * Lynden-Bell (1979) Lynden-Bell D., 1979, MNRAS, 187, 101
  * Lynden-Bell & Kalnajs (1972) Lynden-Bell D., Kalnajs A. J., 1972, MNRAS, 157, 1
  * Maller et al. (2002) Maller A. H., Dekel A., Somerville R., 2002, MNRAS, 329, 423
  * Matsunaga et al. (2015) Matsunaga N., et al., 2015, ApJ, 799, 46
  * Murali (1999) Murali C., 1999, ApJ, 519, 580
  * Navarro et al. (1997) Navarro J. F., Frenk C. S., White S. D. M., 1997, ApJ, 490, 493
  * Obreja et al. (2022) Obreja A., Buck T., Macciò A. V., 2022, A&A, 657, A15
  * Peebles (1969) Peebles P. J. E., 1969, ApJ, 155, 393
  * Peebles (1971) Peebles P. J. E., 1971, A&A, 11, 377
  * Petersen et al. (2016) Petersen M. S., Weinberg M. D., Katz N., 2016, MNRAS, 463, 1952
  * Pichon & Cannon (1997) Pichon C., Cannon R. C., 1997, MNRAS, 291, 616
  * Rozier et al. (2019) Rozier S., Fouvry J. B., Breen P. G., Varri A. L., Pichon C., Heggie D. C., 2019, MNRAS, 487, 711
  * Rozier et al. (2022) Rozier S., Famaey B., Siebert A., Monari G., Pichon C., Ibata R., 2022, ApJ, 933, 113
  * Saha & Naab (2013) Saha K., Naab T., 2013, MNRAS, 434, 1287
  * Sanders et al. (2023) Sanders J. L., Kawata D., Matsunaga N., Sormani M. C., Smith L. C., Minniti D., Gerhard O., 2023, arXiv e-prints, p. arXiv:2311.00035
  * Schönrich et al. (2015) Schönrich R., Aumer M., Sale S. E., 2015, ApJ, 812, L21
  * Sormani & Barnes (2019) Sormani M. C., Barnes A. T., 2019, MNRAS, 484, 1213
  * Sormani et al. (2022) Sormani M. C., et al., 2022, MNRAS, 512, 1857
  * Tremaine & Weinberg (1984) Tremaine S., Weinberg M. D., 1984, MNRAS, 209, 729
  * Villa-Vargas et al. (2010) Villa-Vargas J., Shlosman I., Heller C., 2010, ApJ, 719, 1470
  * Vitvitska et al. (2002) Vitvitska M., Klypin A. A., Kravtsov A. V., Wechsler R. H., Primack J. R., Bullock J. S., 2002, ApJ, 581, 799
  * Weinberg (1985) Weinberg M. D., 1985, MNRAS, 213, 451
  * Weinberg (1989) Weinberg M. D., 1989, MNRAS, 239, 549
  * Weinberg (1991) Weinberg M. D., 1991, ApJ, 368, 66
  * Weinberg (2004) Weinberg M. D., 2004, arXiv e-prints, pp astro–ph/0404169
  * Weinberg & Katz (2007) Weinberg M. D., Katz N., 2007, MNRAS, 375, 425
  * White (1984) White S. D. M., 1984, ApJ, 286, 38
  * White & Rees (1978) White S. D. M., Rees M. J., 1978, MNRAS, 183, 341
  * Widrow & Dubinski (2005) Widrow L. M., Dubinski J., 2005, ApJ, 631, 838
  * Zjupa & Springel (2017) Zjupa J., Springel V., 2017, MNRAS, 466, 1625

##  Appendix A Distribution of angular momentum in the Galactic meridian plane

Figure 9: Mean angular momentum of spinning dark halos in the meridian plane
($r,\vartheta$). Top panel: Empirical model by Liao et al. (2017) based on
cosmological simulation. Middle panel: Our model with a spin function $g$
depending on the ratio $L_{z}/L$ (equation 4). Bottom panel: Model with $g$
depending only on $L_{z}$ (equation 5).

In Section 2, we compared the two models of spinning dark halos (equations 4
and 5) by observing the angular momentum averaged over spherical shells as a
function of radius. Here, we take the comparison a step further and look into
the angular momentum averaged over azimuthal rings as a function of radius $r$
and polar angle $\vartheta$.

Liao et al. (2017) analyzed the dark halos in the Bolshoi cosmological
simulation (Klypin et al., 2011) and found that the distribution of angular
momentum in the $(r,\vartheta)$ plane can be fitted with the following
empirical function

$\displaystyle\bar{L}_{z}(r,\vartheta)=j_{\rm s}\frac{(\tilde{r}/r_{\rm
s})^{2}}{(1+\tilde{r}/r_{\rm s})^{4}}\sin^{2}(\vartheta/\vartheta_{\rm s}),$
(11)

where $\tilde{r}\equiv r/r_{\rm vir}$, and $j_{\rm s}$, $r_{\rm s}$, and
$\vartheta_{\rm s}$ are free parameters. They fit this function to multiple
dark halos and derived the scaling relation between the parameters and the
virial mass of the halo.

Fig. 9 top panel shows the distribution of $\bar{L}_{z}$ from their empirical
model using the virial mass of our Galaxy ($M_{\rm vir}=1.5\times
10^{12}\,{\rm M}_{\odot}$). The distribution is skewed towards the equatorial
plane, which is naturally expected as $L_{z}$ is largest when the angular-
momentum vector is aligned with the $z$ axis.

The middle panel shows $\bar{L}_{z}$ of our spinning halo model (equation 4)
obtained by Monte Carlo integration. The distribution is surprisingly similar
to the empirical model proposed by Liao et al. (2017). The absolute value of
$\bar{L}_{z}$ is much higher than their model since we set $\Lambda=1$. A
quantitative match would require $\Lambda\sim 0.06$.

The bottom panel shows $\bar{L}_{z}$ of the spinning halo with a universal
scale for the spin function $g$ (equation 5). Compared to our model as well as
that of Liao et al. (2017), the distribution depends more on the radial
distance from the $z$ axis (i.e. $R=r\sin\vartheta$) rather than the polar
angle $\vartheta$. This reflects the fact that the spin function $g$ in this
model depends only on $L_{z}$, which sets the range of $R$ an orbit can
explore: the smaller the $L_{z}$, the smaller the minimum $R$ an orbit may
reach. In contrast, $g$ in our model is a function of the orbital inclination
$\beta$, which determines the orbital range in $\vartheta$.

##  Appendix B Singular isothermal sphere

Figure 10: LBK torque as a function of the halo’s spin $\Lambda$ in a singular
isothermal sphere.

In this section, we repeat the calculation of the LBK formula using the
singular isothermal sphere, which was employed in Weinberg (1985). The
singular isothermal sphere has the following density and potential:

$\displaystyle\rho(r)=\frac{M_{\rm s}}{4\pi r_{\rm
s}r^{2}},~{}~{}~{}~{}\Phi(r)=\frac{GM_{\rm s}}{r_{\rm
s}}\ln\left(\dfrac{r}{r_{\rm s}}\right),$ (12)

where $M_{\rm s}$ is the mass enclosed within $r_{\rm s}$. The isothermal
sphere has a flat rotation curve $v_{\rm c}=\sqrt{GM_{\rm s}/r_{\rm s}}$ and a
uniform velocity dispersion $\sigma=v_{\rm c}/\sqrt{2}$, hence the name. The
circular speed $v_{\rm c}$ is the single independent parameter of the model,
and we set this to $235\,{\rm km}\,{\rm s}^{-1}$. The distribution function is
$f(E)\propto\exp(-E/\sigma^{2})$. Since the isothermal sphere has an infinite
mass, we truncate the distribution at $E_{\rm max}=\Phi(r_{\rm max})$ where
$r_{\rm max}=10^{3}\,{\rm kpc}$.

Fig. 10 plots the torque on the bar by the singular isothermal sphere. Similar
to the Hernquist halo, the total dynamical friction weakens with the halo’s
spin $\Lambda$, suggesting that the discrepancy between our calculation and
that of Weinberg (1985) is not due to the difference in the halo’s density
profile. The relative contribution from each resonance is, however, different
from the Hernquist model. In particular, the inner Lindblad resonance [ILR,
${\bm{n}}=(-1,2,2)$] now dominates the torque. This is because the isothermal
sphere has a higher concentration of mass in the inner region, which raises
the orbital frequencies there and thus allows the ILR to expand and cover a
larger phase space. We caution though that, while the isothermal sphere places
the ILR at a realistic position, the mass of dark matter in the inner region
near the ILR is significantly overestimated. A proper quantification of the
relative importance of each resonance will require a model for the
distribution function of the dark halo in equilibrium under the combined
potential of the halo and the disk.

We also explored other double power-law models $\rho\propto
r^{-\gamma}(r+r_{\rm s})^{\gamma-\eta}$, in particular, the truncated NFW
model $(\gamma=1,\eta=3)$ and the Jaffe (1983) model $(\gamma=2,\eta=4)$ but
found similar results. The former yielded results closer to those of the
Hernquist model $(\gamma=1,\eta=4)$, while the latter was closer to the
singular isothermal sphere $(\gamma=2,\eta=2)$, indicating that dynamical
friction depends mainly on the density slope at the inner region $\alpha$,
where the main resonances reside.

##  Appendix C Varying the location of discontinuity

Figure 11: The spin function $g$ (equation 13) corresponding to the Weinberg’s
rotating halo model.

In this paper, we adopted a spinning halo model in which the DF assumes the
largest gradient in $L_{z}$ at $L_{z}=0$ (Section 4.1). In this section, we
check whether our conclusion holds also for spinning models with large
gradients (in particular, discontinuities) in $L_{z}$ away from the origin.
Such a model was in fact used by Weinberg (1985), who set the halo rotating by
reversing retrograde orbits with $\pi/2(2-x)\leq\beta\leq\pi$ where $0\leq
x\leq 1$ and $\beta=\cos^{-1}(L_{z}/L)$ is the orbital inclination. Taking the
cosine, the range transforms to $-1\leq L_{z}/L\leq-a$ where
$a\equiv-\cos\left[\pi/2(2-x)\right]\geq 0$. Reversing orbits in this range is
equivalent to setting the odd DF $g$ (equation 2) as

$\displaystyle
g(L,L_{z})=\Lambda\left[\Theta(L_{z}/L-a)+\Theta(L_{z}/L+a)-1\right],$ (13)

where $\Theta$ is the Heaviside step function. We plot this function in Fig.
11. The function has two discontinuities at $L_{z}/L=\pm a$. In the limit
$a=0$, the two discontinuities merge, and the function reduces to equation
(3).

Figure 12: The LBK torque by an isothermal sphere with two discontinuities
away from the origin (equation 13).

Fig. 12 shows the LBK torque by the isothermal sphere set rotating using
equation (13). We find that, regardless of $a$, dynamical friction on the bar
decreases with $\Lambda$. Interestingly, the impact of the halo’s spin first
increases with $a$. This is because increasing $a$ shifts the two
discontinuities to $\beta=0$ and $\pi$ respectively, so the positive torque
due to the discontinuities (i.e. $\tau_{g}$) by the $n_{\psi}=\pm 2$
resonances increases. Beyond $a\sim 0.5$, however, the slope begins to flatten
because the range of orbits reversed in motion becomes narrower. The impact of
the halo’s spin vanishes at $a=1$ where there is no net rotation.


§ NORMALIZATION RESULTS

We consider the special case of <ref> where
\(\model\) is the initial model \(\workingInitModel\) of
\(\workingtth\) and \(\fun\) is the initial renaming model
\(\workingRenCounit : \workingRenModel \to \workingInitModel\). In this
case, we omit the subscript \({}_{\workingRenCounit}\) and simply
write \(\workingLogos = \workingLogos_{\workingRenCounit}\),
\(\workingNmModel = \workingNmModel_{\workingRenCounit}\), and so
on. The goal of this section is to show that \(\workingLogos\)
validates the following propositions.

\begin{align}
\label{eq:isnfty-contractible}
\begin{autobreak}
\MoveEqLeft
\ilForall_{\ty : \workingTyTmStr}
\ilIsContr(\ilIsNfTy_{\workingNfalg}(\ty))
\end{autobreak}
\\
\label{eq:isnftm-contractible}
\begin{autobreak}
\MoveEqLeft
\ilForall_{\ty : \workingTyTmStr}
\ilForall_{\tm : \ty}
\ilIsContr(\ilIsNfTm_{\workingNfalg}(\tm))
\end{autobreak}
\end{align}

That is, every type or term has a unique normal form. Note that the
initiality of \(\workingInitModel\) or \(\workingRenModel\) is not
visible in the internal language of \(\workingLogos\). Therefore, we
have to do some external reasoning first and then embed
\(\workingLogos\) into another \(\infty\)-logos to internalize necessary

§.§ Semantic setup

By the initiality of \(\workingInitModel\), we have a unique section
\(\workingSection : \workingInitModel \to \workingNmModel\) of
\(\workingNmProj : \workingNmModel \to \workingInitModel\). The
relative induction principle of bocquet2021relative
ensures that \(\workingSection\) is also related to
\(\workingRenCounit : \workingRenModel \to \workingInitModel\) and
\(\workingRenIncNm : \Ctx(\workingRenModel) \to \Ctx(\workingNmModel)\).

One can construct a natural transformation

\begin{equation*}
\workingTrans : \workingRenIncNm \To \workingSection_{\Ctx} \comp
\workingRenCounit_{\Ctx} : \Ctx(\workingRenModel) \to \Ctx(\workingNmModel)
\end{equation*}

over \(\Ctx(\workingInitModel)\). Moreover, the composite

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\Tm(\workingRenModel)
\xrightarrow{\workingRenCounit_{\Tm}} \workingRenCounit_{\Ctx}^{\pbMark} \Tm(\workingInitModel)
\xrightarrow{\workingRenCounit_{\Ctx}^{\pbMark} \workingSection_{\Tm}} \workingRenCounit_{\Ctx}^{\pbMark} \workingSection_{\Ctx}^{\pbMark} \Tm(\workingNmModel)
\xrightarrow{\workingTrans^{\pbMark}} \workingRenIncNm^{\pbMark} \Tm(\workingNmModel)
\end{autobreak}
\end{align*}

is equivalent over
\(\workingRenIncNm^{\pbMark} \Ty(\workingNmModel)
\times_{\workingRenCounit_{\Ctx}^{\pbMark} \Ty(\workingInitModel)}
\workingRenCounit_{\Ctx}^{\pbMark} \Tm(\workingInitModel)\) to the

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\Tm(\workingRenModel)
\xrightarrow{(\workingTrans^{\pbMark} \comp \workingRenCounit_{\Ctx}^{\pbMark} \workingSection_{\Ty}, \id)} \workingRenIncNm^{\pbMark} \Ty(\workingNmModel) \times_{\workingRenCounit_{\Ctx}^{\pbMark} \Ty(\workingInitModel)} \Tm(\workingRenModel)
\xrightarrow{\workingVarToTm} \workingRenIncNm^{\pbMark} \Tm(\workingNmModel).
\end{autobreak}
\end{align*}

The proof of <ref> is essentially the
same as the \(1\)-categorical case bocquet2021relative and
given in <ref>.

We now have the following diagram.

\begin{equation}
\label{eq:working-logos-1-diagram}
\begin{tikzcd}[column sep=0ex]
& \Ctx(\workingNmModel)
\arrow[dr, equal] \\
\Ctx(\workingRenModel)
\arrow[ur, "\workingRenIncNm"]
\arrow[rr, "\workingSection_{\Ctx} \comp \workingRenCounit_{\Ctx}"{description},
"{\phantom{a}}"{name = a0}, "{\phantom{a}}"'{name = a1}]
\arrow[dr, "\workingRenCounit_{\Ctx}"'] &
\arrow[from = u, to = a0, To, "\workingTrans",
start anchor = {[yshift = -1ex]}]
\arrow[from = a1, to = d, phantom, "\simeq"{description}] &
\Ctx(\workingNmModel)
\arrow[r, "\workingNmProj_{\Ctx}"] &
\Ctx(\workingInitModel) \\
& \Ctx(\workingInitModel)
\arrow[ur, "\workingSection_{\Ctx}"']
\end{tikzcd}
\end{equation}

Let \(\workingMSI\) be the mode sketch

\begin{equation*}
\begin{tikzcd}[row sep = 3ex]
& 2'
\arrow[dr] \\
\arrow[ur]
\arrow[rr, "\phantom{a}"{name = a0},
"\phantom{a}"'{name = a1}]
\arrow[dr] &
\arrow[from = u, to = a0, To, start anchor = {[yshift = -1ex]}]
\arrow[from = d, to = a1, phantom, "\simeq"{description}, end anchor = {[yshift = 1ex]}]&
\arrow[r] &
1 \\
& 3
\arrow[ur]
\end{tikzcd}
\end{equation*}

where only \((0 < 2' < 2)\) is not thin. Then
<ref> is a functor
\(\workingLogosIBase : \realize{\workingMSI} \to \Cat^{\nMark{2}}\), and
our second working \(\infty\)-logos \(\workingLogosI\) is
\(\Fun(\realize{\workingMSI}, \RFib)_{\workingLogosIBase}\).

§.§ Axiomatic setup

A function \(\mode : \workingMSI \to \ilLAM\) satisfying
<ref> is
postulated. We define \(\modeRen \defeq \mode(0)\),
\(\modeSyn \defeq \mode(1)\), \(\modeNm \defeq \mode(2)\),
\(\modeNmI \defeq \mode(2')\), and \(\modeSect \defeq \mode(3)\).

By construction, the  \(\modeRen \lor \modeSyn\) corresponds
to the previous \(\infty\)-logos \(\workingLogos\). Therefore, we may
assume all the previous results.

<ref>. <Ref>
are assumed.

<ref>. A
\(\modeRen\)-modal displayed \(\workingtth\)-type-term structure
\(\workingNmDTyTmStr\) over \(\workingTyTmStr\) is postulated, and
it is assumed to have a \(\workingNfalg\)-normalization structure
supporting \(\workingtth\).

Corresponding to the diagram

we have a \((\modeSect \lor \modeNm \lor \modeSyn)\)-modal
\(\workingtth\)-type-term structure whose \(\modeSyn\)-component is
\(\workingTyTmStr\). Since
\(\workingNmProj \comp \workingSection \simeq \id\), the
\((\modeSect \lor \modeSyn)\)-component of the \(\workingtth\)-type-term
structure is \(\modeSyn\)-modal. Furthermore, the functor
\(\opMode^{\modeSect \lor \modeNm \lor \modeSyn}_{\modeSect} :
\ilUniv_{\modeSect \lor \modeNm \lor \modeSyn} \to \ilUniv_{\modeSect}\)
preserves dependent function types indexed over the terms in the
\(\workingtth\)-type-term structure by <ref>. It is then
fractured into the following structures

<ref>. A
\(\modeNm\)-modal displayed \(\workingtth\)-type-term structure
\(\workingNmModelIn\) over \(\workingTyTmStr\) is postulated.

Let \(\tytmstrI\) be a displayed \(\workingtth\)-type-term structure over a
\(\workingtth\)-type-term structure \(\tytmstr\). The notion of a
presection of \(\tytmstrI\) is defined by the logical
relation translation of the notion of a \(\workingtth\)-type-term structure
with respect to the inverse category \(\neord[2]\). Concretely, a
presection \(\sect\) of \(\tytmstrI\) consists of

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilTy^{\neord[2]}_{\sect} :
\ilForall_{\implicit{\ty}}
\tytmstrI(\ty)
\to \ilUniv
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilTm^{\neord[2]}_{\sect} :
\ilForall_{\implicit{\ty}}
\ilForall_{\implicit{\tyI : \tytmstrI(\ty)}}
\ilTy^{\neord[2]}_{\sect}(\tyI)
\to \ilForall_{\implicit{\tm}}
\tyI(\tm)
\to \ilUniv
\end{autobreak}
\end{align*}

and operators depending on the presentation of \(\workingtth\). We regard
\(\sect \mapsto \ilTy^{\neord[2]}_{\sect}\) and
\(\ilTm^{\neord[2]}_{\sect}\) as implicit coercions.

Let \(\mode_{0}\), \(\mode_{1}\), \(\mode_{2}\) be  such
that \(\mode_{\idx} \le {}^{\orthMark} \mode_{\idxI}\) for all
\(\idx < \idxI\). Let \(\tytmstr\) be a \(\mode_{2}\)-modal
type-term structure, \(\tytmstrI\) a \(\mode_{1}\)-modal displayed
type-term structure over \(\tytmstr\), and \(\sect\) a
\(\mode_{0}\)-modal presection of \(\tytmstrI\). We say \(\sect\) is
a section if the type
\(\opMode_{\mode_{0}}(\ilExists_{\tyI :
\tytmstrI(\ty)}\sect(\tyI))\) is contractible for any
\(\ty : \tytmstr\) and if the type
\(\opMode_{\mode_{0}}(\ilExists_{\tmI : \tyI(\tm)}\tyII(\tmI))\) is
contractible for any \(\tyI : \tytmstrI(\ty)\),
\(\tyII : \sect(\tyI)\), and \(\tm : \ty\).

<ref>. A
\(\modeSect\)-modal section \(\workingSectionIn\) of
\(\workingNmModelIn\) is postulated.

<ref>. For
any \(\ty : \workingTyTmStr\), \(\tyI : \workingNmModelIn(\ty)\),
\(\tyII : \workingSectionIn(\tyI)\), and

: _: _: ()() →_,

the canonical map

\begin{equation*}
\opMode_{\modeSect}(\ilForall_{\tm}\ilForall_{\tmI}\ilForall_{\tmII}\tyX(\tm, \tmI, \tmII))
\to (\ilForall_{\tm}\ilForall_{\tmI}\ilForall_{\tmII}\opMode_{\modeSect} \tyX(\tm, \tmI, \tmII))
\end{equation*}

is assumed to be an equivalence.

Let \(\sect\) be a section as in <ref>. We
have the actions of \(\sect\) on types and terms

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTy_{1}}(\sect) :
\ilForall_{\ty : \tytmstr}
\opMode_{\mode_{0}} \tytmstrI(\ty)
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTm_{1}}(\sect) :
\ilForall_{\implicit{\ty : \tytmstr}}
\ilForall_{\tm : \ty}
\ilSectApp_{\ilTy_{1}}(\sect, \ty)(\tm)
\end{autobreak}
\end{align*}

by taking the center of contraction, where
\(\ilTm^{\neord[1]}_{\tytmstrI}(\ty) : \tytmstrI(\ty) \to \ty \to
\ilUniv\) induces a function
\(\opMode_{\mode_{0}} \tytmstrI(\ty) \to \ty \to \ilUniv_{\mode_{0}}\)
by which we regard \(\ilSectApp_{\ilTm_{1}}(\sect, \ty)\) as a
function \(\ty \to \ilUniv_{\mode_{0}}\).

To axiomatize the equivalence

^ ≃,

recall from <ref> that
natural transformations cartesian on representable maps correspond to
cartesian morphisms between type-term structures. Cartesian morphisms
between displayed type-term structures are similarly defined. Since a
natural equivalence is in particular cartesian on representable maps,
we have the following.

<ref>. A
\(\modeNmI\)-modal displayed \(\workingtth\)-type-term structure
\(\workingNmModelInI\) over \(\workingTyTmStr\) and a cartesian
morphism \(\workingCorr\) from \(\workingNmModelIn\) to
\(\workingNmModelInI\) are postulated.

<ref>. A
cartesian morphism \(\workingCorrI\) from \(\workingNmModelInI\) to
\(\workingNmDTyTmStr\) is postulated.

\(\workingCorr\) is interpreted as the identity on
\(\workingNmModel\). This is introduced merely because the language
of mode sketch is restrictive.

We can now internally construct a section of \(\workingNmDTyTmStr\).

<ref>. For
any \(\ty : \workingTyTmStr\), we define

__1^(, )
: ()

\begin{align*}
\begin{autobreak}
\ilUnit
\xrightarrow{\ilSectApp_{\ilTy_{1}}(\workingSectionIn, \ty)} \opMode^{\modeNm}_{\modeSect} \workingNmModelIn(\ty)
\xrightarrow{\unitMode_{\modeRen}} \opMode^{\modeSect}_{\modeRen} \opMode^{\modeNm}_{\modeSect} \workingNmModelIn(\ty)
\simeq \opMode^{\modeNm}_{\modeRen} \workingNmModelIn(\ty)
\xrightarrow{\unitMode^{\modeRen; \modeNm}_{\modeNmI}} \opMode^{\modeNmI}_{\modeRen} \opMode^{\modeNm}_{\modeNmI} \workingNmModelIn(\ty)
\xrightarrow{\opMode^{\modeNmI}_{\modeRen} \ilCorrApp_{\ilTy_{1}}(\workingCorr)} \opMode^{\modeNmI}_{\modeRen} \workingNmModelInI(\ty)
\xrightarrow{\ilCorrApp_{\ilTy_{1}}(\workingCorrI)} \workingNmDTyTmStr(\ty).
\end{autobreak}
\end{align*}

We can similarly define
\(\ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm) :
\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty)(\tm)\) for
any \(\tm : \ty\).

Finally, we internalize the second half of

<ref>. An

__1^(, ) = (, _)

is postulated for any \(\ty : \workingTyTmStr\), \(\var : \ty\), and
\(\var_{\varMark} : \ilIsVar(\var)\).

§.§ Normalization functions

We work in type theory.

<ref>. We
define normalization functions

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilNormalize_{\ilTy} :
\ilForall_{\ty : \workingTyTmStr}
\ilIsNfTy_{\workingNfalg}(\ty)
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilNormalize_{\ilTm} :
\ilForall_{\implicit{\ty : \workingTyTmStr}}
\ilForall_{\tm : \ty}
\ilIsNfTm_{\workingNfalg}(\tm)
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilNormalize_{\ilTy}(\ty) \defeq
\ilnfty(\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty))
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilNormalize_{\ilTm}(\tm) \defeq
\ilreify(\blank, \ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm)).
\end{autobreak}
\end{align*}

<ref>. We
define predicates

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilIsNfTy^{\neord[1]}_{\workingUniqPred} :
\ilForall_{\implicit{\ty : \workingTyTmStr}}
\ilIsNfTy_{\workingNfalg}(\ty)
\to \ilUniv_{\modeRen}
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilIsNfTm^{\neord[1]}_{\workingUniqPred} :
\ilForall_{\implicit{\ty : \workingTyTmStr}}
\ilForall_{\implicit{\tm : \ty}}
\ilIsNfTm_{\workingNfalg}(\tm)
\to \ilUniv_{\modeRen}
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilIsNeTm^{\neord[1]}_{\workingUniqPred} :
\ilForall_{\implicit{\ty : \workingTyTmStr}}
\ilForall_{\implicit{\tm : \ty}}
\ilIsNeTm_{\workingNfalg}(\tm)
\to \ilUniv_{\modeRen}
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilIsNfTy^{\neord[1]}_{\workingUniqPred}(\ty_{\nftyMark}) \defeq
(\ilNormalize_{\ilTy}(\ty) = \ty_{\nftyMark})
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilIsNfTm^{\neord[1]}_{\workingUniqPred}(\tm_{\nftmMark}) \defeq
(\ilNormalize_{\ilTm}(\tm) = \tm_{\nftmMark})
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilIsNeTm^{\neord[1]}_{\workingUniqPred}(\tm_{\netmMark}) \defeq
(\ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm) = \ilreflect(\blank, \tm_{\netmMark})).
\end{autobreak}
\end{align*}

We want to show that \(\ilIsNfTy^{\neord[1]}_{\workingUniqPred}\),
\(\ilIsNfTm^{\neord[1]}_{\workingUniqPred}\), and
\(\ilIsNeTm^{\neord[1]}_{\workingUniqPred}\) are part of a
displayed \(\workingtth\)-normal form algebra \(\workingUniqPred\) over
\(\workingNfalg\) supporting variables, which is defined by the
logical relation translation with respect to the inverse category
\(\neord[1]\), so that it admits a section by the initiality of
\(\workingNfalg\).

<ref>. Then
\(\workingUniqPred\) supports variables in the sense that we have a

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilForall_{\ty : \workingTyTmStr}
\ilForall_{\var : \ty}
\ilForall_{\var_{\varMark} : \ilIsVar(\var)}
\ilIsNeTm^{\neord[1]}_{\workingUniqPred}(\ilVarToNe(\var_{\varMark})).
\end{autobreak}
\end{align*}

By the definition of \(\ilVarToTm\) and

<ref>. Show
that \(\workingUniqPred\) is a displayed \(\workingtth\)-normal form
algebra over \(\workingNfalg\).

We have not used <ref> explicitly. This
axiom is needed in <ref> when
\(\workingtth\) has operators with variable binding such as
dependent function types and lambda abstraction; see
<ref> below.

§.§ Normalization results

Suppose we have done <ref> and assume
in type theory. By
<ref> and
by the initiality of \(\workingNfalg\), we have a section of
\(\workingUniqPred\). By definition, this shows that the propositions
eq:isnfty-contractible,eq:isnftm-contractible are
inhabited with centers \(\ilNormalize_{\ilTy}(\ty)\) and
\(\ilNormalize_{\ilTm}(\tm)\), respectively.

Apply the results to the \(\infty\)-logos \(\workingLogosI\). Since
<ref> are defined in
the universe \(\ilUniv_{\modeRen \lor \modeSyn}\) which corresponds to
the full subcategory \(\workingLogos \subset \workingLogosI\), it follows
that \(\workingLogos\) also validates

§.§ Running example

We consider the case when \(\workingtth =
\basicTT_{\FunMark}\). Before doing
<ref>, we extract more components
from the section \(\workingSectionIn\). <Ref>
shows that the section \(\workingSectionIn\) acts on types and
terms. We can show that it also acts on families of types and
terms. This is where we need <ref>.

<ref>. Then
the type

\begin{align*}
\begin{autobreak}
\opMode_{\modeSect}(\ilExists_{\tyI_{\modeNm} : \ilForall_{\tm_{\modeSyn}}\ty_{\modeNm}(\tm_{\modeSyn}) \to \workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn}))}
\ilForall_{\tm_{\modeSyn}}
\ilForall_{\tm_{\modeNm}}
\ty_{\modeSect}(\tm_{\modeNm})
\to \workingSectionIn(\tyI_{\modeNm}(\tm_{\modeSyn}, \tm_{\modeNm})))
\end{autobreak}
\end{align*}

is contractible for any \(\ty_{\modeSyn} : \workingTyTmStr\),
\(\ty_{\modeNm} : \workingNmModelIn(\ty_{\modeSyn})\),
\(\ty_{\modeSect} : \workingSectionIn(\ty_{\modeNm})\),
and \(\tyI_{\modeSyn} : \ty_{\modeSyn} \to \workingTyTmStr\).

We have

\begin{align*}
& \term{\opMode_{\modeSect}(\ilExists_{\tyI_{\modeNm} : \ilForall_{\tm_{\modeSyn}}\ty_{\modeNm}(\tm_{\modeSyn}) \to \workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn}))}\ilForall_{\tm_{\modeSyn}}\ilForall_{\tm_{\modeNm}}\ty_{\modeSect}(\tm_{\modeNm}) \to \workingSectionIn(\tyI_{\modeNm}(\tm_{\modeSyn}, \tm_{\modeNm})))} \\
\simeq & \by{\(\workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn})) \simeq (\ty_{\modeSect}(\tm_{\modeNm}) \to \workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn})))\) since \(\modeSect \le {}^{\orthMark}\modeNm\)} \\
& \term{\opMode_{\modeSect}(\ilExists_{\tyI_{\modeNm} : \ilForall_{\tm_{\modeSyn}}\ilForall_{\tm_{\modeNm} : \ty_{\modeNm}(\tm_{\modeSyn})}\ty_{\modeSect}(\tm_{\modeNm}) \to \workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn}))}\ilForall_{\tm_{\modeSyn}}\ilForall_{\tm_{\modeNm}}\ilForall_{\tm_{\modeSect}}\workingSectionIn(\tyI_{\modeNm}(\tm_{\modeSyn}, \tm_{\modeNm}, \tm_{\modeSect})))} \\
\simeq & \by{\(\ilForall\) distributes over \(\ilExists\)} \\
& \term{\opMode_{\modeSect}(\ilForall_{\tm_{\modeSyn}}\ilForall_{\tm_{\modeNm} : \ty_{\modeNm}(\tm_{\modeSyn})}\ty_{\modeSect}(\tm_{\modeNm}) \to \ilExists_{\tyI_{\modeNm} : \workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn}))}\workingSectionIn(\tyI_{\modeNm}))} \\
\simeq & \by{\cref{axm:working-logos-2-tiny}} \\
& \term{\ilForall_{\tm_{\modeSyn}}\ilForall_{\tm_{\modeNm} : \ty_{\modeNm}(\tm_{\modeSyn})}\ty_{\modeSect}(\tm_{\modeNm}) \to \opMode_{\modeSect}(\ilExists_{\tyI_{\modeNm} : \workingNmModelIn(\tyI_{\modeSyn}(\tm_{\modeSyn}))}\workingSectionIn(\tyI_{\modeNm}))},
\end{align*}

and the last type is contractible since \(\workingSectionIn\) is a

By taking the center of contraction, we can see that
\(\workingSectionIn\) acts on families of types and similarly on
families of …of families of types/terms. Since
\(\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn)\)
(<ref>) is essentially the
composite of \(\ilSectApp_{\ilTy_{1}}(\workingSectionIn)\),
\(\ilCorrApp_{\ilTy_{1}}(\workingCorr)\), and
\(\ilCorrApp_{\ilTy_{1}}(\workingCorrI)\), it is also extended to a
function on families of …of families of types/terms. For the
record, we have functions such as

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn) :
\ilForall_{\implicit{\ty : \workingTyTmStr}}
\ilForall_{\tyI : \ty \to \workingTyTmStr}
\ilForall_{\implicit{\tm}}
\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty)(\tm)
\to \workingNmDTyTmStr(\tyI(\tm))
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTm_{2}}^{\modeRen}(\workingSectionIn) :
\ilForall_{\implicit{\ty : \workingTyTmStr}}
\ilForall_{\implicit{\tyI : \ty \to \workingTyTmStr}}
\ilForall_{\tmI : \ilForall_{\tm}\tyI(\tm)}
\ilForall_{\implicit{\tm}}
\ilForall_{\tm_{0} : \ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty)(\tm)}
\ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI, \tm_{0})(\tmI(\tm)).
\end{autobreak}
\end{align*}

Moreover, these commute with structural operators such as substitution
and respect all type-theoretic structures, for example

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \tyI(\tm)) =
\ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI)(\ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm))
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ilFun(\ty, \tyI)) =
\ilFun^{\neord[1]}(\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty), \ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI)).
\end{autobreak}
\end{align*}

These functions and identifications are part of an infinite
coherent structure. Our finite set of axioms allows us to
extract arbitrarily many components of that structure.

In the equational reasonings below, many transport functions are
omitted for readability. Some expressions may be even ill-formed but
can be fixed by inserting appropriate transport functions.

Case \(\ilFun_{\nftyMark}(\ty_{\nftyMark}, \tyI_{\nftyMark})\)

Let \(\ty : \workingTyTmStr\),
\(\ty_{\nftyMark} : \ilIsNfTy_{\workingNfalg}(\ty)\),
\(\tyI : \ty \to \workingTyTmStr\), and
\(\tyI_{\nftyMark} : \ilForall_{\var}\ilIsVar(\var) \to
\ilIsNfTy_{\workingNfalg}(\tyI(\var))\), and suppose induction

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilNormalize_{\ilTy}(\ty) =
\ty_{\nftyMark}
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilForall_{\var}
\ilForall_{\var_{\varMark}}
\ilNormalize_{\ilTy}(\tyI(\var)) =
\tyI_{\nftyMark}(\var, \var_{\varMark}).
\end{autobreak}
\end{align*}

Then we have

\begin{align*}
& \term{\ilNormalize_{\ilTy}(\ilFun(\ty, \tyI))} \\
= & \by{definition} \\
& \term{\ilnfty(\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ilFun(\ty, \tyI)))} \\
= & \by{\(\workingSectionIn\) respects function types} \\
& \term{\ilnfty(\ilFun^{\neord[1]}(\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty), \ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI)))} \\
= & \by{definition} \\
& \term{\ilFun_{\nftyMark}(\ilnfty(\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \ty)),} \\
& \term{\quad\ilAbs \var \var_{\varMark}. \ilnfty(\ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI, \ilVarToTm(\blank, \var_{\varMark})))).}
\end{align*}

For the second argument of the last expression, we have

\begin{align*}
& \term{\ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI, \ilVarToTm(\blank, \var_{\varMark}))} \\
= & \by{\cref{axm:working-logos-2-var-to-tm}} \\
& \term{\ilSectApp_{\ilTy_{2}}^{\modeRen}(\workingSectionIn, \tyI, \ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \var))} \\
= & \by{\(\workingSectionIn\) commutes with substitution} \\
& \term{\ilSectApp_{\ilTy_{1}}^{\modeRen}(\workingSectionIn, \tyI(\var)).}
\end{align*}

Then, by the induction hypotheses, we conclude that

_((, )) =
_(_, _).

Case \(\ilabs_{\nftmMark}(\tmI_{\nftmMark})\)

Let \(\ty : \workingTyTmStr\), \(\tyI : \ty \to \workingTyTmStr\),
\(\tmI : \ilForall_{\tm}\tyI(\tm)\), and
\(\tmI_{\nftmMark} : \ilForall_{\var}\ilIsVar(\var) \to
\ilIsNfTm_{\workingNfalg}(\tmI(\var))\), and suppose induction

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilForall_{\var}
\ilForall_{\var_{\varMark}}
\ilNormalize_{\ilTm}(\tmI(\var)) =
\tmI_{\nftmMark}(\var, \var_{\varMark}).
\end{autobreak}
\end{align*}

Then we have

\begin{align*}
& \term{\ilNormalize_{\ilTm}(\ilabs(\tmI))} \\
= & \by{\(\workingSectionIn\) respects function types} \\
& \term{\ilreify(\blank, \ilabs^{\neord[1]}(\ilSectApp_{\ilTm_{2}}^{\modeRen}(\workingSectionIn, \tmI)))} \\
= & \by{definition} \\
& \term{\ilabs_{\nftmMark}(\ilAbs \var \var_{\varMark}. \ilreify(\blank, \ilSectApp_{\ilTm_{2}}^{\modeRen}(\workingSectionIn, \tmI, \ilVarToTm(\blank, \var_{\varMark}))))} \\
= & \by{\cref{axm:working-logos-2-var-to-tm}, and \(\workingSectionIn\) commutes with substitution} \\
& \term{\ilabs_{\nftmMark}(\ilAbs \var \var_{\varMark}. \ilreify(\blank, \ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tmI(\var))))} \\
= & \by{induction hypothesis} \\
& \term{\ilabs_{\nftmMark}(\tmI_{\nftmMark})}.
\end{align*}

Case \(\ilapp_{\netmMark}(\map_{\netmMark}, \tm_{\nftmMark})\)

Let \(\ty : \workingTyTmStr\), \(\tyI : \ty \to \workingTyTmStr\),
\(\map : \ilFun(\ty, \tyI)\),
\(\map_{\netmMark} : \ilIsNeTm_{\workingNfalg}(\map)\), \(\tm : \ty\),
and \(\tm_{\nftmMark} : \ilIsNfTm_{\workingNfalg}(\tm)\), and suppose
induction hypotheses

\begin{align*}
\begin{autobreak}
\MoveEqLeft
\ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \map) =
\ilreflect(\blank, \map_{\netmMark})
\end{autobreak}
\\
\begin{autobreak}
\MoveEqLeft
\ilNormalize_{\ilTm}(\tm) =
\tm_{\nftmMark}.
\end{autobreak}
\end{align*}

Then we have

\begin{align*}
& \term{\ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \ilapp(\map, \tm))} \\
= & \by{\(\workingSectionIn\) respects function types} \\
& \term{\ilapp^{\neord[1]}(\ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \map), \ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm))} \\
= & \by{induction hypothesis for \(\map_{\netmMark}\)} \\
& \term{\ilapp^{\neord[1]}(\ilreflect(\blank, \map_{\netmMark}), \ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm))} \\
= & \by{definition} \\
& \term{\ilreflect(\blank, \ilapp_{\netmMark}(\map_{\netmMark}, \ilreify(\blank, \ilSectApp_{\ilTm_{1}}^{\modeRen}(\workingSectionIn, \tm))))} \\
= & \by{induction hypothesis for \(\tm_{\nftmMark}\)} \\
& \term{\ilreflect(\blank, \ilapp_{\netmMark}(\map_{\netmMark}, \tm_{\nftmMark}))}.
\end{align*}

Other cases

The other cases are straightforward by similar calculation.