# formalization.yaml — self-report for this repository, in the mathlib-initiative # schema v0.4 (https://github.com/mathlib-initiative/formalization.yaml), with the # additional fields the Palomar registry makes mandatory # (https://github.com/PalomarRegistry/PalomarPolicy/blob/main/CONTRIBUTING.md §3). # # `sources[].license` is the licence of the SOURCE MATERIAL being formalized — the paper # or notes whose statements were transcribed — not the licence of this Lean code, which is # `project.license`. # # FIELDS LEFT BLANK ARE NOT YET KNOWN. They are deliberately empty rather than guessed. version: "v0.4" project: name: "Uniform sheafy Tate rings that are not stably uniform" description: >- A Lean 4 formalisation of *Uniform sheafy Tate rings that are not stably uniform* (Birkbeck–Torzewski), answering Question 7 of Kedlaya's *Nonarchimedean Scottish Book* in the negative: a sheafy uniform Huber pair need not be stably uniform. Buzzard–Verberkmoes and Mihara proved that stably uniform Tate Huber rings are sheafy; whether the converse holds was open. The paper gives two complete Tate algebras over a complete discretely valued field `k` that are uniform, nonnoetherian integral domains with `A° = A₀`, strongly sheafy (every Tate algebra `A⟨X₁, …, Xₙ⟩` is sheafy), and yet not stably uniform, because an explicit rational localisation is not uniform. The first (Theorem 1.1) is the finite-jet pinching algebra `𝓐 = B ×_D C`, the pullback of a Milnor square with `B = k⟨W, Q⟩/(Q²)`, `C = k⟨W, W⁻¹⟩⟨Q⟩`, `D = C/(Q²)` — concretely, the series in `k⟨W, W⁻¹⟩⟨Q⟩` whose `Q⁰`- and `Q¹`-coefficients have nonnegative `W`-support; its bad chart `𝓐⟨W/ϖ⟩ ≅ k⟨X, Q⟩/(Q²)` is non-reduced. The second (Theorem 8.1) is the weighted-parity algebra `𝒜_w`, whose bad chart is an integral domain; the paper proves it for every unbounded weight `w ≥ 1`, the formalisation for `w(n) = n`. This submission certifies the seven conclusions of Theorem 1.1 together with two statements ruling out a vacuous reading of its sheafiness claims, stated self-containedly on Mathlib in `Challenge.lean` over an arbitrary complete ultrametric field with DVR valuation ring; Theorem 8.1 is certified by the repository's in-library configuration. The repository also develops the surrounding theory after Wedhorn's *Adic Spaces*: Huber and Tate rings, the adic spectrum, rational localisations, the structure presheaf, and sheafiness (Definition 8.26), including the strongly noetherian theorem (8.28(b)). authors: - "Christopher Birkbeck" - "Alex Torzewski" # [Palomar, required] People responsible for THIS submitted formalisation. responsible_maintainers: - "Christopher Birkbeck" - "Alex Torzewski" license: "Apache-2.0" # matches the root LICENSE file and the Lean file headers. # [Palomar, required] Classification of the MATHEMATICS, not of the use of Lean or AI. classification: arxiv: - "math.AG" # Algebraic Geometry — adic spaces / rigid analytic geometry - "math.NT" # Number Theory — nonarchimedean fields, the perfectoid milieu msc2020: - "14G22" # Rigid analytic geometry - "12J25" # Non-Archimedean valued fields - "13J10" # Complete rings, completion - "16W80" # Topological and ordered rings and modules - "14G45" # Perfectoid spaces and mixed characteristic # [Palomar, required] Where the result came from. Exactly one entry carries the # substantive relationship (`formalizes`), so the derived origin is `source-based`. sources: - title: "Uniform sheafy Tate rings that are not stably uniform" authors: ["Christopher Birkbeck", "Alex Torzewski"] id: "https://cbirkbeck.github.io/uniform-sheafy-tate-domains/" type: "paper" relationship: "formalizes" license: "none stated" author_endorsement: "participated" note: >- The paper this repository formalises. Its two headline theorems are the results certified here: the finite-jet pinching algebra (Theorem 1.1) and the weighted-parity algebra (Theorem 8.1, formalised at the weight `w(n) = n`). The Lean docstrings were written against an earlier revision and cite these as [FJP] Thm 1.3 and [WP] thm 6.2; `Adic spaces/Comparator/README.md` carries the numbering crosswalk. A source author is an author of this formalisation, hence `participated`. No arXiv identifier or DOI as of 2026-08-19; the project page above is the most stable identifier that exists. Novelty of the mathematics is the paper's claim, not a claim established by this formalisation. - title: "Adic Spaces (lecture notes)" authors: ["Torsten Wedhorn"] id: "arXiv:1910.05934" type: "paper" relationship: "background" license: "arXiv nonexclusive-distrib/1.0" author_endorsement: "not-contacted" note: >- The source of the ambient theory: Huber and Tate rings (§6), bounded and power-bounded subsets (§5), uniform and stably uniform pairs (Definitions 7.36, 7.37), rational localisations and the structure presheaf (§7–8), and sheafiness (Definition 8.26, Theorem 8.28(b)). Supplies the definitions the certified statements are phrased in, not the result itself. - title: "The Nonarchimedean Scottish Book" authors: [] contributors: - name: "Kiran S. Kedlaya" role: "editor of the problem collection" id: "https://scripts.mit.edu/~kedlaya/wiki/index.php?title=The_Nonarchimedean_Scottish_Book" type: "web discussion" relationship: "background" license: "none stated" author_endorsement: "not-contacted" note: >- The problem collection that poses Question 7 ("Let (A, A⁺) be a sheafy uniform Huber pair. Is (A, A⁺) necessarily stably uniform?"), which the formalised theorems answer in the negative. Recorded as background: it poses the question rather than supplying the result. A community wiki with no explicit copyright or licence notice; the URL above is the most stable identifier that exists. # Previous Lean work on this material, distinguished from the mathematical sources above. related_formalizations: [] automation: methods: - method: "agent" models: ["Claude Fable 5"] framework: "Claude Code" tool_setup: >- AI-assisted throughout. Lean 4 with mathlib, driven by the `mathlib-quality` Claude Code skill plugin (https://github.com/CBirkbeck/mathlib-quality), which supplies the planning, proving, cleanup, decomposition and review workflows the formalisation was carried out under. Developed upstream in AINTLIB (https://github.com/CBirkbeck/AINTLIB): per-project dev branches in one Lake workspace, with automated cleanup lanes on `main`. This repository is a standalone extract of the adic-spaces project from that workspace. cost: wall_time: "" spend_usd: "4 months of a Claude Code Max 20x subscription (flat-rate, not metered)" hardware: "" prompting_notes: >- The source paper records that the Lean formalisation was carried out by Claude Code. This entry covers the production of the LEAN CODE. - method: "other" models: ["ChatGPT 5.6 Sol"] framework: "" tool_setup: "" cost: wall_time: "" spend_usd: "1 month of a ChatGPT Pro subscription (flat-rate, not metered)" hardware: "" prompting_notes: >- Discovery of the underlying MATHEMATICS, not of the Lean code. Per the source paper's abstract, its two main results are due to ChatGPT 5.6 Sol. Recorded here as a material automated contribution to the result being registered; `other` is used because the upstream vocabulary describes how a formalisation was produced and has no category for the provenance of the theorem itself. spend_usd: "4 months Claude Code Max 20x + 1 month ChatGPT Pro" notes: >- COST CAVEAT: both figures are flat-rate subscriptions, not per-token metering, and each subscription covered all of the holder's work over that period rather than this project alone. So the subscription cost is an UPPER BOUND on what is attributable here, not a measurement of it, and no USD figure is quoted for that reason. Statement-level certification is available via leanprover/comparator; see `scripts/certify.sh` and the configs referenced under `status.main_results`. This repository pins Lean v4.33.0 (stable) + mathlib v4.33.0 — the first stable release line carrying the fix for kernel soundness bug leanprover/lean4#14576. # [Palomar, required] The review completed BEFORE submission. This is metadata about # work already done; it is not, and does not anticipate, the Palomar review. review: status: "agent-reviewed" reviewers: - name: "mathlib-quality automated review lanes" role: >- Independent AI review passes over the Lean development (definition necessity, generalisation, automation, mathlib naming and style), run as a distinct step from the proving work. https://github.com/CBirkbeck/mathlib-quality - name: "OpenAI Codex" role: >- Audit passes over the paper's claims against the Lean proofs, and over the attribution of results, carried out in the companion paper repository https://github.com/CBirkbeck/uniform-sheafy-tate-domains notes: >- No human peer review, and no external reviewer. The review recorded here is automated: distinct AI passes examined the development after it was written, separately from the agent that produced it. Independently of review, the certified statements are checked mechanically: leanprover/comparator pins each statement in a challenge module that cannot see its own proof, replays the proof through the Lean kernel, and confirms the axiom set is within {propext, Quot.sound, Classical.choice}. That is a mechanical check, not a review, and it is not the basis for the status above. status: scope: >- Huber/Tate rings, adic spectra, rational localizations and the structure presheaf (Wedhorn); the finite-jet ring (Theorem 1.1) and its chart; the weighted-parity algebra (Theorem 8.1) — both uniform, strongly sheafy, non-noetherian domains with `A° = A₀` that are not stably uniform, the first with a non-reduced bad chart and the second with a bad chart that is an integral domain; and formal statements of the Nonarchimedean Scottish Book problem list. Both theorems are certified over an abstract complete ultrametric nonarchimedean field whose valuation ring is a DVR, not over a fixed witness field. A parallel finite-jet development over the concrete base `LaurentSeries F` is also present (`FiniteJet`, as against the certified `FiniteJetOver`). sorry_count: 0 # scope: the formalization reported here — the fourteen # certified endpoints (nine per theorem) and their full # proof closures. Their axiom # sets are exactly [propext, Classical.choice, Quot.sound] # (no sorryAx), checked per-result by comparator. The # wider repository tree carries WIP `sorry`s outside this # report's scope (Scottish Book problem STATEMENTS, the # quarantined WP/HeadReduced.lean route, and general # Wedhorn 8.28(b) campaign frontiers). As of this commit: # 155 declarations with `sorry` across the tree, none of # them in the FJP group (0) or on a certified closure. sorry_in_definitions: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] main_results: # The Palomar certificate: [FJP] Theorem 1.1 stated self-containedly on Mathlib in # `Challenge.lean` (every notion the statements use is defined there, on Mathlib # alone) and proved in `Solution.lean` by forwarding the library's theorems across # `Palomar/Bridge*.lean`, which show the Challenge's notions are the library's. The # declarations listed are the Challenge's; `comparator.json` selects all nine. - declaration: "Palomar.fjp_1_1_isSheafy" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] - declaration: "Palomar.fjp_1_1_isUniform" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] - declaration: "Palomar.fjp_1_1_isDomain" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] - declaration: "Palomar.fjp_1_1_not_isNoetherianRing" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] - declaration: "Palomar.fjp_1_1_powerBounded_eq_unitBall" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] - declaration: "Palomar.fjp_1_1_stronglySheafy" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] - declaration: "Palomar.fjp_1_1_not_isStablyUniform" file: "Challenge.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "comparator.json" literature_dependencies: [] # The library's own endpoints, certified by the in-library comparator configs (whose # challenges import the library's definition layer rather than restating it). - declaration: "FiniteJetOver.finiteJet_isSheafyComplete_of_dvr" file: "Adic spaces/FJP/Over/SheafyEndpoints.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "Adic spaces/Comparator/comparator-config.json" literature_dependencies: [] - declaration: "FiniteJetOver.finiteJet_not_stablyUniform_of_dvr" file: "Adic spaces/FJP/Over/SheafyEndpoints.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "Adic spaces/Comparator/comparator-config.json" literature_dependencies: [] - declaration: "WeightedParity.weightedParity_isSheafyComplete_of_dvr" file: "Adic spaces/WP/Main.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "Adic spaces/Comparator/wp-config.json" literature_dependencies: [] - declaration: "WeightedParity.weightedParity_not_stablyUniform_of_dvr" file: "Adic spaces/WP/Main.lean" sorry_count: 0 axioms: ["propext", "Classical.choice", "Quot.sound"] comparator_config: "Adic spaces/Comparator/wp-config.json" literature_dependencies: [] fidelity: divergences: >- (1) SCOPE OF THE FJP BASE. The paper states its main theorem over a complete discretely valued nonarchimedean field k. The certified statements (`FiniteJetMain.lean`) instantiate k at the restricted Laurent-series field over an arbitrary coefficient field F — the base of the revision the Lean docstrings cite; the `FiniteJetOver` layer additionally states the uniform / domain / nonnoetherian / not-stably-uniform endpoints over an abstract such k (any complete ultrametric nontrivially-normed field, with the uniformizer explicit or chosen from a DVR hypothesis). (2) THE WP BASE. Theorem 8.1 is certified over an abstract complete ultrametric nontrivially-normed field K with `IsDiscreteValuationRing 𝒪[K]` — the paper's "complete discretely valued nonarchimedean field", with "discretely valued" rendered as the DVR property of the valuation ring. (3) STRONGLY SHEAFY. The paper's "(strongly) sheafy" (every 𝒜⟨V₁,…,Vₛ⟩ is sheafy) is rendered by the shifted-weight algebras (`shiftWeight`): the certificate pins sheafiness of `WPA K (shiftWeight id s)` for every s, and sheafiness itself is "every valid ring of integral elements gives a sheaf" (`IsSheafyComplete`, the complete-ring form of Wedhorn Definition 8.26). (4) SHEAFINESS AT TATE SCOPE. Wedhorn's Definition 8.26 is stated for arbitrary f-adic rings; the formalisation defines it at Tate (analytic) scope only (`IsSheafyTateRing`), because the restriction maps of Proposition 8.2 are derived from the complete-analytic route. Kedlaya Remark 1.6.10 records that the analytic and non-analytic cases genuinely differ. Both certified examples are Tate, so the statements are unaffected. statement_provenance: >- The Palomar Challenge (`Challenge.lean`) is self-contained on Mathlib: it defines, following Wedhorn, every notion its statements use — Huber/Tate rings, the adic spectrum, rational localisations and their completions, the structure presheaf as a `TopCat.Presheaf TopCommRingCat`, sheafiness as Mathlib's `TopCat.Presheaf.IsSheaf`, the Tate algebras as Gauss-norm completions of polynomial rings, and `𝓐` as the closure of the jet polynomials of [FJP] (1.7) — and imports no project source. `Palomar/Bridge.lean` proves these notions agree with the library's (the completed localisations are the same type; restriction families are unique; the Challenge's sheafiness is equivalent to the library's finite rational-cover criterion, `PalomarBridge.isSheafy_iff`), and `Palomar/Bridge/Jet.lean`, `Palomar/Bridge/TateExt.lean` that its rings are isometrically isomorphic to the library's. Two presentational choices were made for the Challenge and are equivalent to the library's statements, not weaker: sheafiness is stated for every ring of integral elements (`IsSheafyComplete`, Wedhorn 8.26, which the library also proves) rather than for `𝓐⁺ = 𝓐°` alone; and the Tate algebras `𝓐⟨X₁,…,Xₙ⟩` carry the Gauss-norm topology, which the library identifies with its Tate-ring topology. The in-library comparator challenges (`Adic spaces/Comparator/`) restate the conclusions from the library's definition layer instead. checked_by: "" # human sign-off pending acknowledgements: ""