\documentclass[11pt,reqno]{amsart}

\usepackage[margin=1.15in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype}
\usepackage{xurl}
\usepackage{xcolor}
\usepackage{listings}
\usepackage[hidelinks]{hyperref}
\usepackage{aliascnt}
\usepackage[nameinlink,noabbrev]{cleveref}

\definecolor{keywordcolor}{RGB}{88,41,120}
\definecolor{sortcolor}{RGB}{35,79,140}
\definecolor{symbolcolor}{RGB}{125,48,48}
\definecolor{commentcolor}{RGB}{42,105,62}
\input{lstlean_paper.tex}
\lstset{
  language=lean,
  basicstyle=\ttfamily\footnotesize,
  frame=single,
  framerule=0.25pt,
  rulecolor=\color{black!35},
  backgroundcolor=\color{black!2},
  xleftmargin=0.7em,
  xrightmargin=0.7em,
  aboveskip=0.65\baselineskip,
  belowskip=0.65\baselineskip,
  breaklines=true,
  columns=fullflexible,
  captionpos=b
}

\newtheorem{theorem}{Theorem}[section]
\newaliascnt{proposition}{theorem}
\newtheorem{proposition}[proposition]{Proposition}
\aliascntresetthe{proposition}
\newaliascnt{lemma}{theorem}
\newtheorem{lemma}[lemma]{Lemma}
\aliascntresetthe{lemma}
\newaliascnt{corollary}{theorem}
\newtheorem{corollary}[corollary]{Corollary}
\aliascntresetthe{corollary}
\theoremstyle{definition}
\newaliascnt{definition}{theorem}
\newtheorem{definition}[definition]{Definition}
\aliascntresetthe{definition}
\newaliascnt{remark}{theorem}
\newtheorem{remark}[remark]{Remark}
\aliascntresetthe{remark}
\newcommand{\Spa}{\operatorname{Spa}}
\newcommand{\im}{\operatorname{im}}
\newcommand{\cO}{\mathcal O}
\newcommand{\onto}{\twoheadrightarrow}

\title{Uniform sheafy Tate rings that are not stably uniform}
\author{Christopher Birkbeck}
\author{Alex Torzewski}
\date{}

\begin{document}

\begin{abstract}
Buzzard--Verberkmoes and Mihara show that a stably uniform Tate Huber
ring is sheafy.  We construct examples of uniform and strongly sheafy Tate rings
which are not stably uniform, answering Question~7 of Kedlaya's
\emph{Nonarchimedean Scottish Book}.  In the first example a rational
localisation is non-reduced, whilst in the second the rational localisation
is an integral domain but is not uniform.  The two main results are due to
ChatGPT 5.6 Sol.
Both constructions, the rational localisations witnessing failure of stable
uniformity, and their strong sheafiness have been formalised in Lean~4.
\end{abstract}

\subjclass[2020]{Primary 14G22; Secondary 13J10}
\keywords{Huber ring, adic spectrum, sheafiness, stable uniformity, rational localisation, Milnor square}

\maketitle

\section{Introduction}

Work of Buzzard--Verberkmoes and, separately, Mihara shows that every stably
uniform Tate Huber ring is sheafy, but leaves open whether every uniform sheafy
Tate Huber ring is stably uniform \cite{BV,Mihara}.  Hansen and Kedlaya ask
this explicitly \cite[Remark~3.16]{HK}; it is also Question~7 of Kedlaya's
\emph{Nonarchimedean Scottish Book} \cite{Scottish}.  We answer this question
in the negative, by constructing uniform and sheafy Tate rings that are not
stably uniform.  In fact, we prove the stronger statement that both examples
are strongly sheafy.
Both are non-noetherian, so neither Huber's theorem for strongly noetherian
Tate rings nor the stably uniform criterion applies.

The examples and proofs described here were found with the help of AI agents,
specifically ChatGPT 5.6 Sol.  In \Cref{sec:discovery} we describe how we used
ChatGPT in the search for these examples.  Every result discussed here has
also been fully formalised in Lean by Claude Code, and
\cref{sec:formalisation} records the formal definitions and theorem
statements.  This article was prepared with the help of AI from an initial
human-written skeleton.  We have kept many of the names given to our objects
by the AI systems.  This is a conscious choice intended to make it easier to
trace sources that may have influenced their work; see
\Cref{rem:earlier-work}.

We start with the ``finite-jet pullback'' example.
This is a non-noetherian uniform integral domain for which a certain rational
localisation is non-reduced, and hence is no longer uniform.  Let $k$ be a
complete discretely valued nonarchimedean field, with valuation ring
$k^\circ$, uniformizer $\varpi$, and residue field $\widetilde{k}$.  Put
\[
  L_0=k^\circ\langle W,W^{-1}\rangle,
  \qquad
  B_0=k^\circ\langle W,Q\rangle/(Q^2),
\]
\[
  C_0=L_0\langle Q\rangle,
  \qquad
  D_0=L_0\langle Q\rangle/(Q^2),
\]
where $k^\circ\langle W,W^{-1}\rangle$ means
$k^\circ\langle W,V\rangle/(WV-1)$.  There are natural maps
$B_0\to D_0$ and $C_0\onto D_0$.  Define
\[
  A_0=B_0\times_{D_0}C_0,
  \qquad
  A=A_0[1/\varpi],
\]
and endow $A$ with the topology defined by the ring of definition $A_0$.

The main result is the following.

\begin{theorem}\label{thm:main}
The ring $A$ is a complete uniform non-noetherian Tate $k$-algebra and an
integral domain, with $A^\circ=A_0$.  It is strongly sheafy; in particular,
the Huber pair $(A,A^\circ)$ is sheafy.
However,
\[
  A\left\langle \frac{W}{\varpi}\right\rangle
  \cong k\langle X,Q\rangle/(Q^2),
  \qquad X=\frac{W}{\varpi},
\]
so $A$ is not stably uniform.
\end{theorem}

This construction also gives a new example solving Problems~24 and 28 of the
\emph{Nonarchimedean Scottish Book}.  We recall the two problems and give the
argument in \cref{sec:problems-24-28}.

The key element in this example is that after the rational localisation
$A\to A\langle W/\varpi\rangle$, $Q^2$ vanishes whereas $Q$ does not. The proof uses Milnor squares of complete Tate rings.  Recall that a cartesian square of
rings with a surjective leg is called a Milnor square \cite[Section~2]{Milnor}; the
complete Tate setting is used by Kerz--Saito--Tamme in their work on analytic
$K$-theory \cite[Section~3]{KST}.

\begin{definition}\label{def:strict-milnor}
A commutative square of complete Tate $k$-algebras
\[
\begin{matrix}
A&\longrightarrow&C\\
\downarrow&&\downarrow\\
B&\longrightarrow&D
\end{matrix}
\]
is a \emph{strict Milnor square} if it is cartesian, the sequence of underlying topological $k$-vector spaces
\[
  0\longrightarrow A\longrightarrow B\oplus C
  \xrightarrow{\ (b,c)\mapsto \bar b-\bar c\ }D\longrightarrow 0
\]
is strict exact, and $C\to D$ is a strict surjection.
\end{definition}

The maps $C\to D$ and $B\oplus C\to D$ are continuous surjections between
complete normed $k$-vector spaces, and $A$ has the subspace topology as the
kernel of the second.  The nonarchimedean open mapping theorem
\cite[Lemma~3.1]{KST} therefore shows that the square defining $A$ is strict.
Our main input is that,
for this finite-jet square, the strict exact row persists after completed rational
localisation and is compatible with refinement.  This transfers sheafiness from
$B,C,D$ to $A$, giving new ways for proving that these rings are sheafy.  The
second example shows that the failure of stable uniformity
need not come from a non-reduced localisation.

\begin{remark}[Relation with earlier work]\label{rem:earlier-work}
It is difficult to understand exactly what sources an AI agent such as
ChatGPT may have used in doing this work.  In the interest of giving
appropriate credit, we have listed here closely related work that may have
been used in the development of the results here.

Buzzard--Verberkmoes construct a uniform affinoid ring with a rational
localisation which is not uniform
and, separately, a uniform affinoid ring whose structure presheaf is not a
sheaf \cite[Propositions 17 and 18]{BV}.  Mihara gives further examples of both
phenomena \cite{Mihara}.  These examples do not give a uniform sheafy ring which is not
stably uniform.

Ben-Bassat--Kremnizer prove strict two-term resolutions
for Weierstrass and Laurent localisations, and reduce a general rational
localisation to these cases \cite[Lemmas~5.13--5.14]{BBK}.
Bambozzi--Kremnizer formulate rational localisation in terms of Koszul
complexes and prove strict Koszul regularity
\cite[Notation~4.3, Definitions~4.5--4.6, Proposition~4.9,
Lemma~4.11, and Corollary~4.13]{BK}.  The bounded-denominator estimates in
\Cref{lem:koszul} are the form needed to show that rational localisation
preserves the finite-jet Milnor square.  The resulting uniform sheafy domain
which is not stably uniform appears to be new.

The weighted-parity construction of \cref{sec:second-example} is closer to the
infinite monomial-support examples of Buzzard--Verberkmoes and Mihara.  Its additional
feature is that rational localisation can be calculated in a noetherian
finite-variable subring.
\end{remark}


\section{Conventions and notation}\label{sec:conventions}

We follow Huber for Huber pairs, adic spectra, rational subsets, and rational
localisation \cite{Huber94}, and use Wedhorn's account for strong
noetherianity and sheafiness
\cite[Proposition and Definition~6.36, Section~8.1]{Wedhorn}; the
bounded-denominator language for strictness follows Buzzard--Verberkmoes
\cite{BV}, and the quotient presentation of a rational localisation is also
discussed by Hansen--Kedlaya \cite{HK}.

\begin{itemize}
\item \emph{Tate topology.}
Throughout, $E$ denotes a complete Tate $k$-algebra.  In the discretely valued setting of this paper, this means that $E$ contains a topologically nilpotent unit and admits an open bounded $k^\circ$-subalgebra $E_0$ such that
\[
  E=E_0[1/\varpi],
  \qquad
  \{\varpi^nE_0\}_{n\geq0}
\]
is a basis of neighbourhoods of zero.  Such an $E_0$ is called a \emph{ring of definition}.  We always choose it closed, hence $\varpi$-adically complete.  A subset of $E$ is bounded if it is contained in $\varpi^{-r}E_0$ for some $r\geq0$.

\item \emph{Uniformity and noetherianity.}
We write $E^\circ$ for the ring of power-bounded elements.  The ring $E$ is
\emph{uniform} if $E^\circ$ is bounded, and \emph{strongly noetherian} if
$E\langle Z_1,\ldots,Z_s\rangle$ is noetherian for every $s\geq0$.  A Tate ring
is \emph{stably uniform} if every rational localisation is uniform.

\item \emph{Huber pairs and sheafiness.}
A \emph{ring of integral elements} is an open subring
$E^+\subseteq E^\circ$ which is integrally closed in $E$.  We call the Huber pair
$(E,E^+)$ \emph{sheafy} when its structure presheaf, valued in complete
topological rings, satisfies the sheaf condition.  Thus, for a finite rational cover
$U=\bigcup_iU_i$, restriction identifies $\mathcal O(U)$ homeomorphically
with the subspace of $\prod_i\mathcal O(U_i)$ consisting of tuples whose
restrictions to every $U_i\cap U_j$ agree.

\item \emph{Strictness.}
We use the following bounded-denominator form of strictness.  Let $u:M\to N$ be a continuous $k$-linear map, and let $M_0\subset M$ and $N_0\subset N$ be open bounded $k^\circ$-submodules.  Then $u$ is strict if and only if there exists $a\geq0$ such that
\[
  \varpi^a\bigl(u(M)\cap N_0\bigr)\subset u(M_0).
\]
For a surjection this becomes $\varpi^aN_0\subset u(M_0)$.  For an injection it says that the inverse image of $N_0$ is bounded in $M$.  This is the criterion used by Buzzard--Verberkmoes \cite[Lemma~2]{BV}.  We use the term \emph{strict Milnor square} in the sense of \Cref{def:strict-milnor}; the underlying algebraic terminology is standard \cite{Milnor,KST}.

\item \emph{Rational localisation.}
We take every rational datum to have at least one numerator; an empty list may be
padded by $f_1=0$.  Let
$\alpha=(f_1,\dots,f_m;g)$ be a rational datum in $E$, so the ideal generated by
$g,f_1,\dots,f_m$ is open.  Since $E$ is a Tate $k$-algebra, this ideal is the unit ideal.  After multiplying the entire datum by a common power of $\varpi$, we may assume that all entries lie in $E_0$.

The rational localisation $E_\alpha$ is the $\varpi$-adic completion of $E[1/g]$ for the ring of definition generated by
\[
  E_0\left[\frac{f_1}{g},\dots,\frac{f_m}{g}\right].
\]
For such a ring of definition $R$, we use the notation
\[
  \widehat R=\varprojlim_{n\geq1}R/\varpi^nR,
  \qquad
  \ker(R\longrightarrow\widehat R)=\bigcap_{n\geq1}\varpi^nR.
\]
$E_\alpha$ is independent of the ring of definition and of the presentation of the rational
domain, and it is transitive under rational refinement.  Put
\[
  T_E=E\langle T_1,\dots,T_m\rangle
  =E_0\langle T_1,\dots,T_m\rangle[1/\varpi],
  \qquad r_i=gT_i-f_i,
\]
and
\[
  I_{E,\alpha}:=(r_1,\dots,r_m)
  =\operatorname{im}\left(
    T_E^m\xrightarrow{\ d_{1,E}\ }T_E
  \right)\subset T_E,
\]
  where
  $d_{1,E}(u_1,\dots,u_m)=\sum_i u_i(gT_i-f_i).$ Then we have
\begin{equation}\label{eq:graph-model}
  E_\alpha\cong T_E/\overline{I_{E,\alpha}}.
\end{equation}
Here the bar is necessary until the ideal has been shown to be closed.  This is the
standard quotient presentation of rational localisation; see
\cite[Notations, (1.2), Proposition~1.3, Lemma~1.5]{Huber94} and
\cite[Definition~3.6]{HK}.
\end{itemize}


\section{The finite-jet ring}\label{sec:the-global-ring}

