Uniform sheafy Tate rings that are not stably uniform — the Lean formalisation
Lean 4 formalisation of the two counterexamples in Uniform sheafy Tate rings that are not stably uniform (Birkbeck–Torzewski).
The paper answers Question 7 of Kedlaya's Nonarchimedean Scottish Book:
Let
(A, A⁺)be a sheafy uniform Huber pair. Is(A, A⁺)necessarily stably uniform?
The answer is no. Buzzard–Verberkmoes and Mihara showed that a stably uniform Tate Huber ring is sheafy; the paper constructs two uniform, strongly sheafy Tate rings that are not stably uniform. In the first, a rational localisation is non-reduced; in the second, the rational localisation is an integral domain but is not uniform.
Both constructions, the rational localisations witnessing the failure, and their sheafiness are
formalised here — and the two headline theorems are kernel-certified: each statement is
pinned in a file that cannot see its own proof, the proofs are replayed through the Lean
kernel, and the axiom budget is exactly propext, Quot.sound, Classical.choice. Nothing is
assumed, and no certified proof contains a sorry.
The paper's own account of the formalisation is Appendix A.
The two theorems
Theorem 1.1 — the finite-jet ring
Paper: §3, The finite-jet ring · §4, A rational localisation which is not uniform · §6, Milnor descent and strong sheafiness
A is a complete uniform non-noetherian Tate k-algebra and an integral domain, with
A° = A₀. It is strongly sheafy — in particular (A, A°) is sheafy. But
A⟨W/ϖ⟩ ≅ k⟨X, Q⟩/(Q²), X = W/ϖ,
which is non-reduced, so A is not stably uniform.
In Lean, A is the pullback 𝓐 = 𝓑 ×_𝓓 𝓒 of the pinching (Milnor) square
| ring | |
|---|---|
L = k⟨W, W⁻¹⟩ | radius-one restricted Laurent algebra |
𝓑 = k⟨W, Q⟩/(Q²) | realised norm-faithfully as DualNumber (k⟨W⟩) |
𝓒 = L⟨Q⟩ | |
𝓓 = L⟨Q⟩/(Q²) |
realised concretely as the closed subring of 𝓒 of series whose Q⁰- and Q¹-coefficients
have nonnegative W-support.
Definition: FiniteJetOver.JetA K in Adic spaces/FJP/Over/JetRings.lean, over an
arbitrary complete ultrametric nontrivially-normed field K.
Endpoints: Adic spaces/FJP/Over/SheafyEndpoints.lean and Over/StrongSheafy.lean, at the
layer-2 (_of_dvr) form where the valuation ring of K is a DVR.
| paper | Lean | certified |
|---|---|---|
| sheafy | FiniteJetOver.isSheafy_JetA_of_dvr | ✓ |
| uniform | FiniteJetOver.finiteJet_isUniform_of_dvr | ✓ |
| integral domain | FiniteJetOver.finiteJet_isDomain | ✓ |
| non-noetherian | FiniteJetOver.finiteJet_not_noetherian | ✓ |
A° = A₀ | FiniteJetOver.finiteJet_powerBounded_eq_unitBall_of_dvr | ✓ |
| strongly sheafy | FiniteJetOver.finiteJet_tateExt_isSheafyComplete_of_dvr | ✓ |
| not stably uniform | FiniteJetOver.finiteJet_not_stablyUniform_of_dvr | ✓ |
𝓐° is a ring of integral elements | ValuationSpectrum.isRingOfIntegralElements_powerBoundedSubring | ✓ |
so is 𝓐⟨V₁,…,Vₙ⟩° | the same, at the Tate extension | ✓ |
These are the declarations the paper's own <lean> references for Theorem 1.1 point at. A
parallel development over the concrete witness base k = F((t)) lives in
Adic spaces/FJP/ (FiniteJet.JetA F, endpoints in FJP/FiniteJetMain.lean); the
general-base statements above specialise to it.
Theorem 8.1 — the weighted-parity algebra
Paper: §8, A second example · §8.1, The weighted-parity algebra · §8.4, A reduced rational chart which is not uniform · §8.5, Strong sheafiness
For a weight w : ℕ_{>0} → ℕ with w(n) ≥ 1 and unbounded, the complete Tate k-algebra
𝒜_w satisfies:
𝒜_wis a uniform, non-noetherian integral domain with𝒜_w° = 𝒜_{w,0};𝒜_wis strongly sheafy — in particular(𝒜_w, 𝒜_w°)is sheafy;- the rational localisation
ℬ_w = 𝒜_w⟨W/ϖ⟩is an integral domain but is not uniform.
Hence 𝒜_w is not stably uniform — and this time the failure is not explained away by a
nilpotent, which is what makes this example sharper than Theorem 1.1.
In Lean, 𝒜_w is the subring of the countable restricted Tate algebra k⟨W, U₁, U₂, …⟩ of
series supported on the weighted-parity monoid of w.
Definition: WeightedParity.WPA K w in Adic spaces/WP/Algebra.lean, for a general weight.
Endpoints: Adic spaces/WP/Main.lean, at the paper's weight w = id
(WeightedParity.idWeight).
| paper | Lean | certified |
|---|---|---|
| uniform | WeightedParity.weightedParity_isUniform_of_dvr | ✓ |
| integral domain | WeightedParity.weightedParity_isDomain | ✓ |
| non-noetherian | WeightedParity.weightedParity_not_noetherian | ✓ |
𝒜° = 𝒜₀ | WeightedParity.weightedParity_powerBounded_eq_unitBall | ✓ |
| sheafy | WeightedParity.weightedParity_isSheafyComplete_of_dvr | ✓ |
| strongly sheafy | WeightedParity.weightedParity_stronglySheafy_of_dvr | ✓ |
| not stably uniform | WeightedParity.weightedParity_not_stablyUniform_of_dvr | ✓ |
𝒜° is a ring of integral elements | ValuationSpectrum.isRingOfIntegralElements_powerBoundedSubring | ✓ |
so is 𝒜_{w+s}° | the same, at the shifted weights | ✓ |
The base is an abstract complete ultrametric nonarchimedean field whose valuation ring is a DVR, rather than a fixed witness field.
Scope of the certificate
Eighteen statements are certified — nine per theorem — and together they are exactly the conclusions of the two theorems as the paper states them, over a general base: an arbitrary complete ultrametric nontrivially-normed field whose valuation ring is a discrete valuation ring. Neither certificate is pinned to a concrete witness field.
Two of the nine on each side exist because a universally quantified statement can be true for
the wrong reason, and a certificate should rule that out rather than invite the reader to
check. IsSheafyComplete A quantifies over RingOfIntegralElements A, which is a subtype;
over an empty subtype it would hold vacuously and say nothing about (𝓐, 𝓐°). So the maximal
plus ring is certified to be a ring of integral elements — for 𝓐 and 𝒜 themselves, and
separately for the Tate extensions 𝓐⟨V₁,…,Vₙ⟩ and the shifted-weight algebras, which the
strong-sheafiness statements range over. The extension case needed
ValuationSpectrum.isRingOfIntegralElements_powerBoundedSubring, which establishes this for
any Huber ring: the pre-existing argument obtained openness from a metric ball, and the
extensions carry a basis-defined topology rather than a norm.
For the same reason IsStablyUniform now quantifies only over data satisfying D.IsRational
(changed 2026-08-22). RationalLocData is raw data — a pair of definition, a finite T, an
s, a bounded-denominator condition — and carries no guarantee that the ideal generated by T
is open, which is Wedhorn Definition 7.29's condition for D to present a rational subset
R(T/s); IsRational is the separate predicate saying it does, and it constrains T alone,
not T together with s. Because 𝓐 is Tate, openness is here equivalent to span T = ⊤ —
an open ideal contains a power of a topologically nilpotent unit, hence a unit
(RationalLocData.IsRational.span_eq_top; isRational_of_span_eq_top is the converse) — and
that is the form chartDatum_isRational establishes. Quantifying over all data made the class
stronger than stable uniformity in the standard sense and so its negation weaker than the
standard failure, which is the only way this development uses it. The proofs were unaffected —
they always instantiated at the chart datum, which is rational — but the statement now says
what it should.
The challenge files state all of this from the definition layer alone. For the finite-jet
ring that required one refactor: the uniformizer-free IsHuberRing/IsTateRing instances,
without which ¬ IsStablyUniform (JetA K) does not even elaborate, used to live in
Over/Functoriality.lean — a module whose import closure contains Over/Chart.lean, and so
the proof of not_isStablyUniform_JetA. They now live in
Adic spaces/FJP/Over/TateInstances.lean, whose closure is the definition layer plus the
base-agnostic FaithfulLocLift, so the challenge can state the conclusions without seeing
any proof of them.
The Palomar submission
Palomar registers machine-checked Lean proofs, with the rule that the Challenge — the small file a reader audits — imports nothing but Mathlib. Mathlib has no Huber rings or adic spaces, so the Palomar Challenge here is self-contained:
| path | what it is |
|---|---|
Challenge.lean | [FJP] Theorem 1.1, stated on Mathlib alone: Wedhorn's definitions (Huber/Tate rings, Spa, rational localisations and their completions, the structure presheaf as a TopCat.Presheaf TopCommRingCat, sheafiness as Mathlib's TopCat.Presheaf.IsSheaf), the Gauss-norm Tate algebras R⟨G⟩ = Completion R[G], the ring 𝓐 as the closure of the jet polynomials of [FJP] (1.7), and the nine statements with sorry. Within Palomar's 1000-line ceiling, no project imports. |
Solution.lean | the same nine, proved by forwarding the library's theorems across the bridges |
Palomar/Bridge.lean | the Challenge's notions are the library's: the completed rational localisations are the same type; restriction families are unique (RestrictionFamily.ext'); the Challenge's sheafiness is the library's finite rational-cover criterion (PalomarBridge.isSheafy_iff, both directions) |
Palomar/Bridge/Jet.lean, Palomar/Bridge/TateExt.lean | the Challenge's 𝓐 and 𝓐⟨X₁,…,Xₙ⟩ are isometrically isomorphic to the library's (jetAEquiv, gaussEquiv): the Laurent-polynomial / polynomial embeddings are isometries with dense image, so the completions are the library's restricted-series rings |
Palomar/Defs.lean | generated (scripts/gen-defs.py): the Challenge minus its statements, imported by the Solution and bridges, because comparator forbids the Solution from importing the Challenge itself |
comparator.json | selects all nine statements |
The Challenge's statements are equivalent to the library's endpoints, not weaker: sheafiness
is stated for every ring of integral elements (IsSheafyComplete, Wedhorn 8.26, which the
library also proves), and the Tate algebras carry the Gauss-norm topology, which the library
identifies with its Tate-ring topology. The bridges are the proof of that; formalization.yaml
records it under fidelity.statement_provenance.
bash scripts/certify.sh # the Palomar certificate — ends `Your solution is okay!`
Check it yourself
Build
lake exe cache get # mathlib oleans for v4.33.0
lake build # the library — it is this repository's only build target
mathlib is the only dependency. The first build compiles the library from source and takes a while; after that it is incremental.
Kernel certification
The two theorems are certified with leanprover/comparator.
One-time setup — comparator and lean4export must be built on the same toolchain as this
repository, leanprover/lean4:v4.33.0:
git clone https://github.com/leanprover/comparator /tmp/comparator
cd /tmp/comparator && lake build
# the lean4export artifact lake fetches is a Linux ELF; build it natively instead
git clone https://github.com/leanprover/lean4export /tmp/lean4export
cd /tmp/lean4export && git checkout \
$(python3 -c "import json;print([p['rev'] for p in \
json.load(open('/tmp/comparator/lake-manifest.json'))['packages'] \
if p['name']=='lean4export'][0])") && lake build
Then, from this repository's root:
bash scripts/certify.sh # Palomar: Theorem 1.1 on Mathlib alone
CONFIG="Adic spaces/Comparator/comparator-config.json" \
bash scripts/certify.sh # in-library: Theorem 1.1 — nine statements
CONFIG="Adic spaces/Comparator/wp-config.json" \
bash scripts/certify.sh # in-library: Theorem 8.1 — nine statements
Each run ends Your solution is okay!.
On Linux, install landrun for real sandboxing. On macOS
the script falls back to comparator's fake-landrun.sh shim — acceptable here, since the
"submission" being judged is this repository's own code rather than an adversarial one.
What certification buys over #print axioms
For each certified name, comparator
- rebuilds the solution module in a sandbox,
- checks that the solution's statement is structurally identical to the challenge's — and the challenge is a file the solution does not get to edit,
- checks the axiom set is within
propext,Quot.sound,Classical.choice, and - replays the proof through the Lean kernel.
#print axioms answers only (3), and only relative to whatever statement the library happens
to declare — it cannot tell you that the theorem says what you think it says. The trust
boundary is the point: each challenge file imports only the definition layer, and its
import closure provably contains none of the modules that prove the result. See
Adic spaces/Comparator/README.md for the full argument.
Numbering note. The Lean docstrings were written against an earlier revision of the paper
and cite these results as [FJP] Thm 1.3 and [WP] thm 6.2. In the current revision they are
Theorem 1.1 and Theorem 8.1; the certificate names (fjp_1_1_*, wp_8_1_*) follow the current
numbering.
Repository map
| path | what it is |
|---|---|
Adic spaces/FJP/ | Theorem 1.1 — the finite-jet ring |
Adic spaces/FJP/Over/ | the same over a general complete discretely valued base |
Adic spaces/WP/ | Theorem 8.1 — the weighted-parity algebra |
Palomar/ | the Palomar submission: the self-contained Challenge, the Solution, and the bridges (above) |
Adic spaces/Comparator/ | the in-library certificate pairs and their configs (their challenges import the library's definition layer) |
Adic spaces/ (rest) | the supporting adic-spaces library the examples are built on: continuous valuations, Spa, Tate rings, rational subsets, the structure presheaf, completions, Čech cohomology, Milnor squares |
Adic spaces/ScottishBook/ | the Nonarchimedean Scottish Book — Kedlaya's open-problem list, one module per problem, statements only |
scripts/certify.sh | the comparator run (CONFIG selects the Palomar or in-library certificate), plus its one-time setup instructions |
scripts/gen-defs.py | regenerates Palomar/Defs.lean from the Challenge; --check in CI |
scripts/validate-formalization-yaml.py | Palomar's mechanical checks on formalization.yaml |
formalization.yaml | the formalisation self-report (below) |
The manifest
formalization.yaml is a self-report in the
mathlib-initiative schema
(v0.4, with the fields Palomar requires): the sources and their licences, the scope of what is formalised, the per-result
axiom status and comparator config for each headline theorem, the automation provenance
with its cost caveats, and the fidelity divergences from the paper. Fields that need a human
answer are left blank rather than guessed. It is a page long and is the right place to start
if you want the claims without reading Lean.
A handful of docstrings in the supporting library (25 files) point at AINTLIB's internal
planning notes — paths like .mathlib-quality/… or docs/plans/…. Those files are development
process rather than mathematics, so they are not carried here; they live
upstream. None of the certified results depend on them.
Toolchain
Lean v4.33.0 (stable) and mathlib release tag v4.33.0 (db584cd6d46c).
This is deliberate. The v4.33 line is the first stable release line carrying the fix for
kernel soundness bug leanprover/lean4#14576
— an axiom-free proof of False via unchecked projections on phantom-parameter nested
inductives, reported 2026-07-28 and fixed the same day in
#14577. Comparator is built on the same
toolchain, so the judging kernel and the judged development agree.
On sorry
Every certified statement — all eighteen — has a sorry-free proof closure. This is not a
claim you have to take on trust: a sorry anywhere in a proof's closure shows up as the axiom
sorryAx, and both comparator runs pass with an axiom set of exactly
[propext, Quot.sound, Classical.choice].
The wider library does contain sorrys, none of them on the certified results' path:
- the Nonarchimedean Scottish Book modules, which are open-problem statements by design;
Adic spaces/WP/HeadReduced.lean, a quarantined conditional route to a rational stable reducedness claim that the current revision of the paper no longer makes;- work-in-progress frontiers of the general adic-spaces development (the Wedhorn 8.28(b) campaign) that the two examples do not depend on.
As of this commit that is 155 declarations across the tree, none of them in the finite-jet group and none on a certified proof's closure.
Provenance
From the paper's abstract: "The two main results are due to ChatGPT 5.6 Sol." The Lean
formalisation was carried out by Claude Code. The paper's
§9, How the examples were found
tells that story; formalization.yaml records the model, framework and cost caveats for the
formalisation side.
This repository is a standalone extract of the adic-spaces development in
AINTLIB, an AI-built and AI-maintained number-theory
library, where the work continues on the announce/sheafy-not-stably-uniform branch. The
extract carries the library and the certificates, and drops the monorepo's other projects and
its internal process files. It differs from the AINTLIB tree in exactly one mathematical
respect: the instance Module.Flat.pi (finite products of flat modules are flat), which
AINTLIB factors out into its shared Common library, is declared inline in
Adic spaces/FlatnessResults.lean here so that this repository has mathlib as its only
dependency.
Licence
Apache 2.0 — see LICENSE.