\pdfoutput=1
\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amsmath,amssymb,amsthm,mathtools,booktabs}
\usepackage{enumitem}
\usepackage[margin=1in]{geometry}
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
\hypersetup{pdftitle={Twisted conjugacy in spherical Artin groups and their crystallographic quotients},
 pdfauthor={Jason Davies}}
\emergencystretch=2em

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem*{mainthm}{Theorem A}
\newtheorem*{quotientthm}{Theorem B}
\newtheorem*{counterprop}{Proposition C}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\C}{\mathbb{C}}
\newcommand{\HH}{\mathbb{H}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\Aut}{\operatorname{Aut}}
\newcommand{\Out}{\operatorname{Out}}
\newcommand{\Inn}{\operatorname{Inn}}
\newcommand{\End}{\operatorname{End}}
\newcommand{\Sym}{\operatorname{Sym}}
\newcommand{\coker}{\operatorname{coker}}
\newcommand{\Gr}{\operatorname{Gr}}
\newcommand{\Rinf}{R_\infty}

\title{Twisted conjugacy in spherical Artin groups and their crystallographic quotients}
\author{Jason Davies\thanks{\href{mailto:jason@jasondavies.com}{\nolinkurl{jason@jasondavies.com}}}}
\date{November 10, 2026}

\begin{document}
\maketitle

\begin{abstract}
A group has property $\Rinf$ if every automorphism has infinitely many twisted conjugacy classes.
Let $A$ be an irreducible spherical Artin group of Coxeter rank at least two, with pure subgroup $P$.
We classify property $\Rinf$ for the crystallographic quotient $\Gamma=A/[P,P]$.
If $A$ has Coxeter rank at least three, then $\Gamma$ has $\Rinf$.
In type $I_2(m)$, this holds exactly when $4\mid m$, or when $m$ is odd and $3\mid m$.
Together with the known dihedral Artin-group cases, the positive quotient results imply that
every irreducible spherical Artin group of rank at least two has $\Rinf$.

The positive proofs combine the rational representation theory of the holonomy action with
integral lattice constraints and explicit fixed-vector witnesses. In the negative dihedral cases,
we construct automorphisms compatible with the crystallographic extension. For type $I_2(5)$,
we exhibit an automorphism with Reidemeister number $18$, showing concretely that the quotient
construction does not preserve $\Rinf$. This example, including the identification with the
presented Artin quotient and the exact Reidemeister count, is formalised in Lean.
An alternative proof for seven Artin groups is formalised under explicitly stated external hypotheses.
\end{abstract}

\noindent\textbf{AI transparency statement.} The mathematical arguments, programs, Lean formalisation
and manuscript were developed by AI systems under the author's direction. The scope of the formal
verification is stated in Appendix~\ref{app:artin}; details of AI use are given at the end of the paper.

\section{Introduction}

Let $G$ be a group and $\varphi\in\Aut(G)$. Elements $x,y\in G$ are \emph{$\varphi$-twisted conjugate} if
$y=zx\varphi(z)^{-1}$ for some $z\in G$. The number $R(\varphi)\in\{1,2,\dots,\infty\}$ of classes is the
\emph{Reidemeister number}, and $G$ has \emph{property $\Rinf$} if $R(\varphi)=\infty$ for every
$\varphi\in\Aut(G)$ \cite{FT15,FN16}.

For an Artin group $A=A(X)$ with Coxeter group $W=W(X)$, the question ``which Artin groups have $\Rinf$?''
is Problem~8.6 of the AIM problem list on Artin groups \cite{AIMPL}. Known cases include:
\begin{itemize}
\item braid groups \cite{FG10} and pure braid groups \cite{DGO21};
\item the spherical types $A_n$, $B_n$, $D_4$, $I_2(m)$ \cite{CS22};
\item $D_n$ for $n\ge6$ \cite[Thm.~1]{SV24};
\item many non-spherical types \cite{Juh11,SV24,Sor26}.
\end{itemize}
The case $D_5$ was left as a conjecture in \cite[\S1]{SV24}.
It follows from Paris--Soroko \cite[Lemma~4]{PS26}: the kernel of the natural epimorphism
$A[D_5]\to A[A_4]$ is fully characteristic, so the known braid-group case \cite{FG10}
and Lemma~\ref{lem:reid}(a) imply property $\Rinf$ for $A[D_5]$.
This is a consequence of their lemma; we give an independent proof as part of our uniform quotient argument.
For spherical types the known proofs use an explicit description of $\Aut(A)$ or $\Aut(A/Z(A))$. For $I_2(m)$
they use instead the virtual freeness of $A/Z(A)$ \cite{CS22}.

\begin{mainthm}
Every irreducible Artin group of spherical type and rank at least two has property $\Rinf$.
\end{mainthm}

Theorem~A completes the irreducible spherical case of AIM Problem~8.6.
Our proof treats all ranks at least three through their crystallographic quotients; it gives explicit
proofs for $D_5,E_6,E_7,E_8,F_4,H_3,H_4$.
Rank one must be excluded: $A(A_1)\cong\Z$, and inversion has Reidemeister number $2$.

Let $P=\ker(A\to W)$. Marin \cite[Thm.~2.1]{Mar15} proves that $A/[P,P]$ is crystallographic with holonomy
$W/Z(W)$. Theorem~B gives a separate classification of property $\Rinf$ for these crystallographic quotients.
It concerns all automorphisms of the quotient, including those that need not lift to $A$.

\begin{quotientthm}
Let $X$ be irreducible spherical of rank at least two, and let $\Gamma_X=A(X)/[P,P]$.
If $X$ has rank at least three, then $\Gamma_X$ has property $\Rinf$.
In rank two, writing $X=I_2(m)$ with $m\ge3$, we have
\[
 \Gamma_X\text{ has }\Rinf
 \quad\Longleftrightarrow\quad
 4\mid m\ \text{ or }\ (m\text{ odd and }3\mid m).
\]
\end{quotientthm}

The proof is completed in Section~\ref{sec:quotients}. For the exceptional types it uses the full
holonomy-automorphism calculations in Appendix~\ref{app:out}; the classical and dihedral families have
uniform proofs. Since $P$ and hence $[P,P]$ are characteristic \cite{CP03}, the positive cases of Theorem~B
imply $\Rinf$ for the corresponding Artin groups. Together with the known dihedral Artin-group result
\cite{CS22}, this proves Theorem~A. Appendix~\ref{app:artin} explains the different dependencies of the accompanying Lean development.
The next result makes the failure of preservation concrete.

\begin{counterprop}
The crystallographic quotient $A(I_2(5))/[P,P]$ admits an automorphism $\varphi$ with $R(\varphi)=18$.
In particular, it does not have property $\Rinf$.
\end{counterprop}

Thus $A(I_2(5))$ has $\Rinf$, whereas its natural crystallographic quotient does not.
Section~\ref{sec:dihedral-counterexample} gives the affine automorphism, checks the precise translation lattice
and extension, and counts twisted classes directly. The count takes account of torsion.
The positive results use absolutely irreducible multiplicity-one constituents to restrict commuting lattice
automorphisms to signs. In the dihedral example the nontrivial rational constituent instead has an infinite-order unit
in its commutant; a separate extension calculation shows that this unit yields an admissible automorphism.

A close precedent is the work of Dekimpe--Gon\c{c}alves--Ocampo \cite[Thms.~28, 31 and proof of Cor.~32]{DGO24}, which proves
$\Rinf$ for $VB_n/[VP_n,VP_n]$ for $n=3,4$. Those are virtual-braid quotients; the spherical Artin quotients
in Theorem~B have different holonomy modules and extensions.
Recent work also studies torus bundles arising from Bieberbach subgroups of classical braid quotients
\cite{Oca26} and crystallographic quotients of framed braid groups \cite{LOST26}.
Ocampo points to Nielsen and Reidemeister numbers of fibre-preserving maps as further questions for
the torus bundles \cite[\S1]{Oca26}.
The smallest positive case $A_2$ is already implicit in earlier classifications: its quotient is space
group IT~161 \cite[\S5]{GGO17}, which is absent from the complete list of three-dimensional groups
without $\Rinf$ in \cite[Table~2]{DKT19}.

The proof uses the finite holonomy action rather than a description of $\Aut(A)$.
Representation-theoretic approaches to $\Rinf$ occur in \cite{DGO21} and in the multiplicity-one criterion
of Dekimpe--De Rock--Penninckx \cite[Thm.~4.7]{DDP09}. We combine this mechanism with the
crystallographic determinant criterion \cite[Cor.~3.10]{DP11}, which permits torsion, and with
explicit witnesses on stable or exchanged constituents. Section~\ref{sec:alternative} explains an
alternative using Hiss--Lutowski \cite{HL25,HL26} for $D_5,E_6,E_7,E_8,H_4$.
That odd-dimensional criterion does not supply the $F_4$ and $H_3$ cases.

The resulting classification depends on two separate features: the rational holonomy representation
and the integral normaliser compatible with the crystallographic extension. Our positive witnesses
and negative affine maps make both features explicit. The witness argument avoids the classification
of finite simple groups, which enters the Hiss--Lutowski theorem; it still uses results on finite Coxeter
groups and exact exhaustive computations.

\smallskip\noindent\emph{Organisation of the proof.}
Section~\ref{sec:lattice} identifies the reflection lattice and the precise translation lattice of $\Gamma$.
Section~\ref{sec:criterion} states a fixed-vector criterion for crystallographic groups.
Sections~\ref{sec:exceptional} and~\ref{sec:classical} construct the exceptional and classical witnesses;
the latter also controls character-preserving holonomy automorphisms in all classical ranks.
Section~\ref{sec:quotients} combines these inputs and deduces Theorem~A before proving the dihedral classification
and counting the twisted classes in Proposition~C. Appendix~\ref{app:comp} specifies the computational inputs,
Appendix~\ref{app:out} controls the exceptional holonomy automorphisms, and Appendix~\ref{app:artin}
specifies the scope and dependencies of the formalisation.

\smallskip\noindent\emph{Verification.}
Exact computational certificates accompany the exceptional proofs. A conditional Lean~4/Mathlib
formalisation proves seven direct Artin cases through Franzsen--Howlett, using the same fixed-vector mechanism
and finite certificates; Appendix~\ref{app:artin} specifies its four external hypotheses.
Lean also proves Proposition~C for the presented Artin quotient, including its identification
with the affine model and the exact count $R(\varphi)=18$, without external mathematical hypotheses.
The full quotient classification remains outside the formalisation.

\section{The characteristic reflection lattice}\label{sec:lattice}

\begin{lemma}\label{lem:reid}
Let $\psi\in\Aut(G)$.
\begin{enumerate}[label=(\alph*)]
\item If $K\trianglelefteq G$ with $\psi(K)=K$, then $R(\psi)\ge R(\bar\psi)$.
\item If $G=\Z^m$ and $\psi$ is given by $B$, then $R(\psi)=|\coker(I-B)|$. This is $\infty$ if $B$ has eigenvalue $1$.
\item $R(\iota_g\circ\psi)=R(\psi)$, where $\iota_g(x)=gxg^{-1}$.
\item If $[G:H]<\infty$ and $\psi(H)=H$, then $R(\psi|_H)\le[G:H]\,R(\psi)$.
\end{enumerate}
\end{lemma}
\begin{proof}
(a) The projection maps classes onto classes.

(b) $y\sim x$ iff $y-x\in(I-B)\Z^m$.

(c) $x\mapsto xg$ maps $\iota_g\psi$-classes bijectively to $\psi$-classes.

