Depth-one Artin–Schreier defect towers are composita

Dev D. Goyal

Depth-one Artin–Schreier defect towers are composita

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Selected result in this collection

Problem and result

Problem: Nart–Novacoski conjecture on depth-one Artin–Schreier defect towers
Posed in: Nart and Novacoski, 'Depth of Artin–Schreier defect towers', J. Pure Appl. Algebra 230 (2026), 108184 (arXiv:2503.18827), Conjecture 4.1
Status: Proved
Result: Over a perfect henselian K ⊆ k((y^ℚ)) containing k(y) without finite accumulation points (k algebraically closed, char. p), each nontrivial finite Artin–Schreier tower of depth one is a compositum of Artin–Schreier extensions.

Abstract

Let k be algebraically closed of characteristic p > 0 and K a perfect henselian subfield of the Hahn field k((y^ℚ)) that contains k(y) and whose elements have no finite accumulation points in their supports. If a nontrivial finite Artin–Schreier tower M/K has depth one, then M is a compositum of Artin–Schreier extensions of K. Nart and Novacoski proved the reverse implication and conjectured this one. For every θ in M outside K, the truncation of θ at the first finite accumulation point of its support generates a nontrivial elementary abelian subextension of K(θ)/K; the extraction adapts an Ore-relation argument of Kedlaya.

Details

Year: 2026
Discipline: Mathematics
Area: Valuation theory
Subject: Valuation theory
Result type: Theorem resolving a published conjecture and reproducible proof package
Formal proof: Standalone Lean package
Family: artin-schreier-depth
Keywords: Artin–Schreier extensions, defect extensions, depth of valued field extensions, Okutsu sequences, Mac Lane–Vaquié chains, Hahn series, Krasner lemma, Nart–Novacoski conjecture

Statement and scope

Formal scope. Both implications are formalized in two Lean projects. The Lean 4.35 project states the conjecture for every finite Artin–Schreier tower over a base whose valuation ring is henselian in Mathlib's sense, with depth one defined as the least length of a complete Mac Lane–Vaquié chain over all primitive generators; it compares these chains with Okutsu sequences at length one only. The Lean 4.19 project states depth one through Okutsu sequences in the algebraic closure of K inside the Hahn field.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 304 KB
PDF on GitHub: papers/mathematics/artin-schreier-depth/manuscript.pdf
LaTeX source: papers/mathematics/artin-schreier-depth/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Reproduce

The commands below are quoted from papers/mathematics/artin-schreier-depth/VERIFICATION.md, which gives their context and working directory.

Mac Lane–Vaquié project

lake exe cache get
lake build Cli
python3 scripts/verify_cached.py --mathlib-cache .lake/packages/mathlib \
  --lean-bin "$(lean --print-prefix)/bin/lean" --packages-root .lake/packages \
  --output /tmp/artin-schreier-depth-mlv-verification --module-timeout 900

Okutsu project

lake exe cache get
lake build Cli
python3 scripts/verify_cached.py --mathlib-cache .lake/packages/mathlib \
  --lean-bin "$(lean --print-prefix)/bin/lean" --packages-root .lake/packages \
  --output /tmp/artin-schreier-depth-verification

README: papers/mathematics/artin-schreier-depth/README.md
Verification guide: papers/mathematics/artin-schreier-depth/verification/README.md
Verification record: papers/mathematics/artin-schreier-depth/VERIFICATION.md
Authorship: papers/mathematics/artin-schreier-depth/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Nart and Novacoski, 2026.

Source. Nart and Novacoski (JPAA 2026; arXiv:2503.18827v2) stated the converse as Conjecture 4.1 and proved the forward implication. The minimal-face extraction is Kedlaya's (2017, Lemma 9.3). Historical priority is not certified.

Questions and answers

Is the Nart–Novacoski conjecture proved?

This preprint proves Conjecture 4.1 in its stated setting: over a perfect henselian subfield K of k((y^ℚ)) containing k(y) whose elements have no finite accumulation points, with k algebraically closed of characteristic p, a nontrivial finite Artin–Schreier tower of depth one is a compositum of Artin–Schreier extensions of K. Nart and Novacoski proved the reverse implication.

Is the proof formally verified?

Yes. Both implications are formalized in two Lean 4 projects. The Lean 4.35 project, with 100 freshly compiled modules, defines depth by genuine Mac Lane–Vaquié chains, uses ordinary henselianity and proves the comparison with Okutsu sequences at length one, which is all the conjecture needs; no comparison at other lengths is formalized.

What prior work does the proof rely on?

The extraction step adapts an Ore-relation argument of Kedlaya (2017, Lemma 9.3), and the root formula, support estimates and Krasner's lemma are standard. It is an unrefereed preprint, the journal version of the source could not be opened, and historical priority is not certified.

Cite

Citation file papers/mathematics/artin-schreier-depth/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026asdepthtowers,
  author = {Goyal, Dev D.},
  title = {Depth-One {Artin}--{Schreier} Defect Towers Are Composita},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/artin-schreier-depth}
}