# Function-field reconstruction from Milnor K-theory and Galois data

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Bogomolov-Pop reconstruction theorem](../../preprints/The-Bogomolov-Pop-reconstruction-theorem-September-23-2026/paper.pdf)

## Scope

The Bogomolov–Pop reconstruction conjecture concerns recovering a function field and its constants from pro-$\ell$ abelian-by-central Galois data. The linked formalization proves injectivity of the reconstruction correspondence for function fields of transcendence degree at least two over algebraically closed fields of characteristic different from the prime $\ell$.

If two isomorphisms of perfect closures preserving the constant fields induce the same Galois-data isomorphism modulo $\ell$-adic unit scaling, then they agree modulo Frobenius. The selected statement proves this uniqueness; existence of a field isomorphism for every admissible Galois-data isomorphism is outside it.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Injectivity of Bogomolov–Pop reconstruction modulo the stated ambiguities | [BogomolovPopInjectivity.lean](../ComparatorChallenges/BogomolovPopInjectivity.lean) |