(d) Fix $x\in H$ and write $G=\bigsqcup_iHg_i$. If $y=zx\psi(z)^{-1}\in H$ with $z=hg_i$, then $y$ is $\psi|_H$-conjugate to
$g_ix\psi(g_i)^{-1}\in H$. Thus each $G$-twisted class meeting $H$ contains at most
$[G:H]$ twisted classes for the restriction.
\end{proof}

\emph{Notation.} For a Coxeter graph with vertex set $S$:
\begin{itemize}
\item $A=\langle S\mid\Pi(s,t;m_{st})=\Pi(t,s;m_{st})\ (s\ne t,\ m_{st}<\infty)\rangle$, where $\Pi(s,t;m)=sts\cdots$
has $m$ letters;
\item $W=A/\langle\!\langle s^2\rangle\!\rangle$, with quotient map $\mu\colon a\mapsto\bar a$, and $P=\ker\mu$;
\item $\T$ is the set of reflections, $\rho(w)(r)=wrw^{-1}$, and $\rho(w)$ also denotes the permutation matrix on
$\Z^\T$; its permutation character is $\chi_\T(g)=\#\{r:g(r)=r\}$.
\end{itemize}
In spherical type, write $w_0$ for the longest Coxeter element and $\Delta$ for its standard
Garside lift, obtained by replacing the simple reflections in a reduced expression by Artin generators.

Since $\T$ generates $W$, $\ker\rho=Z(W)$. For finite irreducible $W$, in its Euclidean reflection
representation, a central orthogonal operator preserves each simple-root line; commuting with adjacent simple
reflections forces the corresponding signs to agree. Connectivity therefore gives $Z(W)\subseteq\{\pm1\}$.
In rank at least three, $-r$ is not a reflection, so
$r\mapsto\rho(r)$ is injective on $\T$.

\begin{theorem}[{\cite[Thm.~1.4]{CP03}}]\label{thm:char}
If $A$ is irreducible of spherical type, then $P$ is characteristic in $A$.
\end{theorem}

This was extended to reducible types in \cite{FP06}. The proof in \cite{CP03} is computer-assisted in several
cases:
\begin{itemize}
\item for $H_4,F_4,E_6,E_7,E_8$ it uses GAP calculations \cite[Prop.~5.4, Cor.~5.5]{CP03};
\item for $H_3$ it uses one GAP calculation \cite[Lemma~5.1]{CP03};
\item among the classical types it uses GAP for $B_4,B_6,D_4,D_6$ \cite[Lemmas~3.5, 4.4]{CP03}.
\end{itemize}
We have not re-run these calculations.