In this section we identify the finite-jet algebra with a concrete subring of
$C$ and prove that it is a complete uniform domain.  Recall that
\[
  L_0=k^\circ\langle W,W^{-1}\rangle,
  \qquad
  B_0=k^\circ\langle W,Q\rangle/(Q^2),
\]
\[
  C_0=L_0\langle Q\rangle,
  \qquad
  D_0=L_0\langle Q\rangle/(Q^2),
\]
where $k^\circ\langle W,W^{-1}\rangle$ denotes
$k^\circ\langle W,V\rangle/(WV-1)$.  The natural maps
$B_0\to D_0$ and $C_0\onto D_0$ allow us to define
\[
  A_0=B_0\times_{D_0}C_0.
\]
We write
\[
  A=A_0[1/\varpi],\quad
  L=L_0[1/\varpi],\quad
  B=B_0[1/\varpi],\quad
  C=C_0[1/\varpi],\quad
  D=D_0[1/\varpi].
\]
Each of these Tate rings carries the topology defined by the corresponding
subscript-zero ring.

The results in this section and the next do not require the valuation on $k$
to be discrete.  They hold for any complete ultrametric normed field $k$ and
any chosen $\varpi\in k^\times$ with $0<|\varpi|<1$, with the same definitions
using the norm unit ball $k^\circ$.  We return to the discretely valued
hypothesis in \cref{sec:localisation-milnor}.

The quotient map $C_0\to D_0$ has a continuous $k^\circ$-linear section
\[
  \sigma:D_0\longrightarrow C_0,\qquad
  \sigma(f_0+Qf_1)=f_0+Qf_1,
\]
obtained by viewing the unique representative of $Q$-degree at most one as
an element of $C_0$.
Consequently
\[
  0\longrightarrow A_0\longrightarrow B_0\oplus C_0
  \longrightarrow D_0\longrightarrow 0
\]
is exact, and $A_0$ is $\varpi$-adically complete.  After inverting $\varpi$ we obtain a strict Milnor square
\[
\begin{matrix}
A&\longrightarrow&C\\
\downarrow&&\downarrow\\
B&\longrightarrow&D.
\end{matrix}
\]

The map $B_0\to D_0$ is injective.  Projection to $C_0$ therefore identifies $A_0$ with the subring
\begin{equation}\label{eq:coefficient-A0}
  A_0=
  \left\{
  f_0(W)+Qf_1(W)+Q^2h(W,W^{-1},Q):
  f_0,f_1\in k^\circ\langle W\rangle,
  \ h\in C_0
  \right\}.
\end{equation}
Equivalently, $A_0$ consists of the restricted series
\[
  \sum_{(a,b)\in S}c_{a,b}W^aQ^b,
  \qquad
  S=\{(a,b)\in\mathbb Z\times\mathbb N: b\leq 1\Rightarrow a\geq 0\},
\]
with $c_{a,b}\in k^\circ$.  Here restricted means that, for every $n$, only finitely many coefficients are nonzero modulo $\varpi^n$.  The set $S$ is closed under addition, so this is a subring of $C_0$.  The same description with coefficients in $k$ gives $A\subset C$.


Equip $A,B,C,D$ with the coefficientwise Gauss norms whose unit balls are
$A_0,B_0,C_0,D_0$, respectively.  Write
\[
  \iota_B:A\to B,\qquad \iota_C:A\to C,\qquad
  \rho_B:B\to D,\qquad \rho_C:C\to D
\]
for the structural maps, and give \(A\) the restricted Gauss norm from \(C\).  For
\(a=f_0+Qf_1+Q^2h\), the coefficient formulas give
\begin{equation}\label{eq:structural-map-bounds}
  \lVert\iota_C(a)\rVert_C=\lVert a\rVert_A,
  \qquad
  \lVert\iota_B(a)\rVert_B\leq \lVert a\rVert_A,
  \qquad
  \lVert\rho_B(b)\rVert_D\leq\lVert b\rVert_B,
  \qquad
  \lVert\rho_C(c)\rVert_D\leq\lVert c\rVert_C.
\end{equation}
Thus every structural map is norm-nonincreasing.

\begin{proposition}\label{prop:uniform-domain}
The ring $A$ is a complete uniform non-noetherian Tate $k$-algebra and an
integral domain.  Moreover,
\[
  A^\circ=A_0.
\]
\end{proposition}

\begin{proof}
The Gauss norm on $L=k\langle W,W^{-1}\rangle$ is multiplicative, and the
restricted Gauss norm on $C=L\langle Q\rangle$ is therefore multiplicative as
well.  In particular, $C$ is a domain, and hence so is its subring $A$.  The
constant- and linear-coefficient maps $C\to L$ are continuous, and
$k\langle W\rangle$ is closed in $L=k\langle W,W^{-1}\rangle$ for the Gauss
norm.  Hence the condition that these two coefficients lie in
$k\langle W\rangle$ defines a closed subring of $C$, so $A$ is complete.  The
image of $\varpi$ in $A$ is a topologically nilpotent unit, and therefore $A$
is a Tate ring.

The coefficient description of $A_0$ shows that it is exactly the unit ball
for the restricted Gauss norm on $A$.  Since this norm is multiplicative,
\[
  \lVert a^n\rVert=\lVert a\rVert^n.
\]
It follows that $a$ is power-bounded if and only if $\lVert a\rVert\leq1$.
Thus $A^\circ=A_0$, and the unit ball is bounded, so $A$ is uniform.

To see that $A$ is not noetherian, let $J=\ker(\iota_B)=Q^2C\subset A$.  If $J$ were
generated by $a_1,\ldots,a_r$, write $b_i\in L$ for the coefficient of $Q^2$
in $a_i$.  Now, for every $\ell\in L$, we can write
\[
  Q^2\ell=\sum_i x_i a_i,\qquad x_i\in A,
\]
and write $c_i$ for the constant coefficient of $x_i$ as a series in $Q$.
By \eqref{eq:coefficient-A0}, we have $c_i\in k\langle W\rangle$.  Since
$a_i\in Q^2C$, its coefficients in degrees $0$ and $1$ vanish.  The
coefficient of $Q^2$ in $x_i a_i$ is therefore exactly $c_i b_i$.
Comparing the coefficients of $Q^2$ on both sides gives
\[
  \ell=\sum_i c_i b_i,\qquad c_i\in k\langle W\rangle.
\]
Thus $b_1,\ldots,b_r$ would generate $L$ as a
$k\langle W\rangle$-module.  This is impossible.  Indeed, it would make
$W^{-1}$ integral over $k\langle W\rangle$.  Multiplying a monic relation for
$W^{-1}$ of degree $n$ by $W^n$ would put $1$ in the proper ideal
$(W)\subset k\langle W\rangle$.  Thus $J$ is not finitely generated, and $A$
is not noetherian.
\end{proof}


\section{A rational localisation which is not uniform}

We next compute the rational chart which witnesses the failure of stable
uniformity.

Consider the datum
\[
  \alpha=(W;\varpi).
\]
The ideal \((\varpi,W)\) is open, since \(\varpi\) is a unit in \(A\).  Let
\[
  A_\alpha=A\left\langle\frac{W}{\varpi}\right\rangle
\]
be the corresponding rational localisation on which $|W|\leq |\varpi|$, and write
$X=W/\varpi$.  Since $\varpi$ is already invertible in $A$, the algebraic
localisation does not change the ring.  More explicitly,
$A_\alpha$ is obtained by taking the $\varpi$-adic
completion of $A_0[X]\subset A$ and then inverting $\varpi$.

\begin{proposition}\label{prop:bad-chart}
There is a canonical isomorphism of complete topological rings
\[
  A_\alpha\cong k\langle X,Q\rangle/(Q^2),
  \qquad W\longmapsto\varpi X,\quad Q\longmapsto Q.
\]
\end{proposition}

\begin{proof}
Put
\[
  T_0=k^\circ\langle X,Q\rangle/(Q^2),
  \qquad T=T_0[1/\varpi].
\]
Let $\rho:A\to A_\alpha$ be the canonical map.  We first show that
\begin{equation}\label{eq:q2-killed-on-chart}
  Q^2C\subseteq\ker(\rho).
\end{equation}
Take $y\in Q^2C$, and choose $r\geq0$ such that
$\varpi^r y\in Q^2C_0$.  For every $n\geq0$, the coefficient description of
$A_0$ gives
\[
  W^{-n}\varpi^r y\in A_0.
\]
Multiplication by $W^{-n}$ only introduces negative powers of $W$ in terms
of $Q$-degree at least two.  In $A_0[X]$, where $W=\varpi X$, we therefore
have
\[
  \varpi^r y
   =W^n(W^{-n}\varpi^r y)
   =\varpi^nX^n(W^{-n}\varpi^r y)\in\varpi^nA_0[X]
\]
for every $n$.  Hence $\varpi^r y$ maps to zero in
$\widehat{A_0[X]}$.  Since $\varpi$ is invertible in
$A_\alpha$, this proves \eqref{eq:q2-killed-on-chart}.

We now construct the isomorphism.  Recall that the map
$\iota_B:A\to B$ from the defining pullback is given by
\[
  f_0(W)+Qf_1(W)+Q^2h\longmapsto f_0(W)+Qf_1(W);
\]
it simply discards the terms divisible by $Q^2$.  The substitution
$W\mapsto\varpi X$, $Q\mapsto Q$ defines a continuous homomorphism
$B\to T$.  Their composite is
\[
  \theta:A\longrightarrow T,\qquad
  f_0(W)+Qf_1(W)+Q^2h\longmapsto
  f_0(\varpi X)+Qf_1(\varpi X).
\]
It sends $A_0$ into $T_0$ and sends $W/\varpi$ to $X$.  It therefore sends
$A_0[X]$ into $T_0$ and extends, first to the completions and then
after inverting $\varpi$, to a continuous homomorphism
\[
  \Phi:A_\alpha\longrightarrow T.
\]

Set
\[
  \overline X=\rho(W)/\varpi,\qquad \overline Q=\rho(Q).
\]
Both elements are power-bounded: they belong to the completed ring of
definition coming from $A_0[X]$.  Moreover,
\(\overline Q^{\,2}=0\) by \eqref{eq:q2-killed-on-chart}.  Evaluation at
$\overline X$ therefore gives a continuous homomorphism
\[
  \Psi:T\longrightarrow A_\alpha,\qquad
  f+Qg\longmapsto f(\overline X)+g(\overline X)\overline Q.
\]

It remains to check the two composites.  Write
$a=f_0(W)+Qf_1(W)+y\in A$, with $y\in Q^2C$.  Then
\[
  (\Psi \circ \Phi)(\rho(a))
  =f_0(\varpi\overline X)+\overline Qf_1(\varpi\overline X)
  =\rho\bigl(f_0(W)+Qf_1(W)\bigr)
  =\rho(a),
\]
where the last equality uses \eqref{eq:q2-killed-on-chart}.  The
image of $A$ is dense in $A_\alpha$, so continuity gives
$\Psi \circ \Phi=1$.  Conversely, $\Phi \circ \Psi$ fixes $k$, $X$ and $Q$, and hence is
the identity on the dense subring $k[X,Q]/(Q^2)$ of $T$.  It follows by
continuity that $\Phi\circ \Psi=1$.  Thus $\Phi$ and $\Psi$ are inverse continuous
homomorphisms.
\end{proof}

\begin{proposition}\label{prop:not-stably-uniform}
The ring $A$ is not stably uniform.
\end{proposition}

\begin{proof}
In $T=k\langle X,Q\rangle/(Q^2)$, every element of the line $kQ$ is nilpotent and hence power-bounded.  This line is not bounded with respect to the ring of definition $T_0$: for every $r\geq 0$,
\[
  \varpi^r\bigl(\varpi^{-(r+1)}Q\bigr)=\varpi^{-1}Q\notin T_0.
\]
Thus $T$ is not uniform.  By \Cref{prop:bad-chart}, $A_\alpha$ is not uniform.
\end{proof}


\section{Localisation of the Milnor square}\label{sec:localisation-milnor}

In this section we prove that rational localisation preserves the defining pullback.
For the application to the finite-jet ring we again assume that $k$ is
complete and discretely valued.  We first record the strict Koszul estimate
needed for the proof in the greater generality in which it was formalised.

\subsection{Koszul complexes for rational localisations}

Let $E$ be a complete ultrametric normed commutative ring with
$\lVert1\rVert=1$, and let $t\in E^\times$ satisfy
\[
  0<\lVert t\rVert<1,
  \qquad
  \lVert tx\rVert=\lVert t\rVert\lVert x\rVert
  \quad(x\in E).
\]
Write $E_0=\{x\in E:\lVert x\rVert\leq1\}$ for its norm unit ball.  Assume that $E_0$,
$E\langle T_1,\ldots,T_m\rangle$, and the norm unit ball of this Tate algebra
are noetherian.  Let $f_1,\dots,f_m,g\in E$ generate the unit ideal in $E$.
Put
\[
  T_E=E\langle T_1,\dots,T_m\rangle,
  \qquad
  T_{E,0}=E_0\langle T_1,\dots,T_m\rangle,
\]
and set $r_i=gT_i-f_i$.

We give $T_E$ the topology for which
$\{t^nT_{E,0}\}_{n\geq0}$ is a basis of neighbourhoods of zero.  In the
standard exterior basis, $\bigwedge^qT_E^m$ has the finite product topology,
and each image has the subspace topology.  Thus a differential is strict
precisely when it is open onto its image.

The strict Koszul regularity theorem of
Bambozzi--Kremnizer
\cite[Notation~4.3, Definitions~4.5--4.6, Proposition~4.9,
Lemma~4.11, and Corollary~4.13]{BK} gives the exactness, strictness, and
closed-image assertions below.  We include the direct proof followed in the
formalisation because the two bounds \eqref{eq:ideal-denominators} and
\eqref{eq:syzygy-denominators} are not stated there and are needed below.

\begin{lemma}\label{lem:koszul}
The Koszul complex
\[
  0\longrightarrow \bigwedge^mT_E^m\longrightarrow\cdots
  \longrightarrow\bigwedge^2T_E^m\xrightarrow{d_{2,E}}
  T_E^m\xrightarrow{d_{1,E}}T_E
\]
is exact in positive degrees.  Every differential is continuous and strict onto
its image, and every image is closed.  In particular, if
\[
  I_E=(r_1,\ldots,r_m)=\im(d_{1,E})\subset T_E,
  \qquad
  d_{1,E}(u_1,\ldots,u_m)=\sum_i u_ir_i,
\]
then $I_E$ is closed.  Moreover, there exists
$h_E\in\mathbb Z_{\geq0}$ such that
\begin{equation}\label{eq:ideal-denominators}
  t^{h_E}(I_E\cap T_{E,0})
  \subset d_{1,E}(T_{E,0}^m).
