OpenAI claim summary for Math-2796

Bogomolov-Pop pro-ell reconstruction

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 009; 2026-09-23), the asserted result is that for function fields of dimension at least two with algebraically closed constant fields, if $\ell$ is unequal to the characteristic, its pro-$\ell$ abelian-by-central quotient determines both the constant field and the function field's perfect closure.

Mathematical statement of the claimed result

Manuscript 1.

For a fixed prime $\ell$ and fields of characteristic different from $\ell$, let $G_F^{(\ell)}$ be the maximal pro-$\ell$ absolute Galois quotient, $\Pi_F^a=G_F^{(\ell)}/[G_F^{(\ell)},G_F^{(\ell)}]$ and $\Pi_F^c=G_F^{(\ell)}/[[G_F^{(\ell)},G_F^{(\ell)}],G_F^{(\ell)}]$, using closed commutator subgroups. A continuous $\mathbb Z_{\ell}$-linear isomorphism of abelian quotients is compatible when it carries the induced alternating commutator pairing to the other pairing through an isomorphism of central kernels. For function fields $K/k,L/l$ over algebraically closed constants with transcendence degrees at least two, the claimed bijection is \[ \operatorname{Isom}_{\rm F}^{i}(K,L)\xrightarrow{\sim} \operatorname{Isom}^{c}(\Pi_L^a,\Pi_K^a)/\mathbb Z_{\ell}^{\times}. \] The left uses perfect-closure field isomorphisms carrying constants onto constants, modulo integral Frobenius powers in positive characteristic; the right identifies compatible maps up to unit scaling. This includes transcendence degree two and $\ell=2$.

Outline of the argument

For manuscript 1 (family 009; 2026-09-23), commutator relations detect valuations through alternating characters. Kummer tests and uniformly bounded pencils identify curve subfields and rational quotients, from which incidence reconstruction yields the field with exactly the scalar and Frobenius ambiguities.

Formal verification

For manuscript 1 (family 009; 2026-09-23), the documented Lean scope is uniqueness of perfect-closure field maps modulo Frobenius once the induced Galois correspondence agrees up to an $\ell$-adic unit; existence for every admissible correspondence is not included.

The selected formal statement has narrower scope than the full manuscript claim.

The linked family Comparator checks are BogomolovPopInjectivity.lean.

Their named declarations include OAI.BogomolovPop.main_graph_injective.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, The Bogomolov–Pop reconstruction theorem, 2026-09-23; citation key OAI:The-Bogomolov-Pop-reconstruction-theorem-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 009: Lean scope.
• Comparator BogomolovPopInjectivity.json.
• Comparator BogomolovPopInjectivity.lean.
• OpenAI catalogue entry.