\begin{lemma}\label{lem:f}
For any Coxeter group, $s\mapsto(e_s,s)$ defines a homomorphism $f\colon A\to\Z^\T\rtimes W$, with
$(v,w)(v',w')=(v+w\cdot v',ww')$ and $w\cdot e_r=e_{wrw^{-1}}$.
\end{lemma}
\begin{proof}
For $\Pi(s,t;m)$, the $\Z^\T$-component is $\sum_{k=1}^me_{r_k}$ with $r_k=(st)^{k-1}s$. For $\Pi(t,s;m)$ it is
$\sum_ke_{r'_k}$ with $r'_k=(st)^{m-k}s$. Both sets equal $\{(st)^js:0\le j<m\}$. Compare \cite[Lemma~3.7]{CP03}.
\end{proof}

\begin{proposition}\label{prop:H1}
Let $A$ be of spherical type. Then $f(P)=2\Z^\T$, and $f$ induces an isomorphism $H_1(P;\Z)\cong2\Z^\T$ under which
conjugation by $a$ acts as the permutation $\rho(\bar a)$.
\end{proposition}
\begin{proof}
We have $f(as^2a^{-1})=(2e_{\bar as\bar a^{-1}},1)$, and these elements generate $f(P)$. Moreover $P\cong\pi_1$ of
the complexified reflection-arrangement complement \cite{Bri71}, whose integral $H_1$ is free on one
meridian per hyperplane \cite[\S2.3]{Suc14}. Indeed, choose a spanning disk in the ambient complex vector
space transverse to the hyperplanes and disjoint from their pairwise intersections. Removing small disks
around the intersection points expresses the loop's homology class as a sum of meridians;
winding numbers of defining linear forms show that these meridians are independent.
Thus $H_1(P;\Z)$ has rank $|\T|$, and the surjection onto $2\Z^\T$ is an isomorphism.
\end{proof}



\begin{proposition}\label{prop:translation-lattice}
For irreducible spherical $A$, the group $\Gamma=A/[P,P]$ has a faithful crystallographic action
on $\mathbb R^\T$, with holonomy $G=\rho(W)=W/Z(W)$ and characteristic translation lattice
\[
 L=\begin{cases}2\Z^\T,&Z(W)=1,\\2\Z^\T+\Z\mathbf1,&Z(W)\ne1.\end{cases}
\]
Every permutation of $\T$ preserves $L$.
\end{proposition}
\begin{proof}
By Proposition~\ref{prop:H1}, $f(A)\cong\Gamma$. Give it the action
$(v,w)\cdot x=v+\rho(w)x$.
\emph{The translation lattice.} Let $\Lambda=\{(v,w)\in\Gamma: w\in Z(W)\}$, the preimage of $Z(W)$ \cite[Thm.~2.1]{Mar15}.
Its elements act as translations by $v$. This action is faithful: elements with $W$-part $1$ have even coordinates,
while those with $W$-part $w_0$ (if $w_0=-1$) have odd coordinates, since a reduced expression for $w_0$ encounters each positive root once, giving
$f(\Delta)=(\mathbf1,w_0)$. So
$\Lambda\cong L$, where $L=2\Z^\T$ if $Z(W)=1$ and $L=2\Z^\T+\Z\mathbf 1$ otherwise. Every permutation matrix preserves $L$.
Since $\ker\rho=Z(W)$, the resulting affine action is faithful. Its full translation lattice has finite
index, so the action is discrete and cocompact.

\emph{$\Lambda$ is characteristic.} $\Gamma/\Lambda=\rho(W)$ acts faithfully on $L$. Let $N'$ be an abelian normal subgroup
of finite index. For $n\in N'$, the linear part of $n$ fixes the finite-index sublattice $N'\cap\Lambda$ pointwise, so it
is trivial and $n\in\Lambda$. Thus $\Lambda$ is the unique maximal abelian normal subgroup of finite index, hence
characteristic.

This identifies the quotient of Marin \cite[Thm.~2.1, Cor.~2.2]{Mar15}; see also
\cite{GGO17,DKNS24}.
\end{proof}

\section{The fixed-vector criterion}\label{sec:criterion}

Let $L$ be a lattice, $V=L\otimes\Q$, and $G\le GL(L)$ finite. A rational $G$-submodule
$U\subseteq V$ is \emph{good} if $U\otimes\C$ is irreducible and occurs with multiplicity one in
$V\otimes\C$. Such a $U$ is a full isotypic component. Our applications have $V=\Q^\T$.

\begin{lemma}\label{lem:schur}
If $U$ is good and $N\in GL(L)$ commutes with $G$, then $NU=U$ and $N|_U=\pm1$.
\end{lemma}
\begin{proof}
Multiplicity one gives $NU=U$, and absolute irreducibility gives $N|_U=c\in\Q^\times$.
Both $N$ and $N^{-1}$ preserve $U\cap L$. Applying them to a primitive lattice vector gives
$c,c^{-1}\in\Z$, hence $c=\pm1$.
\end{proof}

\begin{lemma}\label{lem:cert}
A nonzero invariant $U\subseteq\Q^\T$ is good in each of the following cases.
\begin{enumerate}[label=(\roman*)]
\item Every orbital matrix of $\rho(W)$ on $\T\times\T$ acts on $U$ by a scalar.
\item $\langle\chi_U,\chi_U\rangle=\langle\chi_U,\chi_\T\rangle=1$.
\item $U\otimes\C$ is irreducible and $\sum_r\dim(U\otimes\C)^{\mathrm{Stab}(r)}=1$, where $r$ runs over
representatives of the $\rho(W)$-orbits on $\T$ (Frobenius reciprocity).
\end{enumerate}
\end{lemma}
\begin{proof}
(i) The orbital matrices span the commutant $\mathcal C=\End_{\C W}(\C^\T)=\prod_iM_{m_i}(\C)$, where
$\C^\T=\bigoplus_iV_i\otimes\C^{m_i}$. By hypothesis $\mathcal C$ maps $U_\C=U\otimes\C$ into itself and acts on it
by scalars. The central idempotents $e_i\in\mathcal C$ act on $U_\C$ by $0$ or $1$ and sum to $1$, so exactly one
$e_i$ acts as $1$. Hence $U_\C\subseteq V_i\otimes\C^{m_i}$ meets only one isotypic component. Being
$W$-invariant, $U_\C=V_i\otimes E$ for some $0\ne E\subseteq\C^{m_i}$, and $M_{m_i}(\C)$ preserves $E$ and acts on it
by scalars. This forces $m_i=1$ and $E=\C$. (ii) and (iii) are standard.
\end{proof}

\begin{theorem}[Fixed-vector criterion]\label{thm:crit}
Let $\Gamma$ be crystallographic with translation lattice $L$ and holonomy $G$.
Suppose that every linear part $D$ of an automorphism of $\Gamma$ admits $\pi\in GL(L)$
inducing the same automorphism of $G$, such that one of the following holds.
\begin{enumerate}[label=(\roman*)]
\item\emph{(stable)} There is a good $U$ with $\pi U=U$ such that, for each $\varepsilon=\pm1$,
some $g\pi$, $g\in G$, has eigenvalue $\varepsilon$ on $U$.
\item\emph{(swap)} There are distinct good constituents $U_1,U_2$ with $\pi U_1=U_2$ and $\pi U_2=U_1$
such that, for each $\varepsilon=\pm1$, some $(g\pi)^2$ has an eigenvector in $U_1$ of eigenvalue $\varepsilon$.
\end{enumerate}
Then $\Gamma$ has property $\Rinf$.
\end{theorem}
\begin{proof}
Fix $\varphi\in\Aut(\Gamma)$, and let $D=\varphi|_L$.
The operator $N=\pi^{-1}D$ centralises $G$, so Lemma~\ref{lem:schur} applies.
In case (i), write $N|_U=c\in\{\pm1\}$ and choose $g\pi v=cv$ with $v\ne0$.
Then $gDv=v$.
In case (ii), write $N|_{U_i}=c_i\in\{\pm1\}$ and choose $(g\pi)^2v=c_1c_2v$ with
$0\ne v\in U_1$. Since $g\pi$ exchanges the two constituents, $(gD)^2v=v$.
The vector $v+gDv$ is nonzero, because its two terms lie in distinct isotypic components, and is fixed by $gD$.

Lift $g$ to $\gamma\in\Gamma$. The restriction of $\iota_\gamma\varphi$ to the characteristic
finite-index subgroup $L$ has a nonzero rational fixed vector, hence an integral one.
Lemma~\ref{lem:reid}(b),(d),(c) gives $R(\varphi)=\infty$.
\end{proof}

\begin{remark}[Relation to the crystallographic criteria]\label{rem:crystal}
The stable case uses the multiplicity-one device of \cite[Thm.~4.7]{DDP09}.
The determinant criterion \cite[Cor.~3.10]{DP11}, stated in \cite[Thm.~3.3]{DKT19}, applies also
with torsion: $R(\varphi)=\infty$ exactly when $\det(I-gD)=0$ for some $g\in G$.
The swap case covers exchanged constituents excluded by the non-conjugacy hypothesis of the stable criterion.
Only holonomy automorphisms induced by the actual extension need be considered. Their image satisfies
\[
 \Theta_\Gamma\subseteq\Theta_\chi
 :=\{\theta\in\Aut(G):\chi_V\circ\theta=\chi_V\},
\]
since $D$ intertwines the representations. Controlling all of $\Aut(G)$ is a sufficient stronger condition.
\end{remark}

\begin{remark}\label{rem:reduce}
\begin{itemize}
\item If $\pi$ works for $\theta$, then $g\pi$ works for $\iota_g\theta$, since $\{hg\pi\}=\{h\pi\}$. So one
$\theta$ per coset of $\Inn(\rho(W))$ suffices.
\item For the identity representative of the inner class, take $\pi=1$. Then (i) holds for any good $U$ on which some reflection acts nontrivially.
This is automatic for a nontrivial good $U$ when all reflections are conjugate: the kernel of the action is normal,
so if it contained one reflection it would contain all of them.
\item If $r\mapsto\rho(r)$ is injective on $\T$ (true for finite irreducible $W$ in rank $\ge3$, and for odd dihedral types) and
$\theta(\rho(\T))=\rho(\T)$, then $\pi(r)=\rho^{-1}\theta\rho(r)$ realises $\theta$.
\end{itemize}
\end{remark}

\section{The exceptional types}\label{sec:exceptional}

Write $\Theta_X$ for the representatives of holonomy automorphisms modulo inner automorphisms
listed in the table below. Appendix~\ref{app:out} proves that these exhaust the possibilities.
We construct the good constituents and witnesses needed for each representative.
For a displayed root-line permutation $\pi_F$ normalising $G=\rho(W)$, write
$\theta_F(g)=\pi_Fg\pi_F^{-1}$ for the induced automorphism of $G$.
This convention applies to $F=\Sigma,L,\Psi$ below.


\begin{proposition}[$E_6,E_7,E_8$]\label{prop:E}
Let $A_\perp$ be the adjacency matrix of the orthogonality graph on root lines.
\begin{enumerate}[label=(\alph*)]
\item $\rho(W)$ has exactly three orbitals on $\T\times\T$: equality, orthogonality and non-orthogonality.
\item The graph is strongly regular with parameters $(36,15,6,6)$, $(63,30,13,15)$, $(120,63,30,36)$. Its
nontrivial eigenvalues are $3^{15},(-3)^{20}$; $3^{35},(-5)^{27}$; $3^{84},(-9)^{35}$ (multiplicities as
exponents).
\item The two nontrivial eigenspaces are good, and every reflection acts nontrivially on them.
\end{enumerate}
\end{proposition}

\begin{proof}
By the pointwise-stabiliser theorem \cite[Thm.~1.12(c),(d), pp.~22--23]{Hum90}, the stabiliser of a root, or of a pair of roots, is the Weyl group of the
perpendicular root subsystem. The perpendicular subsystems are listed below. The root counts and ranks are
finite computations, certified exactly (exact rational ranks) as proof certificates in Appendix~\ref{app:comp}. Each pair (number of roots, rank) in the table occurs for exactly one
simply-laced root system, irreducible or not, of that rank, so the counts determine the types. These are the
classical facts that the centraliser of a reflection in $W(E_8)$, $W(E_7)$, $W(E_6)$ involves $W(E_7)$, $W(D_6)$,
$W(A_5)$.

\begin{center}\small
\begin{tabular}{lccc}
\toprule
 & $\alpha^\perp$ & $\{\alpha,\gamma\}^\perp$, $\alpha\perp\gamma$ & $\{\alpha,\beta\}^\perp$, $(\alpha,\beta)=1$\\
\midrule
$E_6$ & $A_5$ (30, rank 5) & $A_3$ (12, rank 3) & $A_2^2$ (12, rank 4)\\
$E_7$ & $D_6$ (60, rank 6) & $D_4A_1$ (26, rank 5) & $A_5$ (30, rank 5)\\
$E_8$ & $E_7$ (126, rank 7) & $D_6$ (60, rank 6) & $E_6$ (72, rank 6)\\
\bottomrule
\end{tabular}
\end{center}

$W$ is transitive on roots. Inside $W(\alpha^\perp)$, the orbits are as follows.
\begin{itemize}
\item The orbit of an orthogonal root has size $720/24=30$, $23040/384=60$, $2903040/23040=126$, i.e.\ all of
$\alpha^\perp$.
\item For $(\alpha,\beta)=1$, the orbit sizes are $720/36=20$, $23040/720=32$ and
$2903040/51840=56$. Each orbit consists of all such roots.
\end{itemize}
Passing to lines gives (a). Then $k$, $\lambda$, $\mu$ are half the root counts in the table, and (b) follows from
the standard formulas for strongly regular graphs.

By (a) the commutant is spanned by $I$, $A_\perp$ and $J$. These act by scalars on the nontrivial eigenspaces,
which are rational because the eigenvalues are integers. So Lemma~\ref{lem:cert}(i) applies, and
Remark~\ref{rem:reduce} gives the last assertion.
\end{proof}

\begin{proposition}[$H_3$]\label{prop:H3}
\begin{enumerate}[label=(\alph*)]
\item $\rho(W)\cong A_5$. The $15$ root lines form $5$ orthogonal triples (\emph{frames}), which correspond to the
Klein four-subgroups.
\item The frame module $U$ (functions constant on frames, with sum $0$) is a good $4$-dimensional constituent.
More precisely, writing irreducible $A_5$-modules by their dimensions,
\[\Q^\T\cong1\oplus U\oplus5\oplus5 .\]
\item For $\Sigma=\varsigma\circ\sigma$, where $\sigma$ is Galois conjugation $\sqrt5\mapsto-\sqrt5$ on coordinates
and $\varsigma$ swaps the last two coordinates, $\Sigma\Phi=\Phi$ and $\Sigma s_\alpha\Sigma^{-1}=s_{\Sigma\alpha}$. The
induced $\pi_\Sigma$ is not inner on $\rho(W)$.
\item For every outer $\theta\in\Aut(\rho(W))$, let $\pi$ be its induced permutation of root lines,
identified with the involutions of $\rho(W)$. There is $h\in\rho(W)$ such that $h\pi$ acts on the frames as a transposition. It then has
eigenvalues $+1$ (multiplicity 3) and $-1$ (multiplicity 1) on $U$.
\end{enumerate}
\end{proposition}

\begin{proof}
(a) Commuting reflections correspond to orthogonal lines, and the $15$ involutions of $A_5$ lie in $5$ Klein
four-subgroups, permuted as $A_5$ permutes $5$ points.

(b) $U$ is the augmentation module of a $2$-transitive action, hence absolutely irreducible. Since
$\Q^\T=\mathrm{Ind}_{V_4}^{A_5}1$, the multiplicity of an irreducible $\chi$ is $\dim\chi^{V_4}$. This equals
$1,0,0,1,2$ for $\chi$ of degree $1,3,3',4,5$, which gives the displayed decomposition.

(c) $\Sigma$ satisfies $(\Sigma x,\Sigma y)=\sigma(x,y)$. $\theta_\Sigma$ is not inner: on the rotation subgroup $W^+\cong\rho(W)$ it Galois-conjugates the character of
$\mathbb R^3$ on elements of order $5$, while inner automorphisms preserve characters. This is also checked by
machine.

(d) An outer automorphism of $A_5$ is conjugation by an odd permutation, and $\pi$ permutes the frames accordingly.
So $\{h\pi\}$ contains a transposition. In fact $\pi_\Sigma$ itself is a transposition on frames.
\end{proof}

\begin{proposition}[$F_4$]\label{prop:F4}
Let $L(x)=(x_1+x_2,x_1-x_2,x_3+x_4,x_3-x_4)$ and let $\pi_L$ be its permutation of root lines.
Conjugation by $L$ induces a non-inner holonomy automorphism $\theta_L$.
Each class of $12$ root lines (long, short) splits into $3$ orthogonal frames of $4$ lines. Let
$U_{\rm long},U_{\rm short}$ be the corresponding frame modules (sum zero). Then:
\begin{enumerate}[label=(\alph*)]
\item both are good and $2$-dimensional;
\item long reflections act on $U_{\rm long}$ as transpositions of frames and trivially on $U_{\rm short}$, and
vice versa;
\item $\pi_L$ exchanges $U_{\rm long}$ and $U_{\rm short}$, and $\pi_L^2=1$;
\item for a long simple reflection $s$, $(s\pi_L)^2=s\cdot\pi_Ls\pi_L$ has eigenvalue $-1$ on $U_{\rm short}$, and
$\pi_L^2$ gives eigenvalue $+1$.
\end{enumerate}
Hence case (ii) of Theorem~\ref{thm:crit} holds for $\theta_L$.
\end{proposition}

\begin{proof}
The similarity $L$ exchanges the long and short root lines and satisfies
$Ls_\alpha L^{-1}=s_{L\alpha}$, so it normalises $W$. It exchanges the two reflection classes,
whereas inner automorphisms preserve them. It remains non-inner on $\rho(W)$:
equality of two reflection images there forces equality of the reflections, since $-s$
has a three-dimensional $(-1)$-eigenspace and is not a reflection in rank four.

The long roots $\pm e_i\pm e_j$ form a $D_4$, whose frames correspond to the pairings $ij|kl$. The short lines
$e_i$ form one frame. The lines $\frac12(\pm1,\pm1,\pm1,\pm1)$ form two frames, according to the parity of the
number of minus signs. Each frame system is permuted through all of $S_3$, so each frame module is the standard
module of $S_3$.

\emph{Multiplicity one} (Lemma~\ref{lem:cert}(iii)):
\begin{itemize}
\item the stabiliser of the long line $e_1+e_2$ fixes one long frame and contains $s_{e_1-e_2}$, which swaps the
other two, so $\dim U_{\rm long}^{\rm Stab}=1$;
\item the stabiliser of the short line $e_1$ contains $\Sym\{2,3,4\}$, which induces $S_3$ on pairings, so
$\dim U_{\rm long}^{\rm Stab}=0$;
\item $U_{\rm short}$ follows by applying $\pi_L$.
\end{itemize}

(b) Check on $s_{e_1-e_2}$ and $s_{e_1}$, and use conjugacy.

(c) $L$ maps orthogonal frames to orthogonal frames and long to short lines, and $L^2=2I$.

(d) $\pi_Ls\pi_L$ is a short reflection.
\end{proof}

\begin{lemma}[Icosian model of $H_4$]\label{lem:icosian}
Halve the $120$ roots of $H_4$ (Appendix~\ref{app:comp}) and read the first coordinate as the real part. These
form a group $I$ of unit quaternions (the binary icosahedral group), and $K=I/\{\pm1\}\cong A_5$. Identify $\T$ with
$K$. Here $K\cong A_5$ is certified by a finite computation (Appendix~\ref{app:comp}): $K$ has $60$ elements and $15$
involutions, which lie in $5$ Klein four-subgroups; conjugation on these gives an injective homomorphism
$K\to S_5$ whose image consists of even permutations. Then:
\begin{enumerate}[label=(\alph*)]
\item the reflection in a unit root $r$ is $x\mapsto-r\bar xr$, and it acts on $K$ by $x\mapsto rx^{-1}r$;
\item $\rho(W)=\{x\mapsto ax^{\pm1}b:a,b\in K\}\cong(K\times K)\rtimes C_2$.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) For $|r|=1$, $r\bar xr=2(x,r)r-x$, using $\bar xr+\bar rx=2(x,r)$.

(b) By (a), $\rho(W)$ is contained in the right-hand group, which has order $7200=|W|/2=|\rho(W)|$.

The closure of $I$ under multiplication is a finite computation, certified exactly in Appendix~\ref{app:comp}.
\end{proof}