\end{equation}
There also exists $z_E\in\mathbb Z_{\geq0}$ such that
\begin{equation}\label{eq:syzygy-denominators}
  t^{z_E}\bigl(\ker(d_{1,E})\cap T_{E,0}^m\bigr)
  \subset d_{2,E}\bigl(\textstyle\bigwedge^2 T_{E,0}^m\bigr).
\end{equation}
\end{lemma}

\begin{proof}
Over the polynomial ring $E[T_1,\ldots,T_m]$, the sequence
$gT_i-f_i$ has Koszul complex exact in positive degrees.  Indeed, this may be
checked after localising at a prime.  If one of the $gT_i-f_i$ is not in the
prime, it is a unit after localisation and the Koszul complex is contractible.
If all of them lie in the prime, then $g$ does not: otherwise all the $f_i$
would also lie in the prime, contrary to $(g,f_1,\ldots,f_m)=E$.  Thus $g$ is
invertible there and
\[
  gT_i-f_i=g(T_i-f_i/g).
\]
The elements $T_i-f_i/g$ form a regular sequence, since they are monic linear
polynomials in distinct variables.  This proves the assertion over the
polynomial ring.

The map
\[
  E[T_1,\ldots,T_m]\longrightarrow T_E
\]
is flat.  Indeed, $E_0$ is noetherian by assumption, so
$E_0[T_1,\ldots,T_m]$ is noetherian and its $t$-adic completion is flat
over it \cite[Tag~00MB]{Stacks}.  After inverting $t$, the resulting map
$E[T_1,\ldots,T_m]\to T_E$ is flat.  Tensoring the polynomial Koszul complex with $T_E$, and using the
standard base-change identification of its finite free terms, proves
positive-degree exactness.  Notice that this does not assert exactness in
degree zero.

Each differential is continuous because its coordinates are finite sums of
multiplication maps.  The image of $d_{1,E}$ is closed by the noetherian
closed-ideal theorem.  In higher degree, exactness identifies an image with
the kernel of the next continuous differential, and hence that image is
closed.  The nonarchimedean open mapping theorem therefore shows that, for
each differential $d_{q,E}$, there is a constant $C_{q,E}\geq1$ such that
every $y\in\im(d_{q,E})$ has a preimage $x$ satisfying
\[
  d_{q,E}(x)=y,
  \qquad
  \lVert x\rVert\leq C_{q,E}\lVert y\rVert.
\]
This also proves that each differential is strict onto its image.

Choose $h_E\geq0$ such that
$\lVert t\rVert^{h_E}C_{1,E}\leq1$.  If
$x\in I_E\cap T_{E,0}$, choose $u\in T_E^m$ with
\[
  d_{1,E}(u)=x,
  \qquad
  \lVert u\rVert\leq C_{1,E}\lVert x\rVert\leq C_{1,E}.
\]
Then $t^{h_E}u\in T_{E,0}^m$ and
$d_{1,E}(t^{h_E}u)=t^{h_E}x$, which proves
\eqref{eq:ideal-denominators}.  Similarly, choose $z_E\geq0$ such that
$\lVert t\rVert^{z_E}C_{2,E}\leq1$.  If
$u\in\ker(d_{1,E})\cap T_{E,0}^m$, choose $v$ with
$d_{2,E}(v)=u$ and
$\lVert v\rVert\leq C_{2,E}\lVert u\rVert$.  Then
$t^{z_E}v\in\bigwedge^2T_{E,0}^m$, proving
\eqref{eq:syzygy-denominators}.
\end{proof}


\subsection{The defining ideals under pullback}

The formal result used here is not specific to the finite-jet rings.  Let
\[
\begin{matrix}
A&\xrightarrow{\phi_C}&C\\
\scriptstyle\phi_B\downarrow&&\downarrow\scriptstyle\psi_C\\
B&\xrightarrow{\psi_B}&D
\end{matrix}
\]
be a cartesian square of complete ultrametric normed commutative rings.  We
assume that $\phi_C$ and $\psi_B$ preserve the norm, that $\phi_B$ and
$\psi_C$ do not increase it, and that
\[
  \lVert a\rVert=\max\{\lVert\phi_B(a)\rVert,
                         \lVert\phi_C(a)\rVert\}.
\]
We also assume that $\psi_C$ has a norm-preserving section as a map of sets,
that $B,C,D$ have norm-scaling topologically nilpotent units as in
\Cref{lem:koszul}.  For the present number of variables, assume that the
three Tate algebras $T_B,T_C,T_D$ and their norm unit balls are noetherian,
and that the norm unit ball of $D$ is noetherian.  These are precisely the
noetherian inputs used in the formalisation; no noetherianity of the norm unit
balls of $B$ and $C$ is required here.  The finite-jet square satisfies
them, with the coefficientwise section described in \cref{sec:the-global-ring}
and with $t=\varpi$ at each vertex.

Fix elements
\[
  \alpha=(f_1,\dots,f_m;g)
\]
in $A$ which generate the unit ideal.  In the Tate setting this is a rational
datum.  Put
\[
  r_i=gT_i-f_i\in T_A,
\]
and use the same notation for its image in $T_B,T_C$, and $T_D$.  For
$E\in\{A,B,C,D\}$ put
\[
  I_E=(r_1,\ldots,r_m)=\im(d_{1,E})\subset T_E.
\]
Write $E_\alpha=T_E/I_E$ for the graph quotient.  When the vertices are Tate
rings, this is the completed rational localisation by \eqref{eq:graph-model}.

The cartesian property and the section of $C\to D$, applied coefficientwise,
give an exact sequence
\begin{equation}\label{eq:tate-ambient}
  0\longrightarrow T_{A,0}\longrightarrow
  T_{B,0}\oplus T_{C,0}\longrightarrow T_{D,0}\longrightarrow 0.
\end{equation}
The map $T_{C,0}\to T_{D,0}$ is surjective, as are the induced maps on
finite free modules and their exterior powers.  Exactness is coefficientwise:
a compatible restricted coefficient pair lifts to $A_0$, and the max-norm
identity ensures that the lifted coefficients still tend to zero.

\begin{lemma}\label{lem:graph-pullback}
The ideal $I_A$ is closed in $T_A$, and the canonical map
\[
  I_A\longrightarrow I_B\times_{I_D}I_C
\]
is an isomorphism.  Give each $I_E$ the subspace topology inherited from
$T_E$, and give $I_B\oplus I_C$ the max norm.  Then the sequence of
topological abelian groups
\begin{equation}\label{eq:ideal-row}
  0\longrightarrow I_A\longrightarrow I_B\oplus I_C
  \longrightarrow I_D\longrightarrow0
\end{equation}
is strict exact.  Here the maps are
\[
  x\longmapsto(x_B,x_C),
  \qquad
  (x_B,x_C)\longmapsto (x_B)_D-(x_C)_D.
\]
\end{lemma}

\begin{proof}
For $E=B,C,D$, let $C_{1,E}$ be as in the proof of
\Cref{lem:koszul}, and let $C_{2,D}$ be the corresponding constant for
$d_{2,D}$.  Take
$(x_B,x_C)\in I_B\times_{I_D}I_C$, and choose
$u_B\in T_B^m$ and $u_C\in T_C^m$ such that
\[
  d_{1,B}(u_B)=x_B,\qquad
  \lVert u_B\rVert\leq C_{1,B}\lVert x_B\rVert,
\]
\[
  d_{1,C}(u_C)=x_C,\qquad
  \lVert u_C\rVert\leq C_{1,C}\lVert x_C\rVert.
\]
In $T_D^m$
the difference
\[
  w=(u_B)_D-(u_C)_D
\]
belongs to $\ker(d_{1,D})$.  Choose
$v_D\in\bigwedge^2T_D^m$ such that
\[
  d_{2,D}(v_D)=w,\qquad
  \lVert v_D\rVert\leq C_{2,D}\lVert w\rVert.
\]
The norm-preserving coefficientwise section $T_D\to T_C$ induces a
norm-preserving section on second exterior powers; use it to obtain
$v_C\in\bigwedge^2T_C^m$ mapping to $v_D$.  Replacing $u_C$ by
\[
  u_C'=u_C+d_{2,C}(v_C)
\]
does not change $d_{1,C}(u_C)$, and the images of $u_B$ and $u_C'$ in
$T_D^m$ now agree.  Exactness of \eqref{eq:tate-ambient}, applied
coefficientwise, gives $u_A\in T_A^m$ mapping to this pair.  Then
$d_{1,A}(u_A)$ maps to $(x_B,x_C)$.

These bounds, continuity of $d_{2,C}$, and the norm-preserving
coefficientwise section give a constant $C$, independent
of $(x_B,x_C)$, for which $x_A=d_{1,A}(u_A)$ satisfies
\[
  \lVert x_A\rVert\leq
  C\max\{\lVert x_B\rVert,\lVert x_C\rVert\}.
\]
The map $T_A\to T_B\oplus T_C$ is injective, so this proves both the
algebraic pullback assertion and the boundedness of its inverse.

It remains to see that $I_A$ is closed.  The ideals $I_B$ and $I_C$ are
closed by \Cref{lem:koszul}.  If $x$ lies in the closure of $I_A$, its images
lie in $I_B$ and $I_C$.  The pullback isomorphism just proved gives
$x_A\in I_A$ with the same two images as $x$.  Injectivity of
$T_A\to T_B\oplus T_C$ gives $x=x_A$, as required.

Finally, for $y\in I_D$ choose $u_D\in T_D^m$ such that
\[
  d_{1,D}(u_D)=y,\qquad
  \lVert u_D\rVert\leq C_{1,D}\lVert y\rVert.
\]
Apply the norm-preserving section $T_D^m\to T_C^m$ and then $d_{1,C}$.
This gives $x_C\in I_C$ mapping to $y$, with $\lVert x_C\rVert$ bounded
by a fixed multiple of $\lVert y\rVert$.  Thus
$I_B\oplus I_C\to I_D$ is a strict surjection.  Its kernel is $I_A$ by
the pullback assertion, and the preceding bound for the inverse
$I_B\times_{I_D}I_C\to I_A$ makes the inclusion on the left strict.
This proves \eqref{eq:ideal-row}.
\end{proof}

\begin{proposition}\label{prop:localized-milnor}
For every unit-ideal datum $\alpha$ as above, the canonical sequence of graph
quotients
\[
  0\longrightarrow A_\alpha\longrightarrow
  B_\alpha\oplus C_\alpha\longrightarrow D_\alpha\longrightarrow 0
\]
is strict exact, and $C_\alpha\to D_\alpha$ is a strict surjection.  Equivalently,
\[
  A_\alpha\cong B_\alpha\times_{D_\alpha}C_\alpha.
\]
\end{proposition}

\begin{proof}
The ideals $I_B,I_C,I_D$ are closed by \Cref{lem:koszul}, and $I_A$ is
closed by \Cref{lem:graph-pullback}.  Thus
\[
  E_\alpha=T_E/I_E
  \qquad(E=A,B,C,D).
\]

We first prove algebraic exactness.  If a representative $p\in T_A$ maps
into both $I_B$ and $I_C$, the pullback assertion in
\Cref{lem:graph-pullback} gives an element of $I_A$ with the same two images.
Injectivity of $T_A\to T_B\oplus T_C$ then shows that $p\in I_A$.  This gives
injectivity on the left.  Conversely, take compatible classes in
$T_B/I_B$ and $T_C/I_C$ and choose representatives $b$ and $c$.  Their
defect in $T_D$ belongs to $I_D$.  Lift this defect to an element of $I_C$
using the strict surjection in \eqref{eq:ideal-row}, and add it to $c$.
The corrected representatives agree in $T_D$, so
\eqref{eq:tate-ambient} lifts them to $T_A$.  This proves
algebraic exactness.

For the topology on the left, let $x\in A_\alpha$ and put
\[
  M=\max\{\lVert x_B\rVert,\lVert x_C\rVert\}.
\]
Choose representatives $b\in T_B$ and $c\in T_C$ whose norms are
arbitrarily close to the quotient norms of $x_B$ and $x_C$.  Their defect
lies in $I_D$.  The norm estimate for $I_C\to I_D$ proved in
\Cref{lem:graph-pullback} gives a constant $C_0$ and a correction
$y\in I_C$ mapping to this defect such that
\[
  \lVert y\rVert\leq C_0\lVert b_D-c_D\rVert.
\]
Thus $b$ and $c+y$ agree in $T_D$ and lift to
$p\in T_A$.  The max-norm identity for the ambient pullback gives, after
letting the error in the representatives tend to zero,
\[
  \lVert x\rVert\leq C M
\]
for a constant $C$ depending only on the datum.  The two quotient maps are
norm-nonincreasing, so this estimate says precisely that
$A_\alpha\to B_\alpha\oplus C_\alpha$ is a topological embedding.

The coefficientwise section $T_D\to T_C$ shows directly that
$C_\alpha\to D_\alpha$ is surjective.  More precisely, choose a
representative in $T_D$ whose norm is arbitrarily close to the quotient norm
of a given class in $D_\alpha$, and apply the norm-preserving section.  Its
class in $C_\alpha$ has no larger norm.  Thus the surjection is open;
together with continuity, this says that it is strict.

\end{proof}

Applying the preceding two results to the finite-jet square gives the strict
localised Milnor rows used below.  For this square, the coefficient maps in
the identifications commute with rational restriction.  The same
abstract result applies after adjoining any finite number of Tate variables.

\section{Milnor descent and strong sheafiness}

The preceding localisation result gives the following general descent
criterion.

\begin{theorem}[Milnor descent]\label{thm:milnor-sheaf-transfer}
Let $R,B,C,D$ be complete nonarchimedean Huber rings in a commutative square
\[
  \begin{matrix}
    R&\longrightarrow&C\\
    \big\downarrow&&\big\downarrow\\
    B&\longrightarrow&D.
  \end{matrix}
\]
Assume that rational data, covers, and compatible families can be transported
around the square, compatibly with restriction and passage to common
refinements.  Suppose also that, for every rational datum on $R$, the equaliser
and topological-embedding conclusions of \Cref{prop:localized-milnor} hold for
the induced data.  If $B,C,D$ are sheafy, then $R$ is sheafy.
\end{theorem}

\begin{proof}
Let $U=\bigcup_iU_i$ be a finite rational cover.  A compatible family glues over
$B$ and $C$.  The two resulting sections have the same image over $D$, so the
equaliser property gives a unique section over $R$.  The topological-embedding
property, together with the corresponding property for $B$ and $C$, gives the
topological sheaf condition.  The rational-basis theorem now gives the sheaf
condition on all opens \cite[Tag~009O]{Stacks}.
\end{proof}

