Symbol length of Milnor K-theory mod p of ℂ(x₁, …, xₘ) (Becher–Hoffmann, Krashen)

### What is the conjecture

For a field $k$ and a modulus $\ell$ invertible in $k$, the norm residue isomorphism identifies $H^i(k, \mu_\ell^{\otimes i})$ with $K^M_i(k)/\ell$. That a class is a sum of *some* number of symbols is part of the presentation of Milnor K-theory, so the **symbol length problem** — how many symbols are needed — is entirely about the bound.

In degree $2$, over a field containing a primitive $\ell$-th root of unity, Merkurjev and Suslin's theorem that the norm residue map is an isomorphism (Math. USSR-Izv. **21** (1983), 307–340) identifies $K^M_2(k)/\ell$ with ${}_\ell\mathrm{Br}(k)$ and symbols with symbol algebras of degree $\ell$. That is the form in which the question is usually studied: how many symbol algebras are needed to represent a central simple algebra of exponent $\ell$.

Becher and Hoffmann named the degree-$2$ invariant $\lambda_p$ and asked it for exactly the fields below (*Symbol lengths in Milnor K-theory*, Homology Homotopy Appl. **6** (2004), no. 1, 17–31, [doi:10.4310/HHA.2004.v6.n1.a3](https://doi.org/10.4310/HHA.2004.v6.n1.a3), Question 4.6). The general form is Problem 2.1.3.12 of Krashen's notes for the PCMI 2024 minicourse *Field arithmetic and the complexity of algebraic objects*, draft of 24 July 2024, [pdf](https://www.ias.edu/sites/default/files/pcmi-2024-07-24%20krashen.pdf); Krashen notes there that over complex function fields in at least three variables no bound is known beyond Matzri's in degree $2$ and the case of $\ell$ a power of $2$, and that very little is known in degree $3$ and higher (§2.1.3.4).

**Concrete form to formalise.** Determine the symbol length of $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p$ as a function of $m$, $n$ and the prime $p$, possibly infinite. What is known:

* degree $0$: $K^M_0(F)/p = \mathbb{Z}/p$ has symbol length $p - 1$ for every field $F$.
* degree $1$: every class of $F^\times/(F^\times)^p$ is a single symbol.
* $n > m$: the field has cohomological dimension $m$ (Serre, *Galois cohomology*, Ch. II §4.2), so the group vanishes by Bloch–Kato.
* degree $2$ upper bound: $\mathbb{C}(x_1, \dots, x_m)$ is a $C_m$ field (Tsen–Lang), so Matzri's Theorem 8.2 (Trans. Amer. Math. Soc. **368** (2016), 413–427) gives $t(p^{m-1} - 1)$ modulo $p^t$.
* degree $2$ lower bound: a tensor product of $m - 1$ symbol algebras of degree $p$ can be a division algebra over $\mathbb{C}(x_1, \dots, x_m)$, so the symbol length is at least $m - 1$ (Becher–Hoffmann Proposition 4.5, by an argument going back to Nakayama).

Becher–Hoffmann Question 4.6 asks whether $m - 1$ is the answer in degree $2$. Even $m = 2$ is open: whether every class of $K^M_2(\mathbb{C}(x_1, x_2))/p$ is a single symbol is "a striking open question", holding for $p \le 3$ by a theorem of Artin. Since $m - 1$ does not involve $p$, that is an instance of the expectation recorded by Krashen that a bound can be taken independent of $\ell$.

### Prerequisites needed

Mathlib has no Milnor K-theory. This needs a definition in `FormalConjecturesForMathlib/`: the tensor algebra of `Additive Fˣ` modulo the Steinberg relations and modulo $\ell$, via `RingQuot`, together with symbols, the degree-$n$ part, and the set of symbol length bounds. No open Mathlib issue or PR covers this.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-12
* ams-16
* ams-19

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start in FormalConjecturesForMathlib/ and define the required Milnor K-theory construction using RingQuot, including symbols, degree-n parts, and symbol-length bounds. Read the issue's stated prerequisites and known bounds first. Done means the definitions and the concrete conjecture for K^M_n(ℂ(x₁, …, xₘ))/p are represented in Lean.

Written by the indexing model from the issue text.