\begin{proposition}[$H_4$]\label{prop:H4}
Let $V$ be the $4$-dimensional augmentation module of $K\cong A_5$ acting on its five Klein four-subgroups, and
let $U\subseteq\Q^K$ be the span of the matrix coefficients $x\mapsto\operatorname{tr}(X\lambda_V(x))$
for $X\in\End_{\Q}(V)$, so
$U\cong\End(V)$ has dimension $16$.
\begin{enumerate}[label=(\alph*)]
\item $U$ is good.
\item Let $\Psi=\Omega\circ\sigma$, where $\sigma$ is Galois conjugation and $\Omega$ is the rotation $j\mapsto k$,
$k\mapsto-j$. Then $\Psi$ is a ring automorphism of $\HH_{\Q(\sqrt5)}$ with $\Psi(I)=I$. The induced permutation
$\pi_\Psi$ normalises $\rho(W)$, preserves reflections, and is not inner.
\item Every outer automorphism of $\rho(W)$ is realised by a permutation $\pi$ for which some
$h\pi$, $h\in\rho(W)$, acts on $U$ as conjugation by a transposition. This has
eigenvalues $+1$ (multiplicity $10$) and $-1$ (multiplicity $6$).
\end{enumerate}
\end{proposition}

\begin{proof}
(a) By Wedderburn, $\C[K]=\bigoplus_{V'}V'\otimes V'^*$ as a $K\times K$-module, each summand irreducible and
occurring once. The summand for $V_\C$ is $U\otimes\C\cong V_\C\otimes V_\C^*$, which is preserved by inversion. Since
$V$ is defined over $\Q$, so is $U\cong\End_\Q(V)$. Hence $U$ is good for $\rho(W)$. (We do not need the remaining
summands. Over $\C$ they are $1$, $3\otimes3$, $3'\otimes3'$ and $5\otimes5$; over $\Q$ the two $9$-dimensional
ones combine into one $18$-dimensional summand.)

(b) $\Psi$ commutes with quaternion conjugation, so $\Psi s_r\Psi^{-1}=s_{\Psi r}$. The equality $\Psi(I)=I$ is a
finite computation, certified exactly in Appendix~\ref{app:comp}. If $\theta_\Psi$ were inner, then
$\pi_\Psi\in\rho(W)$, because the centraliser of $\rho(W)$ in $\Sym(K)$ is trivial. Indeed, a permutation commuting
with all left and right translations is a translation by an element of $Z(K)=1$. Since $\pi_\Psi$ fixes $1$, it would be $x\mapsto ax^{\pm1}a^{-1}$. The sign $-$ is impossible, since $\pi_\Psi$ is an
automorphism of the non-abelian group $K$. The sign $+$ is impossible, since conjugation preserves real parts up to
sign, whereas $\Psi$ maps a quaternion with real part $\tau/2$ (it has order $10$ in $I$ and represents an element of
order five in $K$) to one with real part $-\tau^{-1}/2$ (here $\tau=\frac{1+\sqrt5}2$).

(c) We argue in three steps.
\begin{enumerate}[label=(\roman*)]
\item By Appendix~\ref{app:out} and Remark~\ref{rem:reduce}, we may take $\pi\in\rho(W)\pi_\Psi$. So $\{h\pi:h\in\rho(W)\}=\{h\pi_\Psi\}$.
\item By (b), $\pi_\Psi=\psi$ is an outer automorphism of $K$.
\item Since $\Aut(A_5)\cong S_5$, acting on the five Klein four-subgroups, $\psi$ is conjugation by an odd
permutation $\delta'$. For $a\in K=A_5$, the element $h=(x\mapsto axa^{-1})$ lies in $\rho(W)$, and $h\psi$ is
conjugation by $a\delta'$. Choose $a$ with $a\delta'=\delta$ a transposition.
\end{enumerate}
The action of $K$ on $V$ extends to $S_5$, with $\lambda_V(\delta)$ having eigenvalues $1,1,1,-1$. Since
$h\pi_\Psi$ acts on $U\cong\End(V)$ as $X\mapsto\lambda_V(\delta)X\lambda_V(\delta)^{-1}$, the eigenvalue $+1$ has
multiplicity $9+1$ and $-1$ has multiplicity $6$.
\end{proof}

\begin{table}[ht]\centering\small
\begin{tabular}{lrrlll}
\toprule
type & $|\T|$ & $|\rho(W)|$ & $\Theta_X$ & good constituent used (dim) & outer witness\\
\midrule
$E_6$ & 36 & 51840 & $1$ & $\mathbf{SRG}$ eigenspace (15; also 20) & ---\\
$E_7$ & 63 & 1451520 & $1$ & $\mathbf{SRG}$ eigenspace (35; also 27) & ---\\
$E_8$ & 120 & 348364800 & $1$ & $\mathbf{SRG}$ eigenspace (84; also 35) & ---\\
$F_4$ & 24 & 576 & $\{1,\theta_L\}$ & $\mathbf{U_{long}},\mathbf{U_{short}}$ (2+2) & swap: $\pi_L^2$, $(s\pi_L)^2$\\
$H_3$ & 15 & 60 & $\{1,\theta_\Sigma\}$ & $\mathbf{frame}$ module (4) & eigen-multiplicities 3, 1\\
$H_4$ & 60 & 7200 & $\{1,\theta_\Psi\}$ & $\mathbf{\End(V)}$ (16) & eigen-multiplicities 10, 6\\
\bottomrule
\end{tabular}
\caption{The exceptional-type data used for Theorems~A and~B. The dimensions agree with independent computer certificates
(Appendix~\ref{app:comp}).}
\end{table}

\section{The classical quotients}\label{sec:classical}

We first construct the constituents, then control the character-preserving holonomy automorphisms.

\begin{proposition}[$A_n$, $n\ge2$]\label{prop:An}
The standard constituent $S^{(n,1)}$ of $\Q^\T$ is good. Every character-preserving automorphism
of $\rho(W)=S_{n+1}$ is inner.
\end{proposition}
\begin{proof}
Here $\rho(W)=S_{n+1}$ acts on the transpositions, i.e.\ on the $2$-subsets. By Young's rule
$\Q^\T=S^{(n+1)}\oplus S^{(n,1)}\oplus S^{(n-1,2)}$ (for $n=2$ the last summand is absent). So $S^{(n,1)}$ is good.
For $n+1\ne6$, $\Aut(S_{n+1})=\Inn$. For $n+1=6$, an outer automorphism maps $(12)\mapsto(12)(34)(56)$, but
$\chi_\T$ takes the values $7$ and $3$ there, so it cannot preserve $\chi_\T$.
\end{proof}

For $B_n$ and $D_n$ let $u_{ij}=e_{[e_i+e_j]}-e_{[e_i-e_j]}$ ($i<j$) and $U^-=\mathrm{span}\{u_{ij}\}$. Let $E\le W$
be the group of sign changes: all of them for $B_n$, the even ones for $D_n$.

\begin{proposition}[$B_n$, $n\ge3$; $D_n$, $n\ge5$]\label{prop:BD}
$U^-$ is good. It has witnesses for both signs in the inner class and, for $D_n$,
in the class of the diagram involution.
\end{proposition}
\begin{proof}
\emph{Weights.} $E$ acts on $u_{ij}$ by $\chi_{ij}(\varepsilon)=\varepsilon_i\varepsilon_j$. These characters are
nontrivial and pairwise distinct on $E$. For $D_n$ this needs $n\ge5$: on even sign changes $\chi_{ij}=\chi_{kl}$
iff $\varepsilon_i\varepsilon_j\varepsilon_k\varepsilon_l$ is trivial or the product of all signs.

\emph{Goodness.} $E$ fixes $e_{[e_i+e_j]}+e_{[e_i-e_j]}$ and the short lines. So each $\chi_{ij}$ occurs once in
$\Q^\T$. Since $S_n\le W$ permutes the weights transitively, $U^-\otimes\C$ is irreducible.

\emph{Witnesses.} For the inner class, $\pi=1$ works: the reflection
$s_{e_n}$ ($B_n$), resp.\ $s_{e_{n-1}-e_n}$ ($D_n$), acts nontrivially on $U^-$. The diagram involution is realised
by negating $e_n$, which acts on $u_{ij}$ by $-1$ if $n\in\{i,j\}$ and by $+1$ otherwise. So case~(i) holds with
$g=1$.
\end{proof}

\begin{proposition}[$D_4$]\label{prop:D4}
In type $D_4$:
\begin{itemize}
\item $U^-$ is reducible: $J(u_{ij})=u_{kl}$ ($\{k,l\}$ complementary) is a non-scalar operator on $U^-$ commuting with
$W(D_4)$;
\item the frame module $U$ on the $3$ orthogonal frames $\{12|34,13|24,14|23\}$ is good of dimension $2$.
\end{itemize}
\end{proposition}
\begin{proof}
For $J$: a permutation $\sigma\in S_4$ maps $u_{ij}$ to $u_{\sigma i\,\sigma j}$ and commutes with taking complements; an
even sign change $\varepsilon$ acts by $\varepsilon_i\varepsilon_j$ on $u_{ij}$, and
$\varepsilon_i\varepsilon_j=\varepsilon_k\varepsilon_l$ because $\varepsilon_1\varepsilon_2\varepsilon_3\varepsilon_4=1$. Hence
$J$ commutes with $W(D_4)=E\rtimes S_4$, and its $\pm1$-eigenspaces are proper invariant subspaces of $U^-$.
The $E$-fixed part of $\Q^\T$ is the permutation module on the $6$ pairs, namely $1+3+2$ for $S_4$. Its
$2$-dimensional summand is $U$. On $U^-$ the three nontrivial sign characters are permuted transitively,
so every irreducible constituent there has dimension divisible by three. Thus $U$ is good and is the
unique rational irreducible constituent of dimension two. The image of $W$ on $U$ is $S_3$;
a transposition has eigenvalues $1,-1$.
\end{proof}

\subsection{Character-preserving holonomy automorphisms}\label{sec:classical-quotients}

The distinction between all holonomy automorphisms and those preserving the reflection character is
useful in the classical families. Write $\chi_\T$ for the permutation character on root lines.

\begin{lemma}\label{lem:classical-character}
For $W$ of type $B_n$, $n\ge3$, or $D_n$, $n\ge5$, every automorphism of $W/Z(W)$ preserving
$\chi_\T$ preserves the images of reflections. In type $B_n$ it preserves the short and long classes separately.
\end{lemma}
\begin{proof}
An involution in $W/Z(W)$ lifts to a signed permutation $w$ with $w^2=I$ or $w^2=-I$.
In the second case $w$ fixes no root line, since a real invariant line would give a real eigenvalue
whose square is $-1$. Thus its character value is zero, unlike that of a reflection in the indicated ranks.

For $w^2=I$, conjugate the signed transposed pairs to positive pairs and write $(a,b,c)$ for the numbers
of positive fixed coordinates, negative fixed coordinates, and transposed pairs; $a+b+2c=n$.
Counting fixed root lines gives
\[
 \chi_D(w)=a(a-1)+b(b-1)+2c,\qquad
 \chi_B(w)=a^2+b^2+2c.
\]
These counts do not depend on the signs on a transposed pair. In type $D_n$ we require $b$ even.

For a long reflection of $B_n$, the value is $(n-2)^2+2$. Equality is equivalent to
\[
 ab=2n(1-c)+2c^2+c-3.
\]
For $c\ge2$, the right-hand side is at most $-(2c-3)(c-1)<0$, using $n\ge2c$.
For $c=1$ it forces $ab=0$, giving a reflection or its negative. For $c=0$ it gives
$(a-2)(b-2)=1$, whose only solution with $n\ge3$ is $(a,b)=(3,3)$ in $B_6$.
That class has size $\binom63/2=10$ in $W/Z(W)$, whereas the long-reflection class has size $30$.
An automorphism cannot exchange them.
For a short reflection the value is $n^2-2n+2$, and the equation is
\[
 ab=n(1-2c)+2c^2+c-1.
\]
Its right-hand side is negative for $c\ge1$, $n\ge3$, $n\ge2c$ (for $c=1$ it is $2-n$).
For $c=0$ it reduces to $(a-1)(b-1)=0$, giving the short reflections and their negatives.
The two reflection character values differ when $n\ge3$.

For $D_n$ the reflection value is $(n-2)(n-3)+2$, and the equation becomes
\[
 ab=2n(1-c)+2c^2+2c-4.
\]
For $c=2$ its right-hand side is $8-2n<0$; for $c\ge3$ it is at most $-2(c-1)(c-2)<0$.
For $c=1$ we again get $ab=0$. For $c=0$ we get $(a-2)(b-2)=0$.
The last possibility is represented, up to the central sign when available, by negating two coordinates.
Its class has size $\binom n2$, whereas the reflection class has size $n(n-1)$.
These are also their class sizes in the even signed-permutation group: each representative has
an unused fixed coordinate, whose sign change is an odd element of its centraliser, so neither
signed-permutation conjugacy class splits upon restriction to $W(D_n)$.
For $n\ge5$ passing to $W/Z(W)$ does not halve either size: a lift and its negative have different
signed cycle types whenever both belong to $W$. This excludes the extra class and proves the lemma.
\end{proof}

\begin{proposition}\label{prop:classical-quotients}
The quotients $\Gamma_{A_n}$ ($n\ge2$), $\Gamma_{B_n}$ ($n\ge3$), and $\Gamma_{D_n}$ ($n\ge4$)
have property $\Rinf$.
\end{proposition}
\begin{proof}
Let $D$ be the linear part of a quotient automorphism and $\theta$ its holonomy automorphism.
It preserves $\chi_\T$, and every permutation of $\T$ preserves the translation lattice of Proposition~\ref{prop:translation-lattice}.

\emph{Type $A_n$.} The proof of Proposition~\ref{prop:An} applies directly: the exceptional outer
automorphism of $S_6$ does not preserve $\chi_\T$, so $\theta$ is inner, and the standard constituent
$S^{(n,1)}$ supplies the two signs.

\emph{Types $B_n,D_n$, $n\ge5$ in type $D$.} By Lemma~\ref{lem:classical-character}, $\theta$ preserves
reflections. For $D_n$, Lemma~\ref{lem:sign} makes it inner up to a diagram automorphism.
The same root argument works for $B_n$, as follows. Choose a root $\beta_i$ for each image of a simple
reflection, with the same length as the corresponding simple root $\alpha_i$; length is preserved by the lemma.
Orders of products of two distinct reflections agree in $W$ and $W/Z(W)$, because their plane action
fixes a nonzero complement and hence no nontrivial power can equal $-I$.
The Coxeter product orders therefore determine $|(\beta_i,\beta_j)|$.
Choose signs along the diagram tree to match all simple-root inner products. The isometry $g\colon\alpha_i\mapsto\beta_i$ satisfies $gWg^{-1}\le W$ and
\[g\Phi=(gWg^{-1})\{\beta_i\}\subseteq\Phi.\]
Since $g$ is injective and $\Phi$ is finite, equality holds. In type $B_n$ every such isometry is a signed permutation
(it permutes the short roots), so it belongs to $W$. Thus $\theta$ is inner in type $B_n$.
The $U^-$ witnesses of Proposition~\ref{prop:BD}, including its diagram-involution case for $D_n$,
now apply through Theorem~\ref{thm:crit}. This includes $B_3$ and $B_4$.

\emph{Type $D_4$.} By Proposition~\ref{prop:D4}, the frame constituent $U$ is the unique rational irreducible
constituent of dimension two. Hence $DU=U$.
The holonomy image on $U$ is $S_3$. Every automorphism of $S_3$ is inner, so $D|_U=c\rho_U(g)$ for some
$g$ and $c\in\Q^\times$. Both operators preserve $U\cap L$, forcing $c=\pm1$.
A reflection of this $S_3$ has eigenvalues $1,-1$, giving the required fixed vector after a holonomy twist.
\end{proof}

\section{The quotient classification}\label{sec:quotients}

\subsection{The six exceptional quotients}

\begin{theorem}[Six exceptional quotients]\label{cor:cryst}
For $X\in\{E_6,E_7,E_8,F_4,H_3,H_4\}$, the crystallographic group $\Gamma=A(X)/[P,P]$ has property $\Rinf$.
\end{theorem}

\begin{proof}
By Proposition~\ref{prop:translation-lattice}, the translation lattice $L$ is characteristic
and every permutation of $\T$ preserves it. An automorphism of $\Gamma$ therefore induces
$D\in GL(L)$ normalising $G=\rho(W)$.
Appendix~\ref{app:out} realises each holonomy automorphism by a permutation $\pi$ consisting of an inner permutation followed by
the appropriate representative $1$, $\pi_\Sigma$, $\pi_L$ or $\pi_\Psi$ from Section~\ref{sec:exceptional}.
For $E_6,E_7,E_8$, the holonomy automorphism is inner,
and Proposition~\ref{prop:E} supplies a good constituent with both signs.
For $H_3,H_4$, Propositions~\ref{prop:H3} and~\ref{prop:H4} give stable constituents and witnesses.
For $F_4$, Proposition~\ref{prop:F4} gives the stable inner case and the exchanged outer case.
Theorem~\ref{thm:crit} completes the proof.
\end{proof}

The proof uses all automorphisms of $\rho(W)$, not only those induced from $\Aut(W)$.
The calculations in Appendix~\ref{app:out} are therefore necessary inputs to this explicit proof.

\subsection{Deduction of Theorem A}

Theorem~\ref{cor:cryst} and Proposition~\ref{prop:classical-quotients} prove the rank-at-least-three
part of Theorem~B. This already suffices for the Artin-group classification.

\begin{proof}[Proof of Theorem A]
For rank at least three, $P$ and hence $[P,P]$ are characteristic in $A$
(Theorem~\ref{thm:char}). Every $\varphi\in\Aut(A)$ therefore induces
$\bar\varphi\in\Aut(A/[P,P])$. Projection is surjective on twisted conjugacy classes, so
\[
R(\varphi)\ge R(\bar\varphi)=\infty
\]
by the positive quotient results. In rank two, the Artin-group result is
\cite[Thm.~1]{CS22}. No negative dihedral construction or exact Reidemeister count is needed
for this deduction.
\end{proof}

\subsection{The odd-dimensional alternative}\label{sec:alternative}

The multiplicity-one argument of Dekimpe--De Rock--Penninckx \cite[Thm.~4.7]{DDP09}, combined with
Hiss--Lutowski \cite[Def.~1.1.3, Thm.~1.1.5]{HL25}, completed in \cite{HL26}, provides an alternative for five positive cases. We give the reduction
explicitly, since the flat-manifold statement in \cite{DDP09} assumes torsion-freeness, whereas our quotients
may have torsion.

Suppose $V$ has a nontrivial good constituent $U$ of odd dimension $d$, and no other irreducible complex
constituent has dimension $d$. Every $D\in N_{GL(L)}(G)$ preserves $U$: it permutes isotypic components
and preserves their irreducible dimensions. Moreover
$N_{GL(U\cap L)}(G|_U)$ is finite. Indeed, conjugation maps this normaliser to the finite group
$\Aut(G|_U)$, with kernel $\{\pm I\}$ by absolute irreducibility and integrality. Hence $D|_U$ has finite
order. The Hiss--Lutowski theorem supplies $g\in G$ with $gD|_U$ having eigenvalue one. The determinant
criterion \cite[Thm.~3.3]{DKT19}, valid with torsion, proves $\Rinf$. The uniqueness of the constituent also
verifies the non-conjugacy hypothesis in \cite[Thm.~4.7]{DDP09}.

\begin{center}\small
\begin{tabular}{lcll}
\toprule
type & odd dimension $d$ & explicit witnesses & odd-dimensional route\\
\midrule
$D_5$ & $5$ & applies & applies\\
$E_6$ & $15$ & applies & applies\\
$E_7$ & $27$ & applies & applies\\
$E_8$ & $35$ & applies & applies\\
$H_4$ & $25$ & applies & applies\\
$F_4,H_3$ & --- & applies & not supplied by this criterion\\
\bottomrule
\end{tabular}
\end{center}

Here are the constituent checks. For $E_n$, Proposition~\ref{prop:E} gives the complete decomposition.
For $D_5$, the sums $e_{[e_i+e_j]}+e_{[e_i-e_j]}$ form the permutation module on the $2$-subsets of five
letters, with irreducible dimensions $1,4,5$ by Young's rule; its complement is the good $10$-dimensional
$U^-$ of Proposition~\ref{prop:BD}. For $H_4$, the $5$-dimensional irreducible representation of $A_5$ is
defined over $\Q$: it is the augmentation module of the action on the six Sylow $5$-subgroups.
This action is doubly transitive, so the augmentation module is absolutely irreducible. Its matrix
coefficients give a rational good constituent of dimension $25$, by the argument of
Proposition~\ref{prop:H4}(a); the remaining complex dimensions are $1,9,9,16$.
Thus the required odd constituent is unique in each case. For $H_3$ the odd nontrivial constituent has
multiplicity two, and for $F_4$ the explicit proof uses the exchanged $2$-dimensional constituents.
The table concerns this particular odd-dimensional route, not every possible application of \cite{HL25,HL26}.

\subsection{Compatibility with the extension}

An infinite integral normaliser alone does not decide $\Rinf$. The extension determines which of its
elements actually occur as linear parts. We record the standard compatibility test
(cf.\ \cite[Algorithm~1]{DKT19}) in notation useful for the counterexample.

\begin{proposition}\label{prop:extension}
Write $\Gamma=\bigcup_{g\in G}(a_g+L,g)\le V_\mathbb R\rtimes G$, with $a_1=0$, and let
$D\in N_{GL(L)}(G)$ and $\theta(g)=DgD^{-1}$. Conjugation by $(d,D)$ is an automorphism of $\Gamma$ if and
only if
\begin{equation}\label{eq:extension}
Da_g+(I-\theta(g))d-a_{\theta(g)}\in L\qquad(g\in G).
\end{equation}
For such an automorphism, $R$ is finite if and only if $\det(I-gD)\ne0$ for every $g\in G$.
\end{proposition}
\begin{proof}
Affine conjugation sends $(a_g,g)$ to $(Da_g+(I-\theta(g))d,\theta(g))$.
Condition~\eqref{eq:extension} is exactly membership in the required coset. Since $DL=L$ and $\theta$ is
onto, these cosets map onto all of $\Gamma$. The last assertion is \cite[Thm.~3.3]{DKT19}.
It is enough to check membership on a set of generators of $\Gamma$, together with $DL=L$ and
surjectivity on $G$.
\end{proof}

Equivalently, $D$ must preserve the extension class with the indicated change of holonomy action.
This condition is separate from avoiding eigenvalue one in all the matrices $gD$.

\subsection{The dihedral classification}\label{sec:dihedral-classification}

\begin{theorem}\label{thm:dihedral-classification}
For $m\ge3$, the quotient $\Gamma_{I_2(m)}$ has $\Rinf$ if and only if $4\mid m$, or $m$ is odd and $3\mid m$.
\end{theorem}
\begin{proof}
On the basis $e_j$, $j\in\Z/m\Z$, put $Ce_j=e_{j+1}$ and $Se_j=e_{-j}$.
The actual quotient is generated affinely by $(e_0,S)$ and $(e_1,C^2S)$, with holonomy
$G=\langle C^2,S\rangle$. Its translation lattice is $2\Z^m$ for odd $m$ and
$2\Z^m+\Z\mathbf1$ for even $m$.

\emph{Odd $m$ divisible by three.} The permutation module on $m$ vertices is the regular module for the cyclic rotation subgroup.
Its rational decomposition is $\Q^m=\bigoplus_{d\mid m}U_d$, where $U_d\cong\Q(\zeta_d)$,
rotation acts by multiplication by $\zeta_d$, and reflection acts by complex conjugation.
Each $U_d$ is rationally irreducible and has dimension $\phi(d)$.
Among odd divisors $d$, the equality $\phi(d)=2$ holds only for $d=3$.
Thus for odd $m$ divisible by three, the unique $2$-dimensional constituent is $U_3$, whose holonomy image is $S_3$.
Every rational normaliser preserves this constituent. As in the $D_4$ case of
Proposition~\ref{prop:classical-quotients}, its restriction is a holonomy element times a rational scalar:
all automorphisms of $S_3$ are inner and the remaining commuting operator is scalar.
Preservation of the constituent lattice by the operator and its inverse forces this scalar to be $\pm1$.
The identity or a reflection then gives a fixed vector after a holonomy twist, so $\Rinf$ holds.

\emph{$m$ divisible by four.} Write $m=2q$, with $q$ even. The only nontrivial rational
$1$-dimensional constituents are the multiplicity-one lines spanned by
\[
 u_0=\sum_{j=0}^{q-1}(-1)^j e_{2j},\qquad
 u_1=\sum_{j=0}^{q-1}(-1)^j e_{2j+1}.
\]
Indeed, on each parity orbit $C^2$ is a $q$-cycle, so its $1$- and $(-1)$-eigenspaces are lines;
the $1$-eigenspaces are trivial $G$-modules. Both displayed lines have character $-1$ on $C^2$,
and their characters on $S$ are $1$ and $-1$, respectively.
Any $D\in N_{GL(L)}(G)$ preserves or swaps these lines. If it preserves them, it acts on each by $\pm1$,
and a holonomy twist gives eigenvalue one. If it swaps them, $D^2$ acts by a common scalar $c=\pm1$,
by preservation of the one-dimensional lattices. On their sum, $(gD)^2$ acts by
$c\chi_0(g)\chi_1(g)$. Choose $g=1$ or $S$ to make this scalar $1$.
Then $v+gDv$ is a nonzero fixed vector for any nonzero $v$ on the first line.

\emph{Odd $m$ not divisible by three.} Put $D=I-C-C^{-1}$ and $d=e_0+e_1$.
The identity $(I+C)(I-C+C^2)=I+C^3$ shows $\det(I-C+C^2)=1$:
both $C$ and $C^3$ are $m$-cycles and $\det(I+C)=\det(I+C^3)=2$ for odd $m$.
Since $D=-C^{-1}(I-C+C^2)$, it follows that $\det D=-1$.
Thus $D$ preserves $L=2\Z^m$ and commutes with $G$. Moreover,
\[
 (D-I)e_0+(I-S)d=-2e_{m-1},\qquad
 (D-I)e_1+(I-C^2S)d=-2e_2.
\]
Proposition~\ref{prop:extension} therefore gives an automorphism of the actual quotient.
The eigenvalues of $D$ are $1-2\cos(2\pi j/m)$. The only one of absolute value one is $-1$ on
the constant line: an eigenvalue $1$ would require $4\mid m$.
As $D$ commutes with the finite-order operators $g\in G$, their restrictions to its eigenspaces have
roots of unity as eigenvalues. Hence $gD$ cannot have eigenvalue one off the constant line, and on that
line it acts by $-1$. All the determinants $\det(I-gD)$ are nonzero, proving finite $R$.

\emph{$m\equiv2\pmod4$.} Write $m=2q$ with $q$ odd. The two parity orbits of reflections are
$G$-equivariantly identified by $j\mapsto j+q$. In the ordered pairs $(e_j,e_{j+q})$, $j$ even, let
\[
 D=I_q\otimes\begin{pmatrix}1&2\\2&5\end{pmatrix},\qquad d=0.
\]
This operator commutes with $G$, is integral unimodular, and is congruent to $I$ modulo two.
The same is true of $D^{-1}$, so both preserve $L=2\Z^m+\Z\mathbf1$.
The generator corrections $(D-I)e_0,(D-I)e_1$ lie in $2\Z^m$, proving extension compatibility.
The eigenvalues of $D$ are $3\pm2\sqrt2$, neither of modulus one. As in the preceding case, no $gD$
has eigenvalue one. This supplies an automorphism with finite $R$ and completes the classification.
\end{proof}

\begin{proof}[Proof of Theorem B]
Theorem~\ref{cor:cryst} and Proposition~\ref{prop:classical-quotients} cover every irreducible spherical
type of rank at least three. Theorem~\ref{thm:dihedral-classification} covers rank two, including
$A_2=I_2(3)$ and $B_2=I_2(4)$.
\end{proof}



\subsection{A dihedral counterexample}\label{sec:dihedral-counterexample}

\begin{proposition}[Proposition C]\label{prop:dihedral-counterexample}
The group $\Gamma=A(I_2(5))/[P,P]$ has an automorphism $\varphi$ with $R(\varphi)=18$.
\end{proposition}
\begin{proof}
Index the reflections by $j\in\Z/5\Z$, with the two simple reflections indexed by $0,1$.
On the reflection lattice set
\[
 Ce_j=e_{j+1},\qquad Se_j=e_{-j},\qquad G=\langle C,S\rangle.
\]
The two simple reflections act as $S$ and $C^2S$. By Proposition~\ref{prop:H1}, the actual quotient is
\[
 \Gamma=\langle(e_0,S),(e_1,C^2S)\rangle\le\Z^5\rtimes G,
 \qquad L=2\Z^5.
\]
Here $Z(W)=1$, so $L$ is the full translation lattice. Put
\[
 D=I-C-C^{-1},\qquad d=e_0+e_1,\qquad
 \varphi(v,g)=(Dv+(I-g)d,g).
\]
We have $D^{-1}=I-C^2-C^{-2}$ and $D$ commutes with $G$, so $DL=L$. For the two generators,
\[
 (D-I)e_0+(I-S)d=-2e_4,\qquad
 (D-I)e_1+(I-C^2S)d=-2e_2.
\]
These corrections lie in $L$. Thus conjugation by $(d,D)$ preserves $\Gamma$ and is onto, by
Proposition~\ref{prop:extension}. This checks the extension as well as the integral lattice.

The characteristic polynomial of $D$ is $(x+1)(x^2-3x+1)^2$, and direct integer determinants give
\[
\begin{array}{c|ccc}
 g&1&C^k\ (1\le k\le4)&C^kS\ (0\le k\le4)\\ \hline
 \det(I-gD)&2&22&-10.
\end{array}
\]
In particular all determinants are nonzero, which already proves $R(\varphi)<\infty$.

For completeness we count the classes without a torsion-free assumption. Since $\varphi$ induces the identity
on $G$, twisted classes project to ordinary conjugacy classes of $G$, represented by $1,C,C^2,S$.
Choose lifts $(a_g,g)\in\Gamma$. Twisted conjugation by translations identifies the fibre above $g$ with
\[
 Q_g=\Z^5/(I-gD)\Z^5,
 \qquad x\longleftrightarrow(a_g+2x,g).
\]
Every twisted class can first be moved into one of these four representative fibres.
Two elements of the same fibre can then be identified only by a conjugator whose holonomy centralises $g$.
Thus the remaining identifications after translation-twisted conjugacy are precisely the action of $C_G(g)$.
For a lift $(b_h,h)$ with $hg=gh$, that action is
\begin{equation}\label{eq:centralizer-action}
 x\longmapsto h x+\tfrac12\bigl(b_h+h a_g-gDb_h-g(I-h)d-a_g\bigr)
 \pmod{(I-gD)\Z^5}.
\end{equation}
The following table gives lifts, cyclic coordinates $k$ on $Q_g$, and the induced actions of centraliser
generators. All vectors are ordered from $0$ to $4$.
\begin{center}\small
\begin{tabular}{clclc}
\toprule
$g$ & $a_g$ & $Q_g$ & centraliser action & orbits\\
\midrule
$1$ & $(0,0,0,0,0)$ & $\Z/2$ & $C:k\mapsto k$, $S:k\mapsto k+1$ & $1$\\
$C$ & $(1,0,1,1,1)$ & $\Z/22$ & $C:k\mapsto5k+6$ & $6$\\
$C^2$ & $(0,1,1,0,0)$ & $\Z/22$ & $C:k\mapsto3k+4$ & $6$\\
$S$ & $(1,0,0,0,0)$ & $\Z/10$ & $S:k\mapsto1-k$ & $5$\\
\bottomrule
\end{tabular}
\end{center}
Here $a_{C^2}=e_1+e_2$ comes from the product of the second generator and the first, and $a_C$ is the parity
representative of its cube. The cyclic coordinates are $k=\ell_g x$ modulo the stated order, with
\[
 \ell_1=(1,1,1,1,1),\quad \ell_C=(1,5,3,15,9),\quad
 \ell_{C^2}=(1,3,9,5,15),\quad \ell_S=(5,1,7,3,9).
\]
Each functional is onto and annihilates $(I-gD)\Z^5$ modulo $|\det(I-gD)|$, so it identifies $Q_g$ with the
indicated cyclic group. Substitution in \eqref{eq:centralizer-action} gives the table.
Each order-five action on $\Z/22$ has two fixed points and four orbits of length five; the involution
$k\mapsto1-k$ on $\Z/10$ has no fixed points. Consequently
\[
 R(\varphi)=1+6+6+5=18.
\]
\end{proof}

\begin{remark}[Torsion and the determinant average]\label{rem:dihedral-average}
The element $((-1,0,-1,1,1),C)$ belongs to $\Gamma$ and has order five: its translation vector differs
from $a_C$ by an element of $2\Z^5$, and its five translates sum to zero. Thus the Bieberbach averaging
formula \cite[Thm.~3.4]{DKT19} cannot be invoked here. In fact its determinant average is
$(2+4\cdot22+5\cdot10)/10=14$, whereas $R(\varphi)=18$.
The exact checker \texttt{code/indep/dihedral\_quotient.py} verifies the preceding calculation and independently
enumerates all $140$ translation-twisted classes: there are $13$ holonomy orbits of size $10$ and $5$ of size $2$.
Equivalently, the identity fixes all $140$ classes, each nonidentity rotation fixes $10$, and each
reflection fixes none. Burnside's lemma gives
\[R(\varphi)=\frac{140+4\cdot10+5\cdot0}{10}=18.\]
The holonomy action is not free, which explains why dividing $140$ by $10$ gives the wrong answer.
\end{remark}

\begin{remark}[The representation-theoretic distinction]
For $I_2(5)$, $\Q^5=\Q\mathbf1\oplus U$, where $U$ is rationally irreducible but splits into two conjugate
$2$-dimensional constituents over $\Q(\sqrt5)$. Its commuting algebra is $\Q(\sqrt5)$.
The operator $D$ acts by $-1$ on the trivial line and by the conjugate units
$(3\pm\sqrt5)/2$ on those two constituents. These units have infinite order. The displayed generator
corrections are what make this particular unit compatible with the extension; the existence of units
alone would not establish Proposition~C.
\end{remark}

\smallskip\noindent\emph{Further question.} For the negative dihedral cases in Theorem~B, determine the
Reidemeister spectrum
$\{R(\varphi):\varphi\in\Aut(\Gamma_{I_2(m)})\}$. Proposition~C shows that $18$ belongs to this spectrum for
$m=5$. The extension-compatible integral normaliser and the torsion-sensitive class count both matter
for this more detailed question.

\appendix
\section{Computational certificates and cross-checks}\label{app:comp}

The repository for the computational sources and Lean development is
\begin{center}
\url{https://github.com/jasondavies/spherical-artin-rinf}.
\end{center}
The Python certificates and Lean development used in this paper are fixed by commit
\href{https://github.com/jasondavies/spherical-artin-rinf/tree/ab2165a10c66a49f462a1543857f98ae69007f87}{\texttt{ab2165a10c66}}
of that repository.
That revision also fixes their dependency versions and includes
the presented-quotient theorem in \texttt{lean/ArtinRinf/Dihedral5/Quotient.lean}.
The command \texttt{python3 scripts/verify.py -{}-clean} runs the certificates and builds the paper
and Lean development. Dependencies are pinned; each run records source, PDF and log hashes in its own
directory under \texttt{verification/runs/}.
The complete submitted snapshot, including the manuscript and PDF, is identified separately by
the SHA-256 checksum of the accompanying review archive. The command
\texttt{python3 scripts/package\_review.py} creates that archive only when its inputs, PDF and logs
match the latest successful full verification run. Its manifest records the source-and-PDF snapshot
digest, base commit and verification run identifier.
Programs, commands and expected outputs are listed in \texttt{code/README.md} of the accompanying repository. We
distinguish \emph{proof certificates} from \emph{corroboration}.
\begin{itemize}
\item Proof certificates are finite computations that the written proofs rely on. They use exact arithmetic over
$\Q$ and $\Q(\sqrt5)$, including exact rational row reduction for ranks, and the programs assert the expected values
(a nonzero exit status on any discrepancy).
\item Corroboration consists of independent recomputations, some of them numerical.
\end{itemize}

\emph{Coordinates.} For $E_8$ we use Bourbaki's simple roots in $\mathbb R^8$ with basis $e_1,\dots,e_8$:
\[\alpha_1=\tfrac12(e_1+e_8)-\tfrac12(e_2+\cdots+e_7),\qquad\alpha_2=e_1+e_2,\qquad\alpha_k=e_{k-1}-e_{k-2}\ \ (3\le k\le8).\]
$E_7$ and $E_6$ use $\alpha_1,\dots,\alpha_7$, resp.\ $\alpha_1,\dots,\alpha_6$, in $\mathbb R^8$. The other types:
\begin{itemize}
\item $F_4$: $e_2-e_3,\ e_3-e_4,\ e_4,\ \frac12(e_1-e_2-e_3-e_4)$;
\item $A_n,B_n,D_n$: standard simple roots;
\item $H_3$: roots $\pm2e_i$ and the even permutations of $(\pm\tau,\pm1,\pm\tau^{-1})$, with $\tau=\frac{1+\sqrt5}2$;
\item $H_4$: roots $\pm2e_i$, $(\pm1,\pm1,\pm1,\pm1)$ and the even permutations of $(\pm\tau,\pm1,\pm\tau^{-1},0)$.
\end{itemize}

\emph{Proof certificates.}
\begin{enumerate}[label=(\arabic*)]
\item Proposition~\ref{prop:E}: perpendicular root counts and their exact ranks (used to identify the subsystems),
together with the SRG parameters, the three orbitals and the eigenspace dimensions.
\item Propositions~\ref{prop:H3}--\ref{prop:H4} and Lemma~\ref{lem:icosian}:
\begin{itemize}
\item frames, and character norms $\langle\chi,\chi\rangle=\langle\chi,\chi_\T\rangle=1$;
\item the images of $W$ on frames ($A_5$, $S_3$);
\item the $(+1,-1)$-eigenspace dimensions of $\pi_\Sigma$ on the $H_3$ frame constituent: $(3,1)$;
of $\pi_L^2$ and $(s\pi_L)^2$ on $U_{\mathrm{short}}$ in type $F_4$, for a long simple reflection $s$:
$(2,0)$ and $(1,1)$, respectively; and of $h\pi_\Psi$ on the $16$-dimensional $H_4$ coefficient constituent,
with the inner adjustment $h$ from Proposition~\ref{prop:H4}(c): $(10,6)$;
\item the closure of $I$, the reflection formula, and $\rho(W)=\{x\mapsto ax^{\pm1}b\}$;
\item $K\cong A_5$: $|K|=60$, $15$ involutions, $5$ Klein four-subgroups, and conjugation is an injective homomorphism
into $A_5$; also $Z(K)=1$;
\item $\Psi(I)=I$, $\Psi$ multiplicative, and the real-part computation in Proposition~\ref{prop:H4}(b).
\end{itemize}
\item The exceptional cases of Theorem~B use the full holonomy-automorphism certificates in Appendix~\ref{app:out}.
\end{enumerate}
\emph{Corroboration.}
\begin{enumerate}[label=(\arabic*),resume]
\item Finite checks supporting the algebraic proofs of Propositions~\ref{prop:BD} and~\ref{prop:D4}:
\begin{itemize}
\item the weight argument for $B_3$--$B_6$ and $D_4$--$D_7$, including its failure for $D_4$;
\item the operator $J$ and the frame module of $D_4$;
\item witnesses for all six graph automorphisms of $D_4$.
\end{itemize}
\item Proposition~C has the direct calculation of Section~\ref{sec:dihedral-counterexample}; its exact
checker verifies the extension, all determinants, the cyclic quotient table, and the full twisted-class count.

\item Independent certificates for the six exceptional types:
\begin{itemize}
\item commutant certificates;
\item character certificates written as fresh code;
\item witnesses for abstractly computed outer automorphisms.
\end{itemize}
They give the same dimensions $15,20$; $27,35$; $35,84$; $4$; $2+2$; $16,25$.
\item The criterion (for automorphisms preserving $\chi_\T$) checked uniformly for $A_2$--$A_7$, $B_3$--$B_7$,
$D_4$--$D_7$, odd $I_2(m)$ with $m\le21$, and the exceptional types other than $E_8$.
\item Additional independent checkers. The one for $D_n$, $F_4$, $H_3$ and parts of the one
for $H_4$ use numerical linear algebra, so they are numerical corroboration only; the exact constituent and classical checks above provide their counterparts.
\item The uniform arguments in Lemma~\ref{lem:classical-character} and
Theorem~\ref{thm:dihedral-classification} have an independent finite cross-check in
\texttt{code/indep/quotient\_families.py}. It counts fixed root lines directly, checks the exceptional
character coincidences and conjugacy-class sizes, and verifies the positive constituents or the affine maps and all adjusted
determinants in the dihedral cases. The unbounded statements are proved in the text, not inferred
from these finite runs.
\end{enumerate}

\section{Automorphisms of the holonomy groups}\label{app:out}

For the six exceptional cases of Theorem~\ref{cor:cryst}, we control all holonomy automorphisms, a sufficient
strengthening of the character-preserving restriction. The following computations are proof certificates
for these cases of Theorem~B, as well as corroboration of \cite[Thm.~31]{FH03}:
\begin{itemize}
\item $\Out(\rho(W))=1$ for $E_6$, $E_7$, $E_8$;
\item $|\Out(\rho(W))|=2$ for $H_3$, $H_4$, $F_4$.
\end{itemize}
These statements were obtained as follows.
\begin{itemize}
\item \emph{Involution classes and Coxeter tuples}, by exact enumeration, for $H_3,H_4,F_4,E_6,E_7$.
No involution class other than the reflection classes has a reflection-class size, so every automorphism preserves
$\rho(\T)$; then the $\Inn$-orbits of generating Coxeter tuples of reflections are counted.
\item For $H_3,F_4$, an independent generator-image enumeration also counts all automorphisms
without first assuming reflection preservation.
\item For $E_7$ and $E_8$, the reflection-preserving stage was re-verified with Schreier--Sims stabiliser chains, and
it also follows from Lemma~\ref{lem:sign} below. For $E_7$ the reflection-preservation stage therefore rests on the
single exact enumeration above.
\item For $E_8$, Proposition~\ref{prop:E8} below gives a proof by hand.
\end{itemize}

The search in \texttt{code/indep/out\_check.py} enumerates the generated permutation group to closure
and partitions all its involutions by conjugation with the simple generators. At each stage of the
Coxeter-tuple search it considers every reflection satisfying the pair-product order constraints,
up to the stabiliser of the preceding tuple; at a leaf it checks generation of the whole group.
Thus no automorphism image tuple is omitted. Conversely, a generating tuple defines a surjection
$W\to\rho(W)$ whose kernel has order $|Z(W)|\le2$. If this order is two, the kernel is central,
so it equals $Z(W)$; the tuple therefore induces an automorphism of $\rho(W)$.
The checked injectivity of the reflection images identifies tuple stabilisers with point stabilisers,
so the resulting orbits are exactly the inner-automorphism orbits.

The separate computation $\Out(\rho(W(D_5)))=1$ is optional corroboration.
The main proof covers $D_5$ uniformly in Proposition~\ref{prop:classical-quotients} and does not use it.
Write $\Gr$ for the diagram automorphism group, acting by isometries that permute the chosen simple roots.

\begin{lemma}\label{lem:sign}
Let $\Phi$ be an irreducible simply-laced root system of rank $\ge3$ (so its diagram is a tree). Then every
$\theta\in\Aut(\rho(W))$ with $\theta\rho(\T)=\rho(\T)$ is inner up to a graph automorphism.
\end{lemma}
\begin{proof}
Write $\theta\rho(s_i)=\rho(s_{\beta_i})$; this uses that $\rho$ is injective on $\T$. Orders of products agree in $W$
and in $\rho(W)$. Indeed, for roots $\beta\ne\pm\gamma$ the element $s_\beta s_\gamma$ is a plane rotation fixing a
complement of dimension $\ge1$, so no nonidentity power of it lies in $Z(W)\subseteq\{\pm1\}$; in particular
$s_is_j\ne-1$. Hence $(\beta_i,\beta_j)=0$ or $\pm1$ according to the diagram. Choose the signs along the tree. Then $g\colon\alpha_i\mapsto\beta_i$ is an isometry, and
$g\Phi=(gWg^{-1})\{\beta_i\}\subseteq\Phi$. So $g\{\alpha_i\}$ is a simple system. As $W$ is simply transitive on simple systems, $g=w\gamma$ with $w\in W$ and
$\gamma$ an isometry permuting $\{\alpha_i\}$, i.e.\ $g\in W\rtimes\Gr=\Aut(\Phi)$ \cite[\S1.8, p.~15]{Hum90}. Compare
\cite[Thm.~18, Cor.~19]{FH03}.
\end{proof}

\begin{proposition}\label{prop:E8}
Every automorphism of $W(E_8)/\{\pm1\}$ is inner.
\end{proposition}
\begin{proof}
$G^+=W^+/\{\pm1\}$ is the commutator subgroup, of index $2$. An involution outside $G^+$ lifts to $w$ with $w^2=1$
and $\det w=-1$; if $w^2=-1$ then $\det w=1$. By \cite[Lemma~5, p.~5]{Car72} (provable via Steinberg's theorem), $w$ is a product of $k=\dim\ker(w+1)$ reflections in
mutually orthogonal roots, and $k$ is odd. Replacing $w$ by $-w$, we may take $k\in\{1,3\}$. For $k=3$, the
$(-1)$-eigenspace of $w$ is spanned by the three roots, and contains only the $6$ roots $\pm\beta_i$: a root
$\sum c_i\beta_i$ has $2c_i=(\cdot,\beta_i)\in\{0,\pm1,\pm2\}$ and $\sum c_i^2=1$. So $w$ determines the triple,
and $-w$ (with $k=5$) is not of this form.

The products for $k=3$ form one class of size $240\cdot126\cdot60/48=37800$, by transitivity along
$E_8\supset E_7\supset D_6$. So the reflections form the unique involution conjugacy class of size $120$ outside $G^+$. Hence every
automorphism preserves $\rho(\T)$, and Lemma~\ref{lem:sign} applies.
\end{proof}

\section{Scope of the formalisation}\label{app:artin}

The Lean development proves the direct Artin cases
$D_5$, $E_6$, $E_7$, $E_8$, $F_4$, $H_3$ and $H_4$ using the same reflection-lattice and fixed-vector
mechanism, with separately certified constituent bases and witnesses. Its automorphism reduction follows a different route:
Franzsen--Howlett \cite[Thm.~31]{FH03} express Coxeter automorphisms as reflection-preserving
automorphisms followed by central twists. Central twists disappear on $W/Z(W)$.
Reflection-tuple search certificates then control the induced holonomy automorphisms.
This route avoids the stronger full-holonomy computations required by Theorem~B.
The complete mathematical account is supplied with the Lean sources in
\texttt{lean/DIRECT\_PROOF.md}.

The Artin-group criterion used there applies the fixed-vector mechanism to the induced map
on $P^{ab}$: a holonomy twist with eigenvalue one gives infinitely many twisted classes on
$P^{ab}$, hence on $P$, and then on $A$ by Lemma~\ref{lem:reid}.
The finite part of the induced-automorphism reduction is checked by orbit--stabiliser search
certificates for all seven types. The kernel also checks the presented Artin group, its affine map,
the equivariant pure abelianisation, the scalar commutants and the sign/swap witnesses.
The constituent bases are computed certificates; the geometric constructions in
Section~\ref{sec:exceptional} are not formalised.

Each of the seven final Franzsen--Howlett theorems has four external hypotheses:
finiteness of $W$; characteristicity of $P$ \cite{CP03};
the abstract group isomorphism $P^{ab}\cong\Z^{|\T|}$ \cite{Bri71}; and the
Franzsen--Howlett decomposition \cite[Thm.~31]{FH03}.
These cited results are hypotheses, not formalised theorems of the development.
For $H_3$ and $F_4$ there are also theorems replacing the last hypothesis by kernel-checked
full-holonomy enumerations. The source contains no \texttt{sorry}, custom \texttt{axiom}
or \texttt{native\_decide}; finite certificates are checked by the Lean kernel.
The scalar and stable/swap arguments are separated into a general integral-lattice criterion.
For Proposition~C, the kernel checks the parity extension, its generation by the two affine
Artin images, the automorphism and its inverse, and the reduction of all twisted classes to
$140$ finite states with exactly $18$ orbits. A Schreier calculation using ten coset representatives
proves that five explicit meridians generate the pure subgroup. Their affine images are the
five standard basis translations, so the pure abelianisation maps isomorphically to $\Z^5$.
This proves that the affine map has kernel $[P,P]$ and identifies the presented quotient with
the affine model. The transferred Reidemeister-number theorem therefore has no external
mathematical hypotheses; in particular, it does not assume the arrangement-homology rank statement.
The full quotient classification remains outside the formalisation.

\section*{Declaration of AI-generated research and authorship}
This paper was developed through an AI-driven research process directed by Jason Davies.
Anthropic's Claude and OpenAI's Codex contributed to the mathematical arguments, computational
verification, Lean formalisation, and preparation and revision of the manuscript.

The Lean kernel checks the seven direct Artin-group results under the external hypotheses stated in
Appendix~\ref{app:artin}, as well as Proposition~C for the presented Artin quotient without external
mathematical hypotheses. The full quotient classification remains outside the formalisation.
Its written proof is accompanied by
the exact computational checks described in Appendix~\ref{app:comp}. These checks do not replace mathematical review of the written arguments.
The author takes responsibility for the content of the paper and the accuracy of this disclosure.

\begin{thebibliography}{99}
\raggedright
\bibitem{AIMPL} American Institute of Mathematics, \emph{Geometry and topology of Artin groups},
Problem 8.6, AIM Problem List. Internet Archive snapshot dated 13 February 2025,
\url{https://web.archive.org/web/20250213025936/http://aimpl.org/geomartingp/8/}
(accessed 10 November 2026).
\bibitem{Bri71} E. Brieskorn, Die Fundamentalgruppe des Raumes der regul\"aren Orbits einer endlichen komplexen Spiegelungsgruppe, \emph{Invent.\ Math.} 12 (1971), 57--61, \url{https://doi.org/10.1007/BF01389827}.
\bibitem{CS22} M. Calvez, I. Soroko, Property $R_\infty$ for some spherical and affine Artin--Tits groups, \emph{J.\ Group Theory} 25 (2022), 1045--1054, \url{https://doi.org/10.1515/jgth-2022-0010}.
\bibitem{Car72} R.\,W. Carter, Conjugacy classes in the Weyl group, \emph{Compositio Math.} 25 (1972), 1--59, \url{https://numdam.org/item/CM_1972__25_1_1_0/}.
\bibitem{CP03} A.\,M. Cohen, L. Paris, On a theorem of Artin, \emph{J.\ Group Theory} 6 (2003), 421--441, \url{https://doi.org/10.1515/jgth.2003.030}; \href{https://arxiv.org/abs/math/0204242}{arXiv:math/0204242}.
\bibitem{DDP09} K. Dekimpe, B. De Rock, P. Penninckx, The $R_\infty$ property for infra-nilmanifolds, \emph{Topol.\ Methods Nonlinear Anal.} 34 (2009), 353--373, \url{https://doi.org/10.12775/TMNA.2009.047}.
\bibitem{DGO21} K. Dekimpe, D.\,L. Gon\c{c}alves, O. Ocampo, The $R_\infty$ property for pure Artin braid groups, \emph{Monatsh.\ Math.} 195 (2021), 15--33, \url{https://doi.org/10.1007/s00605-020-01484-7}.
\bibitem{DGO24} K. Dekimpe, D.\,L. Gon\c{c}alves, O. Ocampo, Characteristic subgroups and the $R_\infty$-property for virtual braid groups, \emph{J.\ Algebra} 663 (2025), 20--47, \url{https://doi.org/10.1016/j.jalgebra.2024.09.002}.
\bibitem{DKT19} K. Dekimpe, T. Kaiser, S. Tertooy, The Reidemeister spectra of low dimensional crystallographic groups, \emph{J.\ Algebra} 533 (2019), 353--375, \url{https://doi.org/10.1016/j.jalgebra.2019.04.038}; \href{https://arxiv.org/abs/1709.07649}{arXiv:1709.07649}.
\bibitem{DP11} K. Dekimpe, P. Penninckx, The finiteness of the Reidemeister number of morphisms between almost-crystallographic groups, \emph{J.\ Fixed Point Theory Appl.} 9 (2011), 257--283, \url{https://doi.org/10.1007/s11784-011-0043-2}.
\bibitem{DKNS24} N.\,K. Dhanwani, P. Kumar, T.\,K. Naik, M. Singh, Linear representations, crystallographic quotients, and twisted conjugacy of virtual Artin groups, \href{https://arxiv.org/abs/2409.10270}{arXiv:2409.10270}.
\bibitem{FG10} A. Fel'shtyn, D.\,L. Gon\c{c}alves, Twisted conjugacy classes in symplectic groups, mapping class groups and braid groups, \emph{Geom.\ Dedicata} 146 (2010), 211--223, \url{https://doi.org/10.1007/s10711-009-9434-6}.
\bibitem{FN16} A. Fel'shtyn, T. Nasybullov, The $R_\infty$ and $S_\infty$ properties for linear algebraic groups, \emph{J.\ Group Theory} 19 (2016), 901--921, \url{https://doi.org/10.1515/jgth-2016-0004}.
\bibitem{FT15} A. Fel'shtyn, E. Troitsky, Aspects of the property $R_\infty$, \emph{J.\ Group Theory} 18 (2015), 1021--1034, \url{https://doi.org/10.1515/jgth-2015-0022}.
\bibitem{FP06} N. Franco, L. Paris, On a theorem of Artin, II, \emph{J.\ Group Theory} 9 (2006), 731--751, \url{https://doi.org/10.1515/jgt.2006.047}.
\bibitem{FH03} W.\,N. Franzsen, R.\,B. Howlett, Automorphisms of nearly finite Coxeter groups, \emph{Adv.\ Geom.} 3 (2003), 301--338, \url{https://doi.org/10.1515/advg.2003.018}. Author manuscript: \url{https://www.maths.usyd.edu.au/u/bobh/fh02.pdf}.
\bibitem{GGO17} D.\,L. Gon\c{c}alves, J. Guaschi, O. Ocampo, A quotient of the Artin braid groups related to crystallographic groups, \emph{J.\ Algebra} 474 (2017), 393--423, \url{https://doi.org/10.1016/j.jalgebra.2016.11.003}.
\bibitem{HL25} G. Hiss, R. Lutowski, The eigenvalue one property of finite groups, I, \emph{J.\ Algebra} 692 (2026), 592--626, \url{https://doi.org/10.1016/j.jalgebra.2025.12.021}; \href{https://arxiv.org/abs/2504.04978}{arXiv:2504.04978}.
\bibitem{HL26} G. Hiss, R. Lutowski, The eigenvalue one property of finite groups, II, \href{https://arxiv.org/abs/2601.09622}{arXiv:2601.09622}.
\bibitem{Juh11} A. Juh\'asz, Twisted conjugacy in certain Artin groups, in: \emph{Ischia Group Theory 2010}, World Sci., 2011, 175--195, \url{https://doi.org/10.1142/9789814350051_0014}.
\bibitem{LOST26} \^E. Leite, O. Ocampo, P.\,C.\,C. dos Santos J\'unior, A.\,C.\,M. Teixeira, A crystallographic quotient of the framed braid group and associated flat manifolds, \href{https://arxiv.org/abs/2610.33308}{arXiv:2610.33308} (2026).
\bibitem{Oca26} O. Ocampo, Crystallographic quotients of Artin braid groups and torus bundles over flat $3$-manifolds, \href{https://arxiv.org/abs/2610.20478}{arXiv:2610.20478} (2026).
\bibitem{Mar15} I. Marin, Crystallographic groups and flat manifolds from complex reflection groups, \emph{Geom.\ Dedicata} 182 (2016), 233--247, \url{https://doi.org/10.1007/s10711-015-0136-y}.
\bibitem{PS26} L. Paris, I. Soroko, Automorphisms of the Artin group of type $D_5$, \href{https://arxiv.org/abs/2606.26082}{arXiv:2606.26082}.
\bibitem{Sor26} I. Soroko, Property $R_\infty$ for Artin and Coxeter groups whose outer automorphisms are length-preserving, \href{https://arxiv.org/abs/2610.13904}{arXiv:2610.13904}.
\bibitem{Suc14} A.\,I. Suciu, Hyperplane arrangements and Milnor fibrations, \emph{Ann.\ Fac.\ Sci.\ Toulouse Math.} (6) 23 (2014), no.~2, 417--481, \url{https://doi.org/10.5802/afst.1412}.
\bibitem{SV24} I. Soroko, N. Vaskou, Property $R_\infty$ for new classes of Artin groups, \href{https://arxiv.org/abs/2409.18123}{arXiv:2409.18123}.
\bibitem{Hum90} J.\,E. Humphreys, \emph{Reflection Groups and Coxeter Groups}, Cambridge Univ.\ Press, 1990, \url{https://doi.org/10.1017/CBO9780511623646}.
\end{thebibliography}

\end{document}