\begin{corollary}\label{thm:sheafy}
For every $s\geq0$ and every ring of integral elements
\[
  A_s^+\subseteq A\langle V_1,\ldots,V_s\rangle^\circ,
\]
the Huber pair
\[
  \bigl(A\langle V_1,\ldots,V_s\rangle,A_s^+\bigr)
\]
is sheafy.  In particular, $A$ is strongly sheafy.
\end{corollary}

The proof below works over the complete discretely valued base fixed in the
introduction.  More generally, it only assumes that the base is a complete
ultrametric field with a chosen uniformizer and noetherian norm unit ball.

\begin{proof}
The estimates \eqref{eq:structural-map-bounds} make the structural maps
morphisms of Huber pairs.  The rings $B,C,D$ are strongly noetherian affinoid
$k$-algebras and hence sheafy by Huber's theorem
\cite[Theorem~2.2]{Huber94}.  \Cref{prop:localized-milnor}, together
with its compatibility under refinement, supplies the hypotheses of
\Cref{thm:milnor-sheaf-transfer}.  This proves sheafiness for $A$, independently
of the choice of its ring of integral elements.

After adjoining $V_1,\ldots,V_s$, the square retains its coefficientwise
section of $C\to D$, and the strict exact rows of
\Cref{prop:localized-milnor} remain strict exact for every unit-ideal datum,
while $B$, $C$ and $D$ remain strongly noetherian.  Applying the same theorem
proves the assertion for every $s$ and every $A_s^+$.
\end{proof}

\begin{proof}[Proof of \Cref{thm:main}]
\Cref{prop:uniform-domain} proves that $A$ is complete, uniform,
non-noetherian, and a domain.  Strong sheafiness is \Cref{thm:sheafy}, and
failure of stable uniformity is \Cref{prop:not-stably-uniform}.
\end{proof}


\section{Problems 24 and 28}\label{sec:problems-24-28}

Problem~24 of the \emph{Nonarchimedean Scottish Book} asks whether the map of
rings underlying a rational localisation of Tate Huber pairs must be flat.
Problem~28 asks whether a non-zero-divisor which generates a closed ideal can
restrict to zero on a nonempty rational subspace \cite[Problems~24 and 28]{Scottish}.
The same rational datum, together with multiplicativity of the Gauss norm,
answers both questions.  We keep the notation of the introduction.  In fact,
the argument only uses that $k$ is complete and ultrametric and that
$0<|\varpi|<1$; neither conclusion uses sheafiness.  For Problem~28 this
answers the Tate-ring case; we do not address the separate perfectoid case.

\begin{proposition}\label{prop:problems-24-28}
Let $k$ be any complete ultrametric normed field, choose
$\varpi\in k^\times$ with $0<|\varpi|<1$, and form $A$ as above.  Let
\[
  U=\{x\in\Spa(A,A^\circ):|W(x)|\leq|\varpi(x)|\}.
\]
Then $U$ is nonempty, the rational localisation
\[
  A\longrightarrow \mathcal O(U)
    =A\left\langle\frac{W}{\varpi}\right\rangle
\]
is not flat, and multiplication by $Q^2$ is a strict embedding with closed
image even though $Q^2$ maps to zero in $\mathcal O(U)$.
\end{proposition}

\begin{proof}
The composite
\[
  A\longrightarrow B=k\langle W,Q\rangle/(Q^2)
    \longrightarrow k,
  \qquad
  f_0(W)+Qf_1(W)+Q^2h\longmapsto f_0(0),
\]
is norm-nonincreasing.  It therefore sends $A^\circ$ into $k^\circ$, and
pulling back the norm valuation on $k$ gives a continuous valuation belonging
to $\Spa(A,A^\circ)$.  At this point $W$ has value zero and $\varpi$ has
nonzero value, so the point lies in $U$.

Since the restricted Gauss norm on $A$ is multiplicative and
$\lVert Q\rVert=1$, for every $a\in A$ we have
\[
  \lVert Q^2a\rVert=\lVert a\rVert.
\]
Thus multiplication by $Q^2$ is an isometry.  Its map onto its image, with the
subspace topology, is consequently a homeomorphism, so the inclusion is
strict.  Moreover, an isometric image of the complete space $A$ is closed in
$A$.  Since $\lVert Q^2\rVert=1$, the element $Q^2$ is nonzero; multiplication
by it is therefore injective because $A$ is a domain.

On the other hand, the calculation \eqref{eq:q2-killed-on-chart} says directly
that the canonical map to the completed rational localisation kills $Q^2$.
The isomorphism of \Cref{prop:bad-chart} identifies this localisation with the
nonzero ring
\[
  A\longrightarrow k\langle X,Q\rangle/(Q^2),
  \qquad W\longmapsto\varpi X,\quad Q\longmapsto Q.
\]
If the canonical map were flat, the non-zero-divisor $Q^2$ would still act
injectively on $\mathcal O(U)$; equivalently, tensoring the injection
\[
  0\longrightarrow A\xrightarrow{\,\cdot Q^2\,}A
\]
with $\mathcal O(U)$ would make multiplication by the image of $Q^2$
injective.  Its image is zero, however, so this multiplication map is zero on
the nonzero ring $\mathcal O(U)$, a contradiction.
\end{proof}

\section{A second example}\label{sec:second-example}

In the finite-jet construction, the bad rational localisation is non-reduced.
In our second example it is an integral domain; the loss of uniformity is
instead caused by an unbounded family of non-nilpotent power-bounded elements.

The formal statements in this section use the following base hypotheses:
$k$ is a complete nontrivially normed ultrametric field, its norm unit ball is
noetherian, and $\varpi$ is a chosen uniformizer.

\begin{theorem}\label{thm:second-example}
Let $w:\mathbb N_{>0}\to\mathbb N$ satisfy $w(n)\geq1$ for every $n$ and
be unbounded.  The complete Tate $k$-algebra $\mathcal A_w$ defined below has
the following properties.
\begin{enumerate}
\item $\mathcal A_w$ is a uniform, non-noetherian integral domain and
      $\mathcal A_w^\circ=\mathcal A_{w,0}$, where $\mathcal A_{w,0}$ is defined below.
\item The ring $\mathcal A_w$ is strongly sheafy; in particular, the Huber pair
      $(\mathcal A_w,\mathcal A_w^\circ)$ is sheafy.
\item The rational localisation
      \[
        \mathcal B_w=\mathcal A_w\left\langle\frac{W}{\varpi}\right\rangle
      \]
      is an integral domain but is not uniform.
\end{enumerate}
Consequently $\mathcal A_w$ is not stably uniform.  In particular, failure of
stable uniformity need not be caused by a nilpotent in the bad rational
localisation.
\end{theorem}

Taking $w(n)=n$ gives the example announced in the introduction.  We prove
the component statements below for the weakest hypotheses on $w$ that they
require.

\subsection{The weighted-parity algebra}

We write $\mathbb N=\{0,1,2,\ldots\}$, put $I=\mathbb N_{>0}$, and fix an
arbitrary function $w:I\to\mathbb N$.  For a finite-support multi-index
$\nu=(\nu_n)_{n\in I}\in\mathbb N^{(I)}$, put
\begin{equation}\label{eq:parity-weight}
  \omega_w(\nu)=\sum_{\substack{n\geq1\\ \nu_n\text{ odd}}} w(n).
\end{equation}
To lighten the notation, write $\omega=\omega_w$ for the rest of the section.
Consider the submonoid
\begin{equation}\label{eq:parity-monoid}
  S=\left\{(a,\nu)\in\mathbb N\times\mathbb N^{(I)}:
       a\geq\omega(\nu)\right\}.
\end{equation}
The inequality
\begin{equation}\label{eq:omega-subadditive}
  \omega(\nu+\mu)\leq\omega(\nu)+\omega(\mu)
\end{equation}
shows that $S$ is closed under addition.  It is locally finite: a fixed element of $S$ has
only finitely many decompositions as a sum of two elements of $S$.

Let $k[S]$ be the monoid algebra with basis $W^aU^\nu$, where
$U^\nu=\prod_nU_n^{\nu_n}$.  Give it the Gauss norm
\begin{equation}\label{eq:parity-gauss-norm}
  \left\lVert\sum_{(a,\nu)\in S}c_{a,\nu}W^aU^\nu\right\rVert_G
  =\sup_{a,\nu}|c_{a,\nu}|.
\end{equation}
Its completion is denoted by $\mathcal A_w$, or simply $\mathcal A$ when
$w$ is understood:
\begin{equation}\label{eq:parity-algebra}
  \mathcal A_w=
  \left\{
    \sum_{(a,\nu)\in S}c_{a,\nu}W^aU^\nu:
    c_{a,\nu}\in k,\quad c_{a,\nu}\longrightarrow0
  \right\},
\end{equation}
where convergence to zero is over the discrete index set $S$.  Local finiteness makes the
coefficientwise convolution finite, and the submultiplicativity of the Gauss norm on $k[S]$
extends multiplication continuously to $\mathcal A$.  Put
\[
  \mathcal A_{w,0}=
  \left\{
    \sum_{(a,\nu)\in S}c_{a,\nu}W^aU^\nu\in\mathcal A_w:
    c_{a,\nu}\in k^\circ
  \right\}.
\]
We henceforth abbreviate these rings to $\mathcal A$ and $\mathcal A_0$.
Then $\mathcal A_0$ is the closed unit ball for \eqref{eq:parity-gauss-norm}, it is
$\varpi$-adically complete, and
$\mathcal A=\mathcal A_0[1/\varpi]$.

Put
\[
  Y_n=W^{w(n)}U_n,\qquad Z_n=U_n^2,
\]
and, for $N\in\mathbb N$, let $\mathcal A^{(N)}\subset\mathcal A$ be the
closed subring supported on monomials involving only
$W,U_1,\ldots,U_N$.  Thus
$\mathcal A^{(0)}=k\langle W\rangle$.  Let
$\mathcal T^{(N)}\subset\mathcal A^{(N)}$ be the subring in which every
$U_n$ has even exponent.

\begin{lemma}[Finite-variable subrings]\label{lem:finite-variable-subrings}
For every weight $w$ and every $N\in\mathbb N$, substitution
$Z_n\mapsto U_n^2$ gives a
norm-preserving ring isomorphism
\[
  k\langle W,Z_1,\ldots,Z_N\rangle
  \xrightarrow{\ \sim\ }\mathcal T^{(N)}.
\]
For $N=0$ this is the evident identification of both sides with
$k\langle W\rangle$.
Every $f\in\mathcal A^{(N)}$ can be written
\begin{equation}\label{eq:finite-variable-decomposition}
  f=\sum_{\epsilon\in\{0,1\}^N} f_\epsilon Y^\epsilon,
  \qquad f_\epsilon\in\mathcal T^{(N)},
  \qquad Y^\epsilon=\prod_{n=1}^NY_n^{\epsilon_n}.
\end{equation}
Consequently $\mathcal A^{(N)}$ is finite over $\mathcal T^{(N)}$ and is
a strongly noetherian Tate ring.  The inclusions
$\mathcal A^{(N)}\to\mathcal A^{(M)}\to\mathcal A$ for $N\leq M$
preserve the norm.  Moreover, for every $f\in\mathcal A$ and $\ell\geq0$
there are $N$ and $f_N\in\mathcal A^{(N)}$ such that
\[
  \lVert f-f_N\rVert_G\leq |\varpi|^\ell\lVert f\rVert_G.
\]
In particular,
\begin{equation}\label{eq:A-completion-finite-variables}
  \mathcal A=\widehat{\bigcup_{N\geq0}\mathcal A^{(N)}}.
\end{equation}
\end{lemma}

\begin{proof}
On even exponents, halving the $U_n$-coordinates identifies the support
monoid with that of the Tate algebra
$k\langle W,Z_1,\ldots,Z_N\rangle$; the coefficient map and its inverse
preserve the Gauss norm.  Write each exponent uniquely as
$\nu_n=2q_n+\epsilon_n$, with $\epsilon_n\in\{0,1\}$.  Since
$\omega(\nu)=\sum_{\epsilon_n=1}w(n)$, every allowed monomial factors as
\[
  W^aU^\nu
  =W^{a-\omega(\nu)}
   \prod_{n=1}^NZ_n^{q_n}
   \prod_{n=1}^NY_n^{\epsilon_n}.
\]
Grouping the monomials with the same tuple
$(\epsilon_1,\ldots,\epsilon_N)$ gives
\eqref{eq:finite-variable-decomposition}.  The finitely many
$Y^\epsilon$ therefore generate $\mathcal A^{(N)}$ over
$\mathcal T^{(N)}$.
The same argument after adjoining any finite number of Tate variables gives
strong noetherianity.  The inclusions are coefficientwise and hence
isometric.  Finally, approximate $f$ to the required precision by a finite
sum of monomials and choose $N$ so that only
$U_1,\ldots,U_N$ occur in that sum.  This gives the stated estimate and
\eqref{eq:A-completion-finite-variables}.
\end{proof}

\begin{proposition}\label{prop:parity-uniform-domain}
For every weight $w$, the ring $\mathcal A_w$ is a complete uniform Tate
$k$-algebra and an integral domain, with
\[
  \mathcal A_w^\circ=\mathcal A_{w,0}.
\]
\end{proposition}

\begin{proof}
Let $f$ and $g$ be nonzero elements of
$k\langle W,U_1,U_2,\ldots\rangle$.  Since their coefficients tend to zero,
each Gauss norm is attained by a coefficient.  After dividing $f$ and $g$ by
coefficients of maximal norm, we may assume that
\[
  \lVert f\rVert_G=\lVert g\rVert_G=1.
\]
Only finitely many coefficients of either series then have norm $1$.
Consequently, reduction modulo the maximal ideal of $k^\circ$ gives nonzero
polynomials
\[
  \overline f,\overline g
  \in \widetilde{k}[W,U_1,U_2,\ldots].
\]
This polynomial ring is an integral domain, so
$\overline f\,\overline g\neq0$.  Reduction commutes with multiplication:
for each monomial, its coefficient in a product is a finite sum.  Hence some
coefficient of $fg$ has norm $1$, and therefore
\[
  \lVert fg\rVert_G\geq1.
\]
The reverse inequality follows from submultiplicativity of the Gauss norm.
Thus $\lVert fg\rVert_G=1$, and rescaling gives
\[
  \lVert fg\rVert_G=\lVert f\rVert_G\lVert g\rVert_G
\]
in general.

The algebra $\mathcal A$ is a closed subring of this restricted Tate algebra,
and its norm is the restriction of the Gauss norm.  Its norm is therefore
multiplicative, and $\mathcal A$ is an integral domain.

