\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern,amsmath,amssymb,amsthm,microtype}
\usepackage[a4paper,hmargin=24mm,vmargin=21mm]{geometry}
\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
\usepackage{xcolor}
\linespread{0.97}
\newif\ifannotated
\ifdefined\AnnotatedEdition\annotatedtrue\else\annotatedfalse\fi
\newtheoremstyle{compactplain}{5pt}{5pt}{\itshape}{}{\bfseries}{.}{.5em}{}
\newtheoremstyle{compactdefinition}{5pt}{5pt}{}{}{\bfseries}{.}{.5em}{}
\theoremstyle{compactplain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}[lemma]{Proposition}
\theoremstyle{compactdefinition}\newtheorem{definition}{Definition}
\newtheorem*{remark}{Remark}
\makeatletter
\renewcommand\section{\@startsection{section}{1}{\z@}
  {-2.2ex \@plus -.8ex \@minus -.2ex}{1.2ex \@plus .2ex}
  {\normalfont\Large\bfseries}}
\makeatother
\newcommand{\Inn}{\operatorname{Inn}}
\newcommand{\Mlt}{\operatorname{Mlt}}
\newcommand{\C}{\operatorname C}
\newcommand{\Z}{\operatorname Z}
\newcommand{\id}{\mathrm{id}}
\newcommand{\ann}[1]{\ifannotated\par\smallskip{\small\raggedright\color{blue!65!black}\noindent\textsf{Formal correspondence.} #1\par}\smallskip\fi}
\title{Bruck loops with abelian inner mapping groups:\texorpdfstring{\\}{ }a short proof}
\author{Bartosz Naskr\k{e}cki}
\newcommand{\authoraffiliations}{%
Faculty of Mathematics and Computer Science, Adam Mickiewicz University, Pozna\'n, Poland\par
Centre for Credible AI, Warsaw University of Technology, Warszawa, Poland}
\date{}
\hypersetup{pdftitle={Bruck loops with abelian inner mapping groups: a short proof},pdfauthor={Bartosz Naskręcki}}
\begin{document}
\begin{center}
{\Large\bfseries Bruck loops with abelian inner mapping groups:\par}
{\large\bfseries a short proof\par}
\smallskip
Bartosz Naskr\k{e}cki\par
{\small\authoraffiliations\par}
\end{center}
\begin{abstract}
Phillips and Stanovsk\'y proved that a Bruck loop with abelian inner mapping
group has central nilpotency class at most two and asked for a human-friendly
proof. We give a short self-contained proof: a displacement cocycle produces
a commutant-valued endomorphism, right alternativity for commutant elements
forces its image to be fixed, and cocycle rigidity makes that image central.
This yields the abelian center quotient.
\end{abstract}
\setlength{\abovedisplayskip}{5pt plus 2pt minus 2pt}
\setlength{\belowdisplayskip}{5pt plus 2pt minus 2pt}

\section{Introduction and elementary structure}
Phillips and Stanovsk\'y's proof uses over 16,000 lines of Waldmeister output,
or over 1,000 pages of structured equational reasoning \cite[\S2]{PS}.
Their Problem~5 asks for a human-friendly proof.

\begin{definition}
A \emph{loop} $Q$ has an identity $1$ and bijective translations
$L_x(y)=xy$, $R_x(y)=yx$ for $x\in Q$. A \emph{Bruck loop} here satisfies,
for all $x,y,z\in Q$, the left Bol identity and automorphic inverse property (AIP):
\begin{equation}\label{eq:axioms}
 x\bigl(y(xz)\bigr)=\bigl(x(yx)\bigr)z,
 \qquad (xy)^{-1}=x^{-1}y^{-1}.
\end{equation}
Compose permutations from right to left. Put
$H=\Inn(Q)=\Mlt(Q)_1$, the stabilizer of $1$ in $\Mlt(Q)=\langle L_x,R_x:x\in Q\rangle$.
The commutant $\C(Q)$ consists of $c\in Q$ with $ct=tc$ for every $t\in Q$.
The center $\Z(Q)$ consists of those $c\in\C(Q)$ satisfying
$(cx)y=c(xy)$, $(xc)y=x(cy)$, and $(xy)c=x(yc)$ for all $x,y\in Q$.
\end{definition}

\begin{theorem}[Phillips--Stanovsk\'y \cite{PS}]\label{thm:main}
If $Q$ is a Bruck loop and $\Inn(Q)$ is abelian, then $Q/\Z(Q)$ is an
abelian group. Thus $Q$ has central nilpotency class at most two.
\end{theorem}
No finiteness or divisibility is assumed. We recall Kreuzer's
automorphism argument~\cite{Kreuzer}.

\begin{lemma}[Bruck structure]\label{lem:structure}
Let $Q$ be a Bruck loop. For $u,v\in Q$, the map
$\lambda(u,v)=L_{uv}^{-1}L_uL_v$ is an automorphism in $H$.
For all $x,y,u,v\in Q$,
\begin{gather}
 L_{x^{-1}}=L_x^{-1},\quad L_{x^2}=L_x^2,\quad
 L_xL_yL_x=L_{x(yx)},\label{eq:basic}\\
 L_{uv}^{\,2}=L_uL_v^{\,2}L_u,\qquad
 \lambda(u,v)^{-1}=L_vL_uL_{uv}^{-1},\label{eq:square}\\
 \lambda(u,v)(vu)=uv.\label{eq:parameters}
\end{gather}
\end{lemma}
\begin{proof}
For $x\in Q$, choose $a\in Q$ with $ax=1$. Bol gives $L_xL_aL_x=L_x$, so
$L_a=L_x^{-1}$ and $xa=1$. Thus inverses are two-sided and
$x^{-1}(xz)=z=x(x^{-1}z)$ for $z\in Q$ (LIP).
Bol with $y=1$ gives left alternativity, proving \eqref{eq:basic}.
By AIP and LIP, $u(uv)^{-1}=u(u^{-1}v^{-1})=v^{-1}$. Thus
right multiplication by $(uv)^{-1}$ gives
\[
 \bigl(u((vv)u)\bigr)(uv)^{-1}
 =u\bigl((vv)(u(uv)^{-1})\bigr)
 =u\bigl((vv)v^{-1}\bigr)=uv.
\]
Left alternativity gives $(ww)w^{-1}=w(ww^{-1})=w$; applying this with
$w=uv$ and cancelling gives $u((vv)u)=(uv)^2$.
Equation \eqref{eq:basic} now gives the square formula,
and multiplication verifies the inverse word in \eqref{eq:square}.

For $\alpha=\lambda(u,v)$ and any $z\in Q$, that inverse word expresses
\[
 \alpha L_z\alpha^{-1}
 =L_{uv}^{-1}\bigl(L_u(L_vL_zL_v)L_u\bigr)L_{uv}^{-1}
\]
as three Bol sandwiches, hence as a left translation. Evaluating at $1$
identifies it as $L_{\alpha(z)}$, since $\alpha(1)=1$; hence $\alpha$ is an
automorphism. Evaluating the square formula at $1$ and cancelling on the left
gives $\alpha(vu)=uv$.
\end{proof}
\ann{\texttt{Loop.lean} proves the inverse laws and translation identities;
\texttt{Structure.lean} proves \texttt{bruck\_square}, \texttt{lam\_auto},
\texttt{gyrocomm}. The square identity supplies the automorphism proof and
quotient commutativity. No parameter-shift identity is required.}

\section{The displacement cocycle}
\begin{lemma}[Displacement cocycle]\label{lem:common}
Let $Q$ be a Bruck loop with $H$ abelian, and fix an automorphism
$\alpha\in H$. Define its \emph{displacement} $f:Q\to Q$ by
$f(x)=\alpha(x)x^{-1}$ and put $D_x=L_{\alpha(x)}L_x^{-1}$ for $x\in Q$.
For all $x,y,z\in Q$,
\begin{gather}
 D_x=L_{f(x)}=R_{\alpha(x)}R_x^{-1},\qquad \alpha(x)=f(x)x,\label{eq:common}\\
 f(xy)(zy)=f(y)\bigl((f(x)z)y\bigr).\label{eq:cocycles}
\end{gather}
\end{lemma}
\begin{proof}
Fix arbitrary $x,y\in Q$.
The permutation $\rho=R_{x^{-1}y}^{-1}R_yR_{x^{-1}}$ fixes $1$, so lies
in $H$. It also fixes $x$, since $xx^{-1}=1$ and $x(x^{-1}y)=y$.
As $\rho$ commutes with $\alpha$, it fixes $\alpha(x)$ too. Thus
$\alpha(x)(x^{-1}y)=(\alpha(x)x^{-1})y$, giving $L_{f(x)}=D_x$.
Naturality under $\alpha$, and its commutation with
$T_x=L_x^{-1}R_x\in H$, give
$L_{\alpha(x)}^{-1}R_{\alpha(x)}=L_x^{-1}R_x$.
Together these give \eqref{eq:common}, with its last assertion obtained by
evaluating at $x$.

Now $R_yR_x=R_{xy}\rho$ for $\rho=R_{xy}^{-1}R_yR_x\in H$.
Conjugate by $\alpha$, use $\alpha\rho=\rho\alpha$, and substitute
$R_{\alpha(t)}=D_tR_t$ (valid for every $t\in Q$) to obtain
$D_yR_yD_xR_x=D_{xy}R_yR_x$. Cancellation in the permutation group gives
$D_{xy}=D_yR_yD_xR_y^{-1}$; evaluation at $zy$ gives \eqref{eq:cocycles}.
\end{proof}
\ann{\texttt{Displacement.lean}: the \texttt{\_of\_central} versions of
\texttt{inner\_fixed\_transport}, \texttt{inner\_displacement\_L},
\texttt{common\_displacement}, \texttt{recover} and
\texttt{disp\_unreversed\_cocycle} require only $\alpha\in\Z(H)$.
The original names retain their full-\texttt{AIM} interfaces.
The last proof uses \texttt{Perm.factor\_cocycle}. Commutant image is not
assumed in this stage.}

\begin{lemma}[Cocycle calculus]\label{lem:cocycle}
In any loop $Q$ with two-sided inverses, LIP and AIP, a map $f:Q\to Q$
satisfying \eqref{eq:cocycles} for all $x,y,z\in Q$ has $f(1)=1$, preserves multiplication, and has image
in $\C(Q)$.
\end{lemma}
\begin{proof}
At $x=y=z=1$, the identity makes $f(1)$ idempotent, hence $f(1)=1$.
For arbitrary $x,y,t\in Q$, its case $z=1$ is
\begin{equation}\label{eq:basiccocycle}
 f(xy)y=f(y)(f(x)y).
\end{equation}
Set $x=y^{-1}$; left inverse cancellation and then right cancellation give
$f(y^{-1})=f(y)^{-1}$. Now apply \eqref{eq:cocycles} at
$(y^{-1},y,f(y)t)$ to obtain
\begin{equation}\label{eq:selfparameter}
 f(y)(ty)=(f(y)t)y.
\end{equation}
Equations \eqref{eq:basiccocycle} and \eqref{eq:selfparameter} yield
$f(xy)=f(y)f(x)$ by right cancellation. Consequently
$f((xy)y^{-1})=f(y)^{-1}(f(y)f(x))=f(x)$, an equality of images under $f$.
Now
\[
\begin{aligned}
 (f(x)y)y^{-1}
 &=\bigl(f(y^{-1})(f(xy)y)\bigr)y^{-1}
       &&\text{by \eqref{eq:basiccocycle} and LIP},\\
 &=f(y^{-1})\bigl((f(xy)y)y^{-1}\bigr)
       &&\text{by \eqref{eq:selfparameter} with }y^{-1},\\
 &=f((xy)y^{-1})(yy^{-1})=f(x)
       &&\text{by \eqref{eq:cocycles} at }(xy,y^{-1},y).
\end{aligned}
\]
Thus $(cy)y^{-1}=c$ for $c\in f(Q)$. Set $y=c^{-1}t^{-1}$: LIP gives
$cy=t^{-1}$ and AIP gives $y^{-1}=ct$, so $t^{-1}(ct)=c$.
Multiplying on the left by $t$ gives $ct=tc$.
Thus $f(Q)\subseteq\C(Q)$, and reversed multiplicativity becomes
$f(xy)=f(x)f(y)$.
\end{proof}
\ann{\texttt{Bruck.cocycle\_calculus} in \texttt{Generic.lean} states the
displayed implication under explicit identity, inverse, cancellation, LIP
and AIP laws, without Bol. \texttt{unreversed\_cocycle\_calculus} specializes
it to Bruck loops; \texttt{displacement\_commutant} and \texttt{disp\_mul}
apply it to displacement.}

\section{Fixed displacement values and rigidity}
\begin{lemma}[Rigidity at a fixed value]\label{lem:fixed}
Let $Q$ be a Bruck loop and let $f:Q\to Q$ satisfy \eqref{eq:cocycles}
for all $x,y,z\in Q$. Fix $y\in Q$ with $f(f(y))=1$. Then, for every $x,z\in Q$,
\begin{equation}\label{eq:fixed}
 f(xy)z=f(x)\bigl(f(y)z\bigr),\qquad
 f(x)(zy)=(f(x)z)y.
\end{equation}
\end{lemma}
\begin{proof}
Fix $x,z\in Q$. By Lemma~\ref{lem:cocycle}, $f$ is multiplicative and commutant-valued.
Equation \eqref{eq:cocycles} at $(x,f(y),z)$ gives
$f(x)(zf(y))=(f(x)z)f(y)$, hence
$R_{f(x)}R_{f(y)}=R_{f(y)}R_{f(x)}$.
For $a\in\C(Q)$ and $b\in Q$, the argument of \cite[Lemma 3.2]{KPV}
gives the following slight strengthening:
\begin{equation}\label{eq:bolproduct}
 a\in\C(Q),\quad R_aR_b=R_bR_a
 \quad\Longrightarrow\quad R_{ab}=R_bR_a.
\end{equation}
To see this, take arbitrary $t\in Q$ and cancel $a$ in the following Bol calculation:
\[
 a\bigl(t(ab)\bigr)=(a(ta))b=((ta)a)b
 =((ta)b)a=a\bigl((ta)b\bigr).
\]
Since $f(x)f(y)=f(xy)\in\C(Q)$, all three corresponding
right translations are left translations. Hence
$L_{f(xy)}=L_{f(x)}L_{f(y)}=L_{f(y)}L_{f(x)}$.
This proves the first assertion of \eqref{eq:fixed}. Substitution into
\eqref{eq:cocycles} gives
$f(y)(f(x)(zy))=f(y)((f(x)z)y)$; left cancellation by $f(y)$ proves the second.
\end{proof}
\ann{\texttt{Calculus.lean} proves the Bol observation as
\texttt{commutant\_right\_product\_apply} and the two conclusions as
\texttt{cocycle\_rigidity}. Its input \texttt{RightCocycle} puts the factor
$f(y)$ on the right; \texttt{disp\_right\_cocycle} makes this equivalent
rearrangement using the already proved commutant image.}

\begin{proposition}[Fixed displacement image]\label{prop:image}
Let $Q$ be a Bruck loop with $H$ abelian. Fix $u,v\in Q$, put
$\alpha=\lambda(u,v)$, and define $f:Q\to Q$ by $f(x)=\alpha(x)x^{-1}$.
Then $\alpha(f(z))=f(z)$ for every $z\in Q$.
\end{proposition}
\begin{proof}
By Lemmas~\ref{lem:common} and \ref{lem:cocycle}, $f$ preserves multiplication,
identity and inverses. Put $a=f(u)$ and $b=f(v)$, both in $\C(Q)$.
Applying $f$ to the definition of $\lambda$ gives
$f\alpha=\lambda(a,b)f$; also $\alpha f=f\alpha$ by the definition of $f$.
Thus $\alpha(f(z))=\lambda(a,b)(f(z))$ for every $z\in Q$.
We first fix the single value $b$. Taking equal factors in
\eqref{eq:bolproduct} gives $(tb)b=t(bb)$ for every $t\in Q$, whence
\[
 \lambda(a,b)(b)=(ab)^{-1}\bigl(a(bb)\bigr)
 =(ab)^{-1}\bigl((ab)b\bigr)=b.
\]
Thus $\alpha(b)=b$ and $f(b)=1$. This one value suffices:
Lemma~\ref{lem:fixed}, applied at $(u,v)$, gives
$L_{ab}=L_aL_b$, hence $\lambda(a,b)=\id$.
Therefore $\alpha(f(z))=f(z)$ for every $z$.
\end{proof}
\ann{\texttt{generator\_fixes\_displacement\_of\_central} proves the proposition
under $\lambda(u,v)\in\Z(H)$; the original name is its \texttt{AIM} specialization.
The parameter case uses \texttt{commutant\_right\_alt}, obtained by
specializing the already proved right-product lemma. The shared identity \texttt{Endo.map\_lam} transports the left inner map
through the displacement endomorphism. No gyro-loop identity is used. The corollary
\texttt{displacement\_square\_zero\_of\_central} supplies the hypothesis for the final
application of \texttt{cocycle\_rigidity}.}

\section{The full center and the quotient}
\begin{lemma}[Center criterion]\label{lem:center}
Let $Q$ be a left Bol loop. An element $c\in Q$ belongs to the center if
$ct=tc$ for every $t\in Q$ and $(cx)y=c(xy)$ for all $x,y\in Q$.
\end{lemma}
\begin{proof}
Bol and the assumed left nuclearity give
$c(x(cy))=(c(xc))y=c((xc)y)$; cancellation proves middle nuclearity.
Commuting $c$ through
$(xy)c=c(xy)=(cx)y=(xc)y=x(cy)=x(yc)$ proves right nuclearity.
\end{proof}

For $c,d\in\Z(Q)$, nuclearity gives
\[
 (cd)x=c(dx)=c(xd)=(cx)d=(xc)d=x(cd),
 \quad ((cd)x)y=c(d(xy))=(cd)(xy).
\]
Hence $cd$ is central by Lemma~\ref{lem:center}; so is $1$.
Also $c(xc^{-1})=(cx)c^{-1}=(xc)c^{-1}=x(cc^{-1})=x=c(c^{-1}x)$, proving that
$c^{-1}$ commutes with $x$. Multiplying the desired left nuclear identity
for $c^{-1}$ on the left by $c$ reduces both sides to $xy$, by left
nuclearity of $c$ and LIP. Thus $c^{-1}$ is central.

For $x,y\in Q$, write $x\sim y$ if $y=cx$ for some $c\in\Z(Q)$.
The closure just proved makes this an equivalence relation.
For $c,d\in\Z(Q)$ and $x,y\in Q$,
$(cx)(dy)=(cd)(xy)$ by nuclearity, and $(cx)^{-1}=c^{-1}x^{-1}$ by AIP.
Hence the class operations $[x][y]=[xy]$ and $[x]^{-1}=[x^{-1}]$ are well defined.

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Fix arbitrary $u,v\in Q$, put $\alpha=\lambda(u,v)$ and define its displacement
$f=f_{u,v}:Q\to Q$ by $f(x)=\alpha(x)x^{-1}$.
For every $y\in Q$, Proposition~\ref{prop:image} gives $\alpha(f(y))=f(y)$,
hence $f(f(y))=\alpha(f(y))(f(y))^{-1}=f(y)(f(y))^{-1}=1$.
Lemma~\ref{lem:fixed} yields $(f(x)t)y=f(x)(ty)$ for all $x,t,y\in Q$.
Since $f(Q)\subseteq\C(Q)$ by Lemma~\ref{lem:cocycle}, Lemma~\ref{lem:center}
gives $f(Q)\subseteq\Z(Q)$.

\emph{Associativity.} For every $z\in Q$, recovery \eqref{eq:common} gives
$[\alpha(z)]=[f(z)z]=[z]$. Taking classes in $(uv)\alpha(z)=u(vz)$, which
defines $\lambda$, gives $([u][v])[z]=[u]([v][z])$.

\emph{Commutativity.} Equation~\eqref{eq:parameters} and recovery \eqref{eq:common} give
$uv=\alpha(vu)=f(vu)(vu)$. The witness $f(vu)\in\Z(Q)$ gives
$[u][v]=[uv]=[vu]=[v][u]$.

Every class has a representative; the identity and inverses descend, so
$Q/\Z(Q)$ is an abelian group. Its projection has kernel $\Z(Q)$, giving the central
series $1\leq\Z(Q)\leq Q$.
\end{proof}
\ann{\texttt{Bruck.bol\_nuclei\_of\_commutant\_left} in \texttt{Generic.lean}
uses only multiplication, left cancellation and Bol. \texttt{Center.lean}
specializes this to the full four-field center criterion and proves
closure, the explicit equivalence relation, compatibility, surjectivity,
and \texttt{project\_eq\_one\_iff}. \texttt{Main.lean} proves the quotient
laws. \texttt{Contract.lean} fixes the exact full-inner-group hypothesis;
\texttt{Equational.lean} recovers the original associator target under full
\texttt{AIM}; it does not derive \texttt{AIM} from the historical finite list
of generator-commutation equations. The quotient characterization of class
at most two is used as the definition; no general upper-central-series
library is assumed.}

\begin{remark}
Abelianness of $H$ is used only in Lemma~\ref{lem:common}, to commute the chosen
$\alpha$ with elements of $H$. Thus the theorem also holds if every
$\lambda(u,v)$ belongs to the group center $\Z(H)$.
\end{remark}
\ann{\texttt{bruck\_central\_left\_inner\_class\_at\_most\_two} formalizes the
remark: \texttt{CentralLeftInner} means $\lambda(u,v)\in\Z(H)$ for all $u,v$.
\texttt{bruck\_aim\_class\_at\_most\_two} retains the original hypothesis.
\texttt{Model8.lean} also proves full \texttt{AIM} for its nonassociative model,
with explicit failures of global right inverse cancellation and of
automorphicity for a particular inner mapping.}

\begingroup\footnotesize
\paragraph{AI disclosure and formalization.}
GPT-Astra generated the exposition and Lean development under the author's
direction. Inspection of the original proof suggested the displacement approach.
The cocycle calculation was reconstructed from automated proof-search output
and checked in Lean. Sources:
\href{https://github.com/nasqret/bruck-palomar}{\texttt{nasqret/bruck-palomar}}
(revision \href{https://github.com/nasqret/bruck-palomar/tree/2b9313afa2364c4af3b5b0390bdc5b3d2ed2aa72}{\texttt{2b9313a}}).
Palomar submission \href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/38102682798}{\texttt{svl2zwiscn4f}}:
mechanically verified; registry review pending.
\par\endgroup

\begin{thebibliography}{9}\small\setlength{\itemsep}{2pt}
\bibitem{PS} J. D. Phillips and D. Stanovsk\'y,
\href{https://doi.org/10.1080/00927872.2011.579587}{\emph{Bruck loops with abelian inner mapping groups}},
Comm. Algebra \textbf{40} (2012), no.~7, 2449--2454.
\bibitem{Kreuzer} A. Kreuzer,
\href{https://doi.org/10.1017/S0305004197001771}{\emph{Inner mappings of Bruck loops}}, Math. Proc. Cambridge Philos. Soc.
\textbf{123} (1998), 53--57.
\bibitem{KPV} M. K. Kinyon, J. D. Phillips, and P. Vojt\v{e}chovsk\'y,
\href{https://doi.org/10.1090/S0002-9947-07-04391-7}{\emph{When is the commutant of a Bol loop a subloop?}},
Trans. Amer. Math. Soc. \textbf{360} (2008), no.~5, 2393--2408.
\end{thebibliography}
\end{document}