If $x\in\mathcal A_0$, then $\lVert x\rVert_G\leq1$, so every power of $x$
also lies in $\mathcal A_0$.  If $x\notin\mathcal A_0$, then
$\lVert x\rVert_G>1$, and multiplicativity gives
\[
  \lVert x^m\rVert_G=\lVert x\rVert_G^m,
\]
which is unbounded.  Hence $\mathcal A^\circ=\mathcal A_0$.  The subring
$\mathcal A_0$ is the norm unit ball and hence bounded, so
$\mathcal A$ is uniform.  Completeness and the Tate property follow from
\eqref{eq:parity-algebra} and the topologically nilpotent unit $\varpi$.
\end{proof}

The multiplicativity argument for the countable restricted Tate algebra has
also been formalised in Lean, using William Coram's restricted-power-series
code \cite{CoramCode}.

\begin{proposition}\label{prop:parity-nonnoetherian}
If $w(n)\geq1$ for every $n\geq1$, then $\mathcal A_w$ is not noetherian.
\end{proposition}

\begin{proof}
Assume that $w(n)\geq1$ for every $n\geq1$.  For $m\geq1$, let
\[
  I_m=(Z_1,\ldots,Z_m)\subset\mathcal A.
\]
We show that $Z_{m+1}\notin I_m$.

Let $e_{m+1}$ denote the multi-index supported at $m+1$, with value $1$
there.  Define
\[
  \psi_m:\mathcal A\longrightarrow k\langle T\rangle
\]
by the formula
\[
  \psi_m\left(\sum_{a,\nu}c_{a,\nu}W^aU^\nu\right)
  =\sum_{q\geq0}c_{0,2q e_{m+1}}T^q.
\]
This is well defined because the retained coefficients still tend to zero.

We claim that $\psi_m$ is multiplicative.  A monomial in $\mathcal A$ which
involves no $W$ and no $U_j$ for $j\neq m+1$ must be of the form
$U_{m+1}^{2q}$.  Indeed, an odd exponent of $U_{m+1}$ would contribute
$w(m+1)\geq1$ to its weight and would therefore require a positive power of
$W$.  Since all exponents are nonnegative, a product can contribute
$U_{m+1}^{2q}$ only when the two monomials are $U_{m+1}^{2q_1}$ and
$U_{m+1}^{2q_2}$, with $q_1+q_2=q$.
It follows that
\[
  \psi_m(fg)=\psi_m(f)\psi_m(g).
\]

For $1\leq j\leq m$, we have $\psi_m(Z_j)=0$, whereas
$\psi_m(Z_{m+1})=T\neq0$.  Thus $\psi_m$ vanishes on $I_m$ but not on
$Z_{m+1}$, so $Z_{m+1}\notin I_m$.  Since $Z_{m+1}\in I_{m+1}$, we obtain a
strictly increasing chain
\[
  I_1\subsetneq I_2\subsetneq I_3\subsetneq\cdots,
\]
and therefore $\mathcal A$ is not noetherian.
\end{proof}

\subsection{Small perturbations of rational data}

\begin{lemma}[Small perturbation lemma]\label{lem:small-perturbation}
Let $(E,E^+)$ be a complete Tate Huber pair and let
$\alpha=(f_1,\ldots,f_m;g)$ be a rational datum in $E$.  There is a
neighbourhood $V$ of zero in $E$ such that, whenever
\[
  g'-g,\ f_1'-f_1,\ldots,f_m'-f_m\in V,
\]
the tuple $\alpha'=(f_1',\ldots,f_m';g')$ is a rational datum and
$\alpha$ and $\alpha'$ define the same rational subset of
$\Spa(E,E^+)$.  Their completed rational localisations are canonically
bicontinuously isomorphic over $E$.
\end{lemma}

\begin{proof}
Apply \cite[Lemma~3.10]{Huber93} after including $g$ among the
numerators; see also \cite[Remark~2.4.7]{KL}.
The assertion about completed rational localisations follows from their
universal property \cite[Proposition~1.3]{Huber94}.
\end{proof}

\subsection{Rational localisations defined over finitely many variables}

Fix $N\in\mathbb N$.  Let
$\mu=(\mu_n)_{n>N}$ be a finitely supported family of nonnegative integers
and put
\[
  e_\mu=W^{\omega(\mu)}U^\mu,
\]
where $\mu$ is extended by zero for $n\leq N$.  Every
$f\in\mathcal A$ has a unique convergent expression
\begin{equation}\label{eq:coefficient-decomposition}
  f=\sum_\mu f_\mu e_\mu,
  \qquad
  f_\mu\in\mathcal A^{(N)},
  \qquad
  \lVert f_\mu\rVert_G\longrightarrow0,
\end{equation}
and
\[
  \lVert f\rVert_G=\sup_\mu\lVert f_\mu\rVert_G.
\]
Multiplication is determined by
\begin{equation}\label{eq:coefficient-multiplication}
  e_\mu e_\lambda
  =W^{\omega(\mu)+\omega(\lambda)-\omega(\mu+\lambda)}
   e_{\mu+\lambda}.
\end{equation}
The map
\[
  \rho_N:\mathcal A\longrightarrow\mathcal A^{(N)},
  \qquad
  \sum_\mu f_\mu e_\mu\longmapsto f_0,
\]
is a norm-nonincreasing ring retraction.

\begin{proposition}[Coefficientwise localisation]\label{prop:coefficientwise-localization}
Let $\alpha$ be a rational datum whose entries lie in
$\mathcal A^{(N)}$, and put
$P=(\mathcal A^{(N)})_\alpha$.  There is a bicontinuous ring isomorphism
\[
  \mathcal A_\alpha
  \xrightarrow{\ \sim\ }
  \left\{
    \sum_\mu p_\mu e_\mu:
    p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0
  \right\}.
\]
The ring on the right has the supremum norm, and its multiplication is
given by \eqref{eq:coefficient-multiplication}, with $W$ replaced by its
image in $P$.  If a rational refinement is also represented by data in
$\mathcal A^{(N)}$ and $P\to P'$ is the corresponding restriction map,
then the induced restriction sends
\[
  \sum_\mu p_\mu e_\mu
  \longmapsto
  \sum_\mu (p_\mu|_{P'})e_\mu.
\]
\end{proposition}

\begin{proof}
Apply the canonical map $\mathcal A^{(N)}\to P$ to every coefficient in
\eqref{eq:coefficient-decomposition}.  This gives a continuous homomorphism
\[
  \Phi_0:\mathcal A\longrightarrow
  \left\{
    \sum_\mu p_\mu e_\mu:
    p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0
  \right\}.
\]
In the target, the image of $g$ is a unit and each $f_i/g$ is
of norm at most $1$, by the defining property of $P$.  Thus $\Phi_0$
extends continuously to $\mathcal A[1/g]$ for the rational-localisation
topology, and then to the completion:
\[
  \Phi:\mathcal A_\alpha\longrightarrow
  \left\{
    \sum_\mu p_\mu e_\mu:
    p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0
  \right\}.
\]

In the other direction, the inclusion
$\mathcal A^{(N)}\to\mathcal A$ gives a continuous homomorphism
$P\to\mathcal A_\alpha$.  Each $e_\mu$ lies in $\mathcal A_0$, and the
canonical map to a rational localisation is bounded.  Hence the family
$(e_\mu)_\mu$ is bounded in $\mathcal A_\alpha$.  Apply the homomorphism to
every coefficient.  If
$\lVert p_\mu\rVert\to0$, the series
\[
  \sum_\mu p_\mu e_\mu
\]
converges in $\mathcal A_\alpha$.  The resulting map $\Psi$ is continuous,
and \eqref{eq:coefficient-multiplication} shows that it is multiplicative.

The composite $\Phi\Psi$ fixes every term $p e_\mu$, and hence every
finite sum of such terms.  These finite sums are dense.  The other composite
fixes the dense image of $\mathcal A[1/g]$.  Continuity therefore gives
$\Phi\Psi=1$ and $\Psi\Phi=1$.  This proves the claimed isomorphism.

If $P\to P'$ comes from a rational refinement, all the maps just used
commute with this restriction map.  On a finite sum, restriction simply
applies $P\to P'$ to each coefficient; continuity gives the stated formula
for every convergent sum.
\end{proof}

\begin{corollary}[Finite-variable presentation]\label{cor:finite-variable-presentation}
For every rational localisation of $\mathcal A_w$, there is $N_0$ such that,
for every $N\geq N_0$, it is bicontinuously isomorphic to a ring of the form
\[
  \left\{
    \sum_\mu p_\mu e_\mu:
    p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0
  \right\},
\]
where $P$ is a rational localisation of the strongly noetherian Tate ring
$\mathcal A^{(N)}$.
\end{corollary}

\begin{proof}
Start with a rational datum
$\alpha=(f_1,\ldots,f_m;g)$ in $\mathcal A$.  Choose a scalar
$t\in k^\times$ with $0<|t|<1$ and small enough that
$tg,tf_1,\ldots,tf_m$ lie in $\mathcal A_0$.  Multiplying the datum by
$t$ does not change the rational subset or its localisation, so we may
assume that $g,f_1,\ldots,f_m$ lie in $\mathcal A_0$.  Choose a
neighbourhood $V$ as in \Cref{lem:small-perturbation}.  By
\eqref{eq:A-completion-finite-variables}, for some $N$ there are
$g',f_1',\ldots,f_m'\in\mathcal A^{(N)}\cap\mathcal A_0$ such that
\[
  g'-g,\ f_1'-f_1,\ldots,f_m'-f_m\in V.
\]
By \Cref{lem:small-perturbation}, the datum
$\alpha'=(f_1',\ldots,f_m';g')$ gives the same rational subset and the same
completed localisation.  It is rational in $\mathcal A$, so applying
$\rho_N$ to a Bezout identity for its entries shows that it is already a
rational datum in $\mathcal A^{(N)}$.  The same datum belongs to every larger
finite-variable ring, and the corresponding retraction shows from the same
Bezout identity that it is rational there.  Now apply
\Cref{prop:coefficientwise-localization} at every stage beyond $N$.
\end{proof}

\subsection{A reduced rational chart which is not uniform}

The ideal $(W,\varpi)$ is open because $\varpi$ is a unit of $\mathcal A$.
Define the complete $k^\circ$-algebra
\begin{equation}\label{eq:weighted-chart-ring}
  \mathcal B_{w,0}=
  \left\{
    \sum_{\substack{\nu\in\mathbb N^{(I)},\ d\geq\omega(\nu)}}
      b_{d,\nu}X^dU^\nu:
    b_{d,\nu}\in\varpi^{\omega(\nu)}k^\circ,
    \quad
    \varpi^{-\omega(\nu)}b_{d,\nu}\longrightarrow0
  \right\},
\end{equation}
with norm
\begin{equation}\label{eq:weighted-chart-norm}
  \left\lVert\sum b_{d,\nu}X^dU^\nu\right\rVert_{\mathcal B}
  =\sup_{d,\nu}|\varpi|^{-\omega(\nu)}|b_{d,\nu}|.
\end{equation}
The subadditivity \eqref{eq:omega-subadditive} shows that $\mathcal B_{w,0}$
is a ring.  Put $\mathcal B_w=\mathcal B_{w,0}[1/\varpi]$, and abbreviate
these rings to $\mathcal B$ and $\mathcal B_0$ when $w$ is understood.

\begin{proposition}\label{prop:weighted-chart-identification}
For every weight $w$, there is a bicontinuous ring isomorphism
\[
  \mathcal A_w\left\langle\frac{W}{\varpi}\right\rangle
  \xrightarrow{\ \sim\ }\mathcal B_w,
  \qquad W\longmapsto\varpi X.
\]
\end{proposition}

\begin{proof}
The datum $(W;\varpi)$ lies in
$\mathcal A^{(0)}=k\langle W\rangle$.  Put
\[
  P=
  \mathcal A^{(0)}\langle T\rangle/
  \overline{(\varpi T-W)}.
\]
Evaluation at $W=\varpi X$ and $T=X$ gives a continuous map
$P\to k\langle X\rangle$.  Conversely, evaluation of
$k\langle X\rangle$ at the image of $T$ gives a continuous map in the other
direction.  The two maps are inverse by polynomial density, and the norm
estimates in the two universal properties show that the isomorphism is
isometric.

Apply \Cref{prop:coefficientwise-localization} with $N=0$.  It describes the
rational chart as the ring of sums
\[
  \sum_\nu p_\nu e_\nu,
  \qquad p_\nu\in P,\qquad \lVert p_\nu\rVert\longrightarrow0.
\]
Under $P\cong k\langle X\rangle$, this is precisely the model
\eqref{eq:weighted-chart-ring}.  Its sup norm is
\eqref{eq:weighted-chart-norm}, because the term indexed by $\nu$ is
multiplied by $\varpi^{\omega(\nu)}$.  The map from
$\mathcal A^{(0)}$ sends $W$ to $\varpi X$.
\end{proof}

\begin{proposition}\label{prop:weighted-chart-domain-nonuniform}
For every weight $w$, the ring $\mathcal B_w$ is an integral domain.  If $w$
is unbounded, then $\mathcal B_w$ is not uniform.
\end{proposition}

\begin{proof}
Put $R=k\langle X\rangle$.  Here
\[
  R[[U_1,U_2,\ldots]]
  =\left\{\sum_{\nu\in\mathbb N^{(I)}}a_\nu U^\nu:a_\nu\in R\right\}
\]
denotes the ring of all coefficient families indexed by finite-support
multi-indices.  Multiplication is convolution.  For a fixed $\nu$ there are
only finitely many decompositions $\nu=\lambda+\mu$, so every coefficient of
a product is a finite sum.  Order $\mathbb N^{(I)}$ by comparing two vectors
at the largest index where they differ.  This is an additive well-order.  If
two series are nonzero, the coefficient at the sum of their least nonzero
exponents is the product of the corresponding coefficients and is nonzero.
Thus $R[[U_1,U_2,\ldots]]$ is a domain.

The coefficient description gives a homomorphism
\[
  \mathcal B\longrightarrow
  R[[U_1,U_2,\ldots]],
  \qquad
  \sum_\nu p_\nu e_\nu\longmapsto
  \sum_\nu(\varpi X)^{\omega(\nu)}p_\nu(X)U^\nu.
\]
It is a homomorphism by \eqref{eq:coefficient-multiplication}.  If its image
is zero, then
\[
  (\varpi X)^{\omega(\nu)}p_\nu(X)=0
\]
for every $\nu$.  Since $k\langle X\rangle$ is a domain, every
$p_\nu$ is zero.  The map is therefore injective, and hence $\mathcal B$ is
a domain.

Assume now that $w$ is unbounded.  Inside $\mathcal A$ write
$Y_n=W^{w(n)}U_n$ and put
\[
  T_n=\varpi^{-w(n)}Y_n=X^{w(n)}U_n\in\mathcal B.
\]
Formula \eqref{eq:weighted-chart-norm} gives
\[
  \lVert T_n\rVert_{\mathcal B}=|\varpi|^{-w(n)},
  \qquad
  \lVert T_n^2\rVert_{\mathcal B}=1.
\]
The even powers of $T_n$ have norm at most $1$, and the odd powers have
norm at most $\lVert T_n\rVert_{\mathcal B}$.  Thus every $T_n$ is
power-bounded.  The family $(T_n)_{n\geq1}$ is not bounded, since its norms
$|\varpi|^{-w(n)}$ are unbounded.  Hence
$\mathcal B^\circ$ is unbounded and $\mathcal B$ is not uniform.
\end{proof}

\subsection{Strong sheafiness}

\begin{theorem}\label{thm:parity-sheafy}
For every weight $w$, every $s\geq0$, and every ring of integral elements
$\mathcal A_{w,s}^+$ of
$\mathcal A_w\langle V_1,\ldots,V_s\rangle$, the Huber pair
\[
  \bigl(\mathcal A_w\langle V_1,\ldots,V_s\rangle,
        \mathcal A_{w,s}^+\bigr)
\]
is sheafy.  In particular, $\mathcal A_w$ is strongly sheafy.  No positivity
or unboundedness hypothesis on $w$ is needed here.
\end{theorem}

\begin{proof}
We first work with a finite rational cover $U=\bigcup_iU_i$.  Choose one
$N$ large enough to approximate the datum for $U$ and the data for all the
$U_i$ in $\mathcal A^{(N)}$.  The standard combined data for every pairwise
intersection $U_i\cap U_j$ then also lie in $\mathcal A^{(N)}$.  The small
perturbation lemma does not change the rational domains, and
\Cref{prop:coefficientwise-localization} gives
compatible identifications
\[
  \mathcal O(U)\cong
  \left\{\sum_\mu p_\mu e_\mu:
    p_\mu\in P,\ \lVert p_\mu\rVert\to0\right\},
\]
\[
  \mathcal O(U_i)\cong
  \left\{\sum_\mu p_{i,\mu}e_\mu:
    p_{i,\mu}\in P_i,\ \lVert p_{i,\mu}\rVert\to0\right\},
\]
with coefficientwise restriction maps.  Here $P$ is a rational localisation
of the strongly noetherian Tate ring $\mathcal A^{(N)}$, and the $P_i$ are
rational localisations corresponding to the $U_i$.  Let $V$ and $V_i$ be
the rational subsets of
\[
  \Spa\bigl(\mathcal A^{(N)},(\mathcal A^{(N)})^\circ\bigr)
\]
defined by the data giving $P$ and $P_i$.  Then $V=\bigcup_iV_i$.  Indeed,
if $v\in V$, the composite $v\circ\rho_N$ is a point of
$\Spa(\mathcal A,\mathcal A^\circ)$, since $\rho_N$ sends power-bounded
elements to power-bounded elements.  For data in $\mathcal A^{(N)}$,
membership in the corresponding rational subset is unchanged by this
pullback because $\rho_N$ is a retraction.  Thus $v\circ\rho_N$ belongs to
$U$, and hence to some $U_i$, which gives $v\in V_i$.  We may therefore
apply sheafiness of the strongly noetherian ring $\mathcal A^{(N)}$ to the
cover $V=\bigcup_iV_i$.

Let $(x_i)_i$ be a compatible family and write
$x_i=\sum_\mu x_{i,\mu}e_\mu$.  Since $\mathcal A^{(N)}$ is sheafy,
the compatible family $(x_{i,\mu})_i$ glues to a unique $q_\mu\in P$ for every
$\mu$.  It remains to check that $\lVert q_\mu\rVert\to0$.  The restrictions
of the $q_\mu$ to every $P_i$ tend to zero because the coefficients of each
$x_i$ do.  The product restriction map
\[
  P\longrightarrow\prod_iP_i
\]
is a topological embedding, so it reflects convergence to zero.  Hence
$q_\mu\to0$, and $\sum_\mu q_\mu e_\mu$ is the required section over $U$.
The same coefficientwise argument proves separation.

The image of the product restriction map for $\mathcal A$ is therefore the
subspace of tuples whose restrictions to every pairwise intersection agree.
This subspace is closed: it is the common zero locus of the continuous
difference maps, and hence is a Banach $k$-space.  The restriction map is a
continuous bijection from the Banach $k$-space $\mathcal O(U)$ to this
closed subspace.  The nonarchimedean open mapping theorem therefore makes it
a homeomorphism.  We have proved the topological sheaf condition on finite
rational covers.  The
general rational-basis theorem upgrades this to the all-open structure
presheaf, and its plus-ring independence gives the same conclusion for every
ring of integral elements.  In particular, $(\mathcal A,\mathcal A^\circ)$
is sheafy.

For $s\geq0$, the Tate extension
$\mathcal A\langle V_1,\ldots,V_s\rangle$ is bicontinuously isomorphic to the
same weighted-parity construction with the first $s$ weights equal to zero
and the remaining weights shifted by $s$.  The argument above applies to
every weight function and is independent of the ring of integral elements,
so this Tate extension is sheafy for every such choice.  Hence $\mathcal A$
is strongly sheafy.
\end{proof}

\begin{proof}[Proof of \Cref{thm:second-example}]
The fact that $\mathcal A$ is a uniform domain is
\Cref{prop:parity-uniform-domain}, and its failure to be noetherian is
\Cref{prop:parity-nonnoetherian}.  Strong sheafiness is
\Cref{thm:parity-sheafy}.  Finally,
\Cref{prop:weighted-chart-identification,prop:weighted-chart-domain-nonuniform} identify the
rational chart $|W|\leq|\varpi|$ as an integral domain which is not uniform.
\end{proof}

\begin{remark}[Admissible blow-ups]\label{rem:second-example-relation}
There is a common formal interpretation of the two bad rational charts.  Let
$R_0$ denote $A_0$ in the finite-jet example and $\mathcal A_0$ in the
weighted-parity example.  The affine chart of the admissible blow-up of
$\operatorname{Spf}(R_0)$ along $(\varpi,W)$ on which the pullback of this
ideal is generated by $\varpi$ has ring
\[
  \widehat{R_0[W/\varpi]}.
\]
Here $R_0[W/\varpi]$ means the subring of $R_0[1/\varpi]$ generated by
$R_0$ and $W/\varpi$, and the hat denotes the $\varpi$-adic completion
defined above.  After inverting $\varpi$, its coordinate ring is the completed
rational localisation $R_0[1/\varpi]\langle W/\varpi\rangle$, corresponding
to $|W|\leq|\varpi|$.  This description applies to our non-noetherian formal
models because they are $\varpi$-adic and their ideal of definition
$(\varpi)$ is principal; see
\cite[Chapter~0, Section~7.1(c), and Chapter~II, Section~1.1(b)]{FK}.

For $R_0=A_0$, the ring $A_0[W/\varpi]$ is a domain, but the calculation in
the proof of \Cref{prop:bad-chart} shows that
\[
  Q^2\in\bigcap_{n\geq1}\varpi^nA_0[W/\varpi].
\]
This intersection is the kernel of the completion map.  Thus $Q^2$ is killed,
while $Q$ survives, so this rational chart is non-reduced.  The map from $A$ to
this completed rational localisation is also not flat by
\Cref{prop:problems-24-28}.  For $R_0=\mathcal A_0$, the completed
chart remains a domain, but its generic fibre is not uniform because the
power-bounded elements $T_n=X^{w(n)}U_n$ form an unbounded family.  Thus the two
examples give different failures on the same kind of affine blow-up chart.

The proof of sheafiness for $\mathcal A$ uses the further fact that a rational
datum can be approximated inside some strongly noetherian
$\mathcal A^{(N)}$, after which localisation and restriction are computed
coefficient by coefficient.  The infinite monomial support and the unbounded
power-bounded elements are in the tradition of the examples of
Buzzard--Verberkmoes and Mihara; the approximation by the rings
$\mathcal A^{(N)}$ is what makes sheafiness accessible here.
\end{remark}

\section{How the examples were found}\label{sec:discovery}

The authors had for some time been interested in finding a counterexample to
Problem~7 of the \emph{Nonarchimedean Scottish Book}.  Our attempts had
centred on the example of
\cite[Section~4.5, Proposition~17]{BV}, which is uniform but not stably
uniform.  We believe that this example is in fact sheafy, but we have not
found a proof.

In January 2026 we began to experiment with AI tools, initially ChatGPT 5.2
Pro.  Buzzard--Verberkmoes reduce exactness for a two-member Laurent cover to
a boundedness condition on the relevant rings of definition
\cite[Lemma~2]{BV}.  For a uniform ring this follows from boundedness of the
power-bounded elements \cite[Lemma~3 and Corollary~4]{BV}.  Their reduction
from general rational covers to Laurent covers is given in
\cite[Lemma~8 and the proof of Theorem~7]{BV}.  For sheafiness these checks
must also be made after rational localisation.  Their Theorem~7 cannot be
applied directly to Proposition~17, since one of the rational localisations
in that example is not uniform.  Our plan was instead to ask ChatGPT to
write down many explicit rational covers and check the required exactness
directly for each one, in the hope that a pattern, and eventually a proof,
would emerge.

After a couple of weeks ChatGPT 5.2 Pro claimed to have a complete proof.
The authors then began the slow process of understanding this proof, only to
discover, with the help of ChatGPT 5.3, that one of its arguments used the
following assertion:

\emph{If $\phi:A\to B$ is a continuous homomorphism of Hausdorff
topological abelian groups and $A$ is complete, then $\phi(A)$ is closed in
$B$.}

This assertion is false, and its use completely broke the purported proof.

Motivated by this, we began in parallel to use Claude Code to formalise the
parts of the theory of adic spaces needed here, including the theorem that
strongly noetherian Tate rings are sheafy.  The aim was a practical one:
future AI-generated proofs could be formalised before the human authors had
spent days understanding an argument containing a fatal error near its end.

We then returned to writing down covers and looking for a pattern.  This
continued through ChatGPT 5.3 and subsequent versions.  When ChatGPT 5.6 Sol
became available, we asked, almost in passing, whether it could prove the
result we wanted or \emph{find a new example}.  It produced the examples
studied here.  By then the Lean development was far enough advanced that we
could use Claude Code to formalise the arguments quickly in Lean and check
that they were correct.

At the time of writing, it is still possible to reproduce this by asking the
agents to \emph{find an example of a uniform and sheafy non-noetherian ring
which is not stably uniform}.  One point to note is that they sometimes reply
that this is an open problem, which prevents them from proceeding.  In such
cases, saying \emph{an example exists; find it} often produces an example.

\appendix
\section{Lean formalisation and verification}\label{sec:formalisation}

This appendix records the Lean definitions and theorem statements.  Theorem
listings stop before their proof terms, and the links open the checked declarations.  The
formalisation is available as a self-contained repository,
\href{https://github.com/CBirkbeck/uniform-sheafy-tate-domains-lean}{\texttt{uniform-sheafy-tate-domains-lean}} \cite{SheafyLean},
which carries the adic-spaces library, both examples and the Comparator
certificates, and has mathlib as its only dependency.  It is extracted from the
development repository AINTLIB \cite{AINTLIB}, whose commits the per-declaration
links below pin; a few of those declarations sit on other public branches there.
It uses
Lean~4.33.0 \cite{Lean4} and mathlib~4.33.0 \cite{mathlib}.  The headline
statements for both examples have been checked with
\href{https://github.com/leanprover/comparator}{Comparator}, which compares
them with independent challenge statements, checks their axiom dependencies,
and replays the proofs through the Lean kernel.  The interactive appendix was
prepared with \href{https://github.com/roed-math/paperforge}{PaperForge}; each
Lean button opens the corresponding declaration.

\subsection{The predicate \texttt{IsSheafy}}

\begin{definition}[The rational-cover predicate]
\label{def:lean-rational-sheafiness}
The arguments in the paper use finite rational covers, and Lean therefore uses
the following predicate.  Here
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.RationalCoveringData.html}{\texttt{RationalCoveringData A}}
consists of a rational domain together with a finite rational cover of it,
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.RationalCoveringData.IsRational.html}{\texttt{C.IsRational}}
imposes the usual open-ideal condition, and
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.presheafValue.html}{\texttt{presheafValue D}}
is the completed rational localisation attached to \(D\).

\begin{lstlisting}
class IsSheafy (A : Type u) [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [inst₁ : PlusSubring A]
    [inst₂ : IsHuberRing A] [T2Space A] [NonarchimedeanRing A]
    [letI : UniformSpace A :=
      IsTopologicalAddGroup.rightUniformSpace A; CompleteSpace A]
    [IsRingOfIntegralElements (A⁺)] : Prop where
  embedding : ∀ (C : RationalCoveringData A), C.IsRational →
    Topology.IsEmbedding (productRestrictionSub A C)
  gluing : ∀ (C : RationalCoveringData A), C.IsRational →
    ∀ (f : ∀ (D : ↥C.covers), presheafValue D.1),
    (∀ (D₁ D₂ : ↥C.covers) (D₃ : RationalLocData A)
      (h₃₁ : rationalOpen D₃.T D₃.s ⊆
        rationalOpen D₁.1.T D₁.1.s)
      (h₃₂ : rationalOpen D₃.T D₃.s ⊆
        rationalOpen D₂.1.T D₂.1.s),
      restrictionMap D₁.1 D₃ h₃₁ (f D₁) =
        restrictionMap D₂.1 D₃ h₃₂ (f D₂)) →
    ∃ x : presheafValue C.base, ∀ (D : ↥C.covers),
      restrictionMap C.base D.1 (C.hsubset D.1 D.2) x = f D
\end{lstlisting}

The first field says that restriction to a finite rational cover is a
topological embedding.  The second says that every compatible family of
sections glues; compatibility is expressed on common rational refinements.
This is the topological sheaf condition on the rational basis.  We use this
form because it speaks directly about the rational localisations occurring in
the paper.
\end{definition}

\subsection{Comparison with Mathlib's sheaf predicate}

\begin{remark}
\label{rem:lean-sheaf-comparison}
\par
For an open subset \(V\subseteq\Spa(A,A^+)\),
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.limitSections.html}{\texttt{limitSections V}}
is the projective limit of the sections on rational subdomains contained in
\(V\), and
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.limitRestrict.html}{\texttt{limitRestrict}}
is the restriction map between these limits.  The predicate
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.IsLimitSheaf.html}{\texttt{IsLimitSheaf}}
is the separation, gluing and topological-embedding condition for arbitrary
open covers.  Lean proves:

\begin{lstlisting}
theorem isSheafy_iff_isLimitSheaf :
    IsSheafy A ↔ IsLimitSheaf A
\end{lstlisting}

For a presheaf \(F\) as above, \texttt{IsSheafOfTopologicalRings} is Wedhorn's
condition that
\[
  U\longmapsto\operatorname{Hom}_{\mathrm{cont}}(T,F(U))
\]
is a sheaf of sets for every topological commutative ring \(T\).  For the
structure presheaf:

\begin{lstlisting}
theorem structurePresheaf_isSheafOfTopologicalRings_iff :
    TopCat.Presheaf.IsSheafOfTopologicalRings
        (structurePresheaf A) ↔
      IsLimitSheaf A
\end{lstlisting}

It also proves the general comparison with Mathlib's categorical predicate:

\begin{lstlisting}
theorem isSheafOfTopologicalRings_iff_forgetToTopCommRingCat_isSheaf :
    F.IsSheafOfTopologicalRings ↔ TopCat.Presheaf.IsSheaf
      (F ⋙ CompleteTopCommRingCat.forgetToTopCommRingCat)
\end{lstlisting}

The forgetful functor retains the topology but forgets completeness and
separatedness.  Its target has all topological commutative rings as objects,
which is precisely the class of test rings in Wedhorn's formulation.  Combining
the preceding equivalences gives the direct comparison used here:

\begin{lstlisting}
theorem isSheafy_iff_structurePresheaf_forgetToTopCommRingCat_isSheaf
    [DecidableEq A] [DecidableEq (RationalLocData A)] [IsTateRing A]
    [IsRingOfIntegralElements (A⁺ : Subring A)] [T2Space A]
    [NonarchimedeanRing A]
    [letI : UniformSpace A :=
      IsTopologicalAddGroup.rightUniformSpace A; CompleteSpace A] :
    IsSheafy A ↔
      TopCat.Presheaf.IsSheaf
        (structurePresheaf A ⋙
          CompleteTopCommRingCat.forgetToTopCommRingCat)
\end{lstlisting}

Thus \texttt{IsSheafy} is equivalent both to Wedhorn's representable
formulation and to Mathlib's sheaf condition for the structure presheaf.  It is
used here because it is convenient, not because it defines a weaker or
stronger notion.

The auxiliary class
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/ValuationSpectrum.HasLocLiftPowerBounded.html}{\texttt{HasLocLiftPowerBounded}}
constructs restriction maps between completed rational localisations.  For an
inclusion of rational domains it says that the old denominator becomes a unit
and that the old numerator fractions are power-bounded on the smaller domain.
It is supplied by the theory for the complete Tate pairs used here and is not
an additional hypothesis in the main results.
\end{remark}

\subsection{Sheafiness for Tate rings}

For a complete Tate ring, the following definitions fix a ring of integral
elements and then quantify over all such choices.  The final definition also
removes the choice of completion for a Tate ring which is not assumed complete.

\begin{lstlisting}
def IsSheafyFor (Aplus : RingOfIntegralElements A) : Prop :=
  letI := Aplus.toPlusSubring
  haveI : IsRingOfIntegralElements (A⁺ : Subring A) := Aplus.2
  haveI : HasLocLiftPowerBounded A :=
    hasLocLiftPowerBounded_faithful
  IsLimitSheaf A

def IsSheafyComplete : Prop :=
  ∀ Aplus : RingOfIntegralElements A, IsSheafyFor A Aplus

def IsSheafyTateRing : Prop :=
  ∀ (P : PairOfDefinition A)
    (Bplus : RingOfIntegralElements (CompletionModel A P)),
    IsSheafyFor (CompletionModel A P) Bplus
\end{lstlisting}

Thus \texttt{IsSheafyFor A Aplus} is sheafiness of \((A,A^+)\),
\texttt{IsSheafyComplete A} requires this for every ring of integral elements,
and \texttt{IsSheafyTateRing A} requires it for every completion model.

Two remarks on what these universal statements exclude, since a universally quantified
claim can hold for the wrong reason.  \texttt{RingOfIntegralElements A} is a subtype, so
\texttt{IsSheafyComplete} would hold vacuously if \(A\) admitted no valid \(A^+\); the
certified statements therefore include, for each ring they quantify over, that its maximal
plus ring \(A^\circ\) is one.  This holds in any Huber ring --- \(A^\circ\) is open
because it contains a ring of definition, and integrally closed by Wedhorn 5.30(4) --- so it
covers the Tate algebras \(A\langle X_1,\ldots,X_n\rangle\) as well as \(A\) itself.
Separately, \texttt{IsStablyUniform} quantifies only over localisation data satisfying
\texttt{D.IsRational}, Wedhorn 7.29's condition that \(T\cdot A\) be open.  The
distinction matters in the direction the paper uses: \texttt{RationalLocData} is raw data,
so dropping the condition would strengthen the class and thereby weaken its negation,
turning the failure of stable uniformity into a claim about data that need not present a
rational subset at all.  The witness here is the genuine rational chart
\(A\langle W/\varpi\rangle\), and its rationality is proved.

\subsection{Strong noetherianity}

\begin{definition}[Strong noetherianity]
\label{def:lean-strong-noetherianity}
Lean defines restricted power series and strong noetherianity as follows.

\newpage\begin{lstlisting}
def MvPowerSeries.IsRestricted {k : ℕ} {A : Type*}
    [CommRing A] [TopologicalSpace A]
    (f : MvPowerSeries (Fin k) A) : Prop :=
  Tendsto
    (fun s : Fin k →₀ ℕ => MvPowerSeries.coeff s f)
    cofinite (nhds 0)

class IsStronglyNoetherian (A : Type*) [CommRing A]
    [TopologicalSpace A] [NonarchimedeanRing A] : Prop where
  isNoetherianRing_restricted : ∀ k : ℕ,
    IsNoetherianRing (restrictedMvPowerSeriesSubring k A)
\end{lstlisting}

The first condition says exactly that the coefficients tend to zero.  Hence
the subring in the second declaration is
\(A\langle T_1,\ldots,T_k\rangle\), and the second declaration says that this
ring is noetherian for every \(k\).  This is the usual notion of strong
noetherianity \cite[Proposition and Definition~6.36]{Wedhorn}.
\end{definition}

For a Tate ring not assumed complete, the condition is imposed on a completion
model.  Lean then records Wedhorn's sheafiness theorem at the same level of
generality:

\begin{lstlisting}
def IsStronglyNoetherianTateRing [IsTateRing A] : Prop :=
  ∃ P : PairOfDefinition A,
    IsStronglyNoetherian (CompletionModel A P)

theorem isSheafyTateRing_of_stronglyNoetherianTateRing
    [IsTateRing A] (h : IsStronglyNoetherianTateRing A) :
    IsSheafyTateRing A

theorem isSheafyComplete_of_stronglyNoetherianTate
    [IsStronglyNoetherian A] :
    IsSheafyComplete A
\end{lstlisting}

The first theorem is independent of the chosen completion model; the second is
its complete-ring specialisation.  These are the formal versions of the
strongly noetherian sheaf theorem \cite[Theorem~8.28(b)]{Wedhorn}.

\subsection{The finite-jet example}

\begin{definition}[The finite-jet ring]
\label{def:lean-finite-jet-ring}
The four rings in the defining square and the finite-jet ring itself are
represented as follows.

\begin{lstlisting}
abbrev L : Type u := RestrictedLaurent K

abbrev JetC : Type u := PowerSeries.Restricted (L K) (1 : ℝ)

abbrev JetB : Type u := DualNumber (PowerSeries.Restricted K (1 : ℝ))

abbrev JetD : Type u := DualNumber (L K)

noncomputable def jetSupport : Subring (JetC K) where
  carrier := {f |
    qCoeff K 0 f ∈ nonnegSubring K ∧
    qCoeff K 1 f ∈ nonnegSubring K}
  ...

abbrev JetA : Type u := ↥(jetSupport K)
\end{lstlisting}

Here \texttt{RestrictedLaurent K} is
\(K\langle W,W^{-1}\rangle\), while
\texttt{PowerSeries.Restricted R 1} is the radius-one restricted power-series
ring over \(R\).  The condition defining \texttt{jetSupport} says that the
coefficients of \(Q^0\) and \(Q^1\) have no negative powers of \(W\).  Thus
\texttt{JetA K} is precisely
\[
  \left\{
    f_0(W)+Qf_1(W)+Q^2h(W,W^{-1},Q):
    f_0,f_1\in K\langle W\rangle,\;
    h\in K\langle W,W^{-1}\rangle\langle Q\rangle
  \right\}.
\]
This is the coefficient description of \(A\) in
\eqref{eq:coefficient-A0} after inverting \(\varpi\).
\end{definition}

For a complete nontrivially normed ultrametric field \(K\), a uniformizer
\(\varpi\), and, where stated, a noetherian norm unit ball, the following are
the formal counterparts of
\Cref{prop:uniform-domain,prop:bad-chart,prop:not-stably-uniform}:

\begin{lstlisting}
theorem finiteJet_isUniform (ϖ : Uniformizer K) :
    TopologicalRing.IsUniform (JetA K)

theorem finiteJet_isDomain :
    IsDomain (JetA K)

theorem finiteJet_not_noetherian :
    ¬ IsNoetherianRing (JetA K)

def chartEquiv (ϖ : Uniformizer K) :
    presheafValue (chartDatum K ϖ) ≃+* JetB K := ...

theorem chartEquiv_continuous (ϖ : Uniformizer K) :
    Continuous (chartEquiv K ϖ)

theorem chartEquiv_symm_continuous (ϖ : Uniformizer K) :
    Continuous (chartEquiv K ϖ).symm

theorem finiteJet_not_stablyUniform (ϖ : Uniformizer K) :
    ¬ TopologicalRing.IsStablyUniform (JetA K)
\end{lstlisting}

The equivalence and the two continuity statements identify the completed
rational localisation with
\[
  A\left\langle\frac{W}{\varpi}\right\rangle
    \simeq K\langle X,Q\rangle/(Q^2)
\]
as a topological ring.  The domain and non-noetherianity statements do not
require a uniformizer.

Ordinary sheafiness, independently of the choice of ring of integral
elements, is recorded by

\begin{lstlisting}
theorem finiteJet_isSheafyComplete
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    IsSheafyComplete (JetA K)
\end{lstlisting}

The formal statement of strong sheafiness is:

\begin{lstlisting}
theorem finiteJet_tateExt_isSheafyComplete
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K))
    (n : ℕ) :
    letI := mvTateAlgebraTopology' (A := JetA K) n
    haveI := mvTate_isTateRing (A := JetA K) n
    haveI := mvTate_t2Space (A := JetA K) n
    haveI := mvTate_nonarchimedean (A := JetA K) n
    haveI := mvTateAlgebraTopology'_isTopologicalRing
      (A := JetA K) n
    haveI : @CompleteSpace
      ↥(restrictedMvPowerSeriesSubring n (JetA K))
      (IsTopologicalAddGroup.rightUniformSpace _) :=
        finiteJet_tateExt_completeSpace K n
    IsSheafyComplete
      ↥(restrictedMvPowerSeriesSubring n (JetA K))
\end{lstlisting}

The restricted power-series subring here is
\(A\langle V_1,\ldots,V_n\rangle\), with its canonical Tate-algebra topology,
and \texttt{IsSheafyComplete} says that it is sheafy for every ring of integral
elements.  This is precisely the strong-sheafiness assertion of
\Cref{thm:sheafy}.  The separate
\texttt{\_of\_dvr} theorem supplies \(\varpi\) and the noetherianity hypothesis
from the assumption that \(\mathcal O[K]\) is a discrete valuation ring.

\subsubsection{The Scottish Book statements}

For \Cref{prop:problems-24-28}, the base need only be a complete ultrametric
normed field with a chosen nonzero element \(\varpi\) satisfying
\(\lVert\varpi\rVert<1\); Lean packages this as \texttt{IsFJPBase}.  The element
\texttt{scottishWitness K} is \(Q^2\).

\begin{lstlisting}
class IsFJPBase (K : Type u) [NormedField K]
    [IsUltrametricDist K] [CompleteSpace K] where
  pseudoUniformizer : K
  pseudoUniformizer_ne_zero : pseudoUniformizer ≠ 0
  norm_pseudoUniformizer_lt_one :
    ‖pseudoUniformizer‖ < 1

theorem finiteJet_problem28 :
    (chartDatum K).IsRational ∧
    (rationalOpen
      (chartDatum K).T (chartDatum K).s).Nonempty ∧
    Nontrivial (presheafValue (chartDatum K)) ∧
    Function.Injective
      (fun a : JetA K => scottishWitness K * a) ∧
    Continuous
      (fun a : JetA K => scottishWitness K * a) ∧
    IsStrictMap
      (fun a : JetA K => scottishWitness K * a) ∧
    IsClosed
      (Set.range
        (fun a : JetA K => scottishWitness K * a)) ∧
    (chartDatum K).canonicalMap
      (scottishWitness K) = 0

theorem finiteJet_not_flat_canonicalMap :
    ¬ @Module.Flat
      (JetA K)
      (presheafValue (chartDatum K))
      _ _
      (RingHom.toModule (chartDatum K).canonicalMap)
\end{lstlisting}

The first theorem says that multiplication by the non-zero-divisor \(Q^2\) is
a continuous strict injection with closed image, while \(Q^2\) becomes zero on
a nonempty rational subspace with nonzero section ring.  The second says that
the canonical map to this completed rational localisation is not flat.

\subsubsection{Koszul complexes and Milnor descent}

The statement formalised for \Cref{lem:koszul} is more general than its use in
the finite-jet example.  Let \(E\) be the complete ultrametric normed
commutative ring appearing in the theorem below and put
\(P(E,m)=E\langle T_1,\ldots,T_m\rangle\).  The graph sequence is
\(r_i=gT_i-f_i\).

\begin{lstlisting}
theorem koszulGraph_exact_strict_closed
    [IsNoetherianRing (P E m)]
    (hE₀ : IsNoetherianRing (unitBall E))
    (t : E) (htu : IsUnit t)
    (ht1 : ‖t‖ < 1) (ht0 : 0 < ‖t‖)
    (hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖)
    (hE₀P : IsNoetherianRing (unitBall (P E m)))
    (g : E) (f : Fin m → E)
    (hunit : Ideal.span ({g} ∪ Set.range f) = ⊤)
    (r : Fin m → P E m)
    (hr : ∀ i, r i =
      polyToP
        (MvPolynomial.C g * MvPolynomial.X i -
          MvPolynomial.C (f i))) :
    (∀ q, Function.Exact
      (koszulDifferential r (q + 1))
      (koszulDifferential r q)) ∧
    (∀ q, IsStrictLinearMap
      (koszulDifferential r q)) ∧
    (∀ q, IsClosed
      (Set.range (koszulDifferential r q)))
\end{lstlisting}

This is exactly the positive-degree exactness, strictness and closed-image
part of \Cref{lem:koszul}.  The
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/FiniteJet.GraphKoszul.pow_smul_graphIdeal_inter_unitBall_subset.html}{ideal-denominator declaration}
and
\href{https://cbirkbeck.github.io/uniform-sheafy-tate-domains/lean/AdicSpaces/declarations/FiniteJet.GraphKoszul.pow_smul_ker_d1_inter_subset.html}{syzygy-denominator declaration}
state respectively the two denominator inclusions
\eqref{eq:ideal-denominators} and \eqref{eq:syzygy-denominators}.
The declarations attached to
\Cref{lem:graph-pullback,prop:localized-milnor}
state the corresponding ideal pullback, exactness and topological-embedding
results for the general corner square used there.

Finally, \texttt{MilnorSquareData} packages exactly the transport of rational
data, covers and compatible families, together with the local equaliser and
topological-embedding conditions of \Cref{thm:milnor-sheaf-transfer}.  The
abstract theorem is:

\begin{lstlisting}
theorem isSheafy_of_milnorSquare
    [DecidableEq (RationalLocData B)]
    [DecidableEq (RationalLocData C)]
    [DecidableEq (RationalLocData D)]
    (phiB : R →+* B) (phiC : R →+* C)
    (phiD : R →+* D)
    (hphiB : Continuous phiB)
    (hphiC : Continuous phiC)
    (hphiD : Continuous phiD)
    (sq : MilnorSquareData
      phiB phiC phiD hphiB hphiC hphiD)
    (hB : IsSheafy B)
    (hC : IsSheafy C)
    (hD : IsSheafy D) :
    IsSheafy R
\end{lstlisting}

The finite-jet square supplies this data, so the theorem specialises to the
sheafiness statement used in the paper.  No claim is made that an arbitrary
strict Milnor square is sufficient.

\subsection{The weighted-parity example}

Let \(K\) be a complete nontrivially normed ultrametric field and let
\(w:\mathbb N\to\mathbb N\).  Lean indexes the variables by \(\mathbb N\):
index \(0\) represents \(W\), and index \(n\geq1\) represents \(U_n\).  The
ambient restricted Tate algebra and the support condition defining
\(\mathcal A_w\) are:

\begin{lstlisting}
abbrev Amb : Type _ :=
  MvPowerSeries.Restricted K (fun _ : ℕ => (1 : ℝ))

def wpWeight (w : ℕ → ℕ) (t : ℕ →₀ ℕ) : ℕ :=
  ∑ n ∈ t.support,
    if (t n).mod 2 = 1 ∧ n ≠ 0 then w n else 0

def WPMem (w : ℕ → ℕ) (t : ℕ →₀ ℕ) : Prop :=
  wpWeight w t ≤ t 0

noncomputable def wpSupport : Subring (Amb K) where
  carrier := {f | ∀ t : ℕ →₀ ℕ, ¬ WPMem w t →
    MvPowerSeries.coeff t f.1 = 0}
  ...

abbrev WPA : Type _ := ↥(wpSupport K w)
\end{lstlisting}

For an exponent \(t\), \texttt{t 0} is the exponent of \(W\), while
\texttt{wpWeight w t} is
\[
  \sum_{\substack{n\geq1\\t(n)\ {\rm odd}}}w(n).
\]
Thus \texttt{WPMem w t} is precisely the condition
\(a\geq\omega_w(\nu)\) in \eqref{eq:parity-monoid}, and
\texttt{wpSupport} says that all coefficients outside this monoid vanish.
Consequently \texttt{WPA K w} is exactly the ring \(\mathcal A_w\) of
\eqref{eq:parity-algebra}.

The formal counterparts of
\Cref{prop:parity-uniform-domain,prop:parity-nonnoetherian} are:

\begin{lstlisting}
theorem norm_wpa_mul (a b : WPA K w) :
    ‖a * b‖ = ‖a‖ * ‖b‖

instance : IsDomain (WPA K w)

theorem powerBoundedSubring_eq_unitBall
    (ϖ : Uniformizer K) :
    powerBoundedSubring (WPA K w) =
      (FiniteJet.unitBall (WPA K w) : Set (WPA K w))

theorem isUniform_WPA (ϖ : Uniformizer K) :
    IsUniform (WPA K w)

theorem not_isNoetherianRing_WPA
    (hw : ∀ n, 1 ≤ n → 1 ≤ w n) :
    ¬ IsNoetherianRing (WPA K w)
\end{lstlisting}

The equality with \texttt{FiniteJet.unitBall} says exactly that
\(\mathcal A_w^\circ=\mathcal A_{w,0}\), and \texttt{hw} is the condition
\(w(n)\geq1\) for \(n\geq1\).

Strong sheafiness, including ordinary sheafiness when (s=0), is stated
directly for the finite Tate extensions:

\begin{lstlisting}
theorem wp_tateExt_isSheafyComplete
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K))
    (s : ℕ) :
    letI := mvTateAlgebraTopology' (A := WPA K w) s
    haveI := mvTate_isTateRing (A := WPA K w) s
    haveI := mvTate_t2Space (A := WPA K w) s
    haveI := mvTate_nonarchimedean (A := WPA K w) s
    haveI := mvTateAlgebraTopology'_isTopologicalRing
      (A := WPA K w) s
    haveI : @CompleteSpace
      ↥(restrictedMvPowerSeriesSubring s (WPA K w))
      (IsTopologicalAddGroup.rightUniformSpace _) :=
        wp_tateExt_completeSpace (w := w) s
    IsSheafyComplete
      ↥(restrictedMvPowerSeriesSubring s (WPA K w))
\end{lstlisting}

Here the restricted power-series subring is
\(\mathcal A_w\langle V_1,\ldots,V_s\rangle\).  Hence this theorem is precisely
the strong-sheafiness assertion of \Cref{thm:parity-sheafy}; it holds for every
\(w\), without a positivity or unboundedness assumption.

Finally, \texttt{chartDatum} is the rational datum \((W;\varpi)\).  The
statements corresponding to
\Cref{prop:weighted-chart-identification,prop:weighted-chart-domain-nonuniform}
are:

\begin{lstlisting}
theorem chartDatum_isRational (ϖ : Uniformizer K) :
    (chartDatum (w := w) ϖ).IsRational

theorem isDomain_chart
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    IsDomain (presheafValue
      (chartDatum (w := w) ϖ))

theorem not_isUniform_chart
    (hwu : ∀ M, ∃ n, 1 ≤ n ∧ M ≤ w n)
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    ¬ IsUniform (presheafValue
      (chartDatum (w := w) ϖ))

theorem not_isStablyUniform_WPA
    (hwu : ∀ M, ∃ n, 1 ≤ n ∧ M ≤ w n)
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    ¬ IsStablyUniform (WPA K w)
\end{lstlisting}

The condition \texttt{hwu} says exactly that \(w\) is unbounded.  Thus every
positive unbounded weight gives all the assertions of
\Cref{thm:second-example}; the paper takes \(w(n)=n\).

\subsection{Mathematical and code provenance}

The definitions of rational localisation, the structure presheaf and the sheaf
condition follow Huber \cite{Huber94} and Wedhorn \cite{Wedhorn}.  The
independence of the choice of ring of integral elements uses the standard
rational-refinement formalism described by Kedlaya
\cite[Lemma~1.6.8 and Remark~1.6.9]{KedlayaAWS}.

The restricted-power-series implementation includes code adapted from William
Coram's development \cite{CoramCode}.  Its univariate Gauss-norm layer uses
Fabrizio Barroero's mathlib code \cite{BarroeroCode}, while the multivariable
power-series equivalences use code of Bingyu Xia \cite{XiaCode}.  These are
separate sources, and their attribution is retained in the corresponding
source-file headers.
\begin{thebibliography}{99}

\bibitem{AINTLIB}
C.~Birkbeck and contributors,
\emph{AINTLIB: AdicSpaces formalisation},
Lean~4 source code, Scottish Book snapshot
\href{https://github.com/CBirkbeck/AINTLIB/commit/01116aca6070283726008536cba16d165a01b505}{\texttt{01116aca6}},
2026, \href{https://github.com/CBirkbeck/AINTLIB}{GitHub repository}.

\bibitem{SheafyLean}
C.~Birkbeck and A.~Torzewski,
\emph{Uniform sheafy Tate rings that are not stably uniform: the Lean
formalisation},
Lean~4 source code, snapshot
\href{https://github.com/CBirkbeck/uniform-sheafy-tate-domains-lean/commit/e3514f12e382a8ef8f0d2b8822ed9b792bcaf838}{\texttt{e3514f12e}},
2026, \href{https://github.com/CBirkbeck/uniform-sheafy-tate-domains-lean}{GitHub repository}.

\bibitem{BBK}
O.~Ben-Bassat and K.~Kremnizer,
\emph{Non-Archimedean analytic geometry as relative algebraic geometry},
Ann. Fac. Sci. Toulouse Math. (6) \textbf{26} (2017), no.~1, 49--126,
\href{https://doi.org/10.5802/afst.1526}{DOI}.

\bibitem{BK}
F.~Bambozzi and K.~Kremnizer,
\emph{On the sheafyness property of spectra of Banach rings},
J. Lond. Math. Soc. (2) \textbf{109} (2024), no.~1, e12855,
\href{https://doi.org/10.1112/jlms.12855}{DOI}.

\bibitem{BV}
K.~Buzzard and A.~Verberkmoes,
\emph{Stably uniform affinoids are sheafy},
J. Reine Angew. Math. \textbf{740} (2018), 25--39.

\bibitem{BarroeroCode}
F.~Barroero,
Lean source code,
\href{https://github.com/leanprover-community/mathlib4/blob/fd1d54bcac5caba4eff2ea3421c47d907333f515/Mathlib/RingTheory/PowerSeries/GaussNorm.lean}{mathlib source file}.

\bibitem{CoramCode}
W.~Coram,
Lean source code,
\href{https://github.com/WilliamCoram/PhD/tree/e8fcf8fbff848a95475ab62ae2568cbb73961de8}{GitHub repository}.

\bibitem{FK}
K.~Fujiwara and F.~Kato,
\emph{Foundations of Rigid Geometry I},
EMS Monographs in Mathematics, vol.~7,
European Mathematical Society, 2018,
\href{https://doi.org/10.4171/135}{DOI}.

\bibitem{HK}
D.~Hansen and K.~S. Kedlaya,
\emph{Sheafiness criteria for Huber rings},
preprint, version of 23 April 2025,
\href{https://kskedlaya.org/papers/criteria.pdf}{preprint PDF}.

\bibitem{XiaCode}
B.~Xia,
Lean source code,
\href{https://github.com/leanprover-community/mathlib4/pull/36507}{mathlib pull request \#36507}.

\bibitem{Huber93}
R.~Huber,
\emph{Continuous valuations},
Math. Z. \textbf{212} (1993), no.~3, 455--477,
\href{https://doi.org/10.1007/BF02571668}{DOI}.

\bibitem{Huber94}
R.~Huber,
\emph{A generalization of formal schemes and rigid analytic varieties},
Math. Z. \textbf{217} (1994), 513--551,
\href{https://doi.org/10.1007/BF02571959}{DOI}.


\bibitem{KedlayaAWS}
K.~S. Kedlaya,
\emph{Sheaves, stacks, and shtukas},
Arizona Winter School notes, 2017,
\href{https://swc-math.github.io/aws/2017/2017KedlayaNotes.pdf}{course notes}.

\bibitem{KL}
K.~S. Kedlaya and R.~Liu,
\emph{Relative $p$-adic Hodge theory: Foundations},
Ast\'erisque \textbf{371} (2015),
\href{https://arxiv.org/abs/1301.0792}{arXiv:1301.0792}.

\bibitem{KST}
M.~Kerz, S.~Saito, and G.~Tamme,
\emph{$K$-theory of non-archimedean rings II},
Nagoya Math. J. \textbf{251} (2023), 669--685.

\bibitem{Lean4}
L.~de Moura and S.~Ullrich,
\emph{The Lean 4 theorem prover and programming language},
in \emph{Automated Deduction---CADE 28},
Lecture Notes in Comput. Sci., vol.~12699, Springer, 2021, 625--635,
\href{https://doi.org/10.1007/978-3-030-79876-5_37}{DOI}.

\bibitem{mathlib}
The mathlib Community,
\emph{The Lean mathematical library},
in \emph{Proceedings of the 9th ACM SIGPLAN International Conference on
Certified Programs and Proofs}, ACM, 2020, 367--381,
\href{https://doi.org/10.1145/3372885.3373824}{DOI}.

\bibitem{Milnor}
J.~Milnor,
\emph{Introduction to Algebraic $K$-Theory},
Annals of Mathematics Studies, vol.~72,
Princeton University Press, Princeton, 1971.

\bibitem{Mihara}
T.~Mihara,
\emph{On Tate's acyclicity and uniformity of Berkovich spectra and adic spectra},
Israel J. Math. \textbf{216} (2016), no.~1, 61--105.

\bibitem{Scottish}
K.~S. Kedlaya,
\emph{The Nonarchimedean Scottish Book}, Problems~7, 24, and 28,
\href{https://web.archive.org/web/20251124070248/https://scripts.mit.edu/~kedlaya/wiki/index.php?title=The_Nonarchimedean_Scottish_Book}{available
online}, Internet Archive snapshot of 24 November 2025 of the author's wiki at
MIT.

\bibitem{Stacks}
The Stacks Project Authors,
\emph{The Stacks Project},
\href{https://stacks.math.columbia.edu}{project website}.

\bibitem{Wedhorn}
T.~Wedhorn,
\emph{Adic spaces},
2019,
\href{https://arxiv.org/abs/1910.05934}{arXiv:1910.05934}.

\end{thebibliography}

\end{document}