Shafarevich's relation-rank bound

shafarevich_relation_rank_bound — a formalization challenge from the lean-eval benchmark.

Notes

For a number field F and odd prime p, with G = Gal(F^{un,p}/F) the Galois group of the maximal unramified pro-p extension, the relation rank r(G) = dim_{𝔽_p} H²(G; 𝔽_p) is finite and r(G) ≤ d(G) + (r₁ + r₂ - 1) + δ_p(F), where d(G) is the generator rank, r₁/r₂ are the numbers of real/complex places of F, and δ_p(F) = 1 iff F contains a primitive p-th root of unity. The statement rests on substantial trusted scaffolding (non-holes): the bespoke construction MaxUnramifiedProPGaloisGroup (with IsEverywhereUnramified and maximalUnramifiedProPF) fixing Gal(F^{un,p}/F), and the rank definitions generatorRank, relationRank, H2Finite — a solver proves the inequality about these definitions, whose correctness is part of the trusted statement. This is one of the two external inputs taken as a hypothesis in Logical Intelligence's formalization of the disproof of Erdős's unit-distance conjecture (Hyp_ShafarevichRelationRankBound). It was reviewed for faithfulness against Mayer Theorem 5.1 (S=∅) and Koch 11.5/11.8; the unit-rank term r₁+r₂-1 and the root-of-unity correction match Mayer's corrected statement, and the MaxUnramifiedProPGaloisGroup construction was checked as a faithful (non-vacuous) maximal unramified pro-p extension in the source development (whose universal-property/maximality lemmas are not shipped with this problem — only the definitions are).

Formal statement

/-- **Shafarevich's relation-rank bound** (odd `p`, empty-`S` specialization).

For a number field `F` and an odd prime `p`, with `G = Gal(F^{un,p}/F)` the
Galois group of the maximal unramified pro-`p` extension, the relation rank is
finite and

r(G) ≤ d(G) + (r₁ + r₂ - 1) + δ_p(F),

where `r₁ = nrRealPlaces F`, `r₂ = nrComplexPlaces F`, and `δ_p(F) = 1` iff `F`
contains a primitive `p`-th root of unity.

References: Mayer, Theorem 5.1 (`S = ∅`); Koch, Theorems 11.5 and 11.8. -/
theorem shafarevich_relation_rank_bound
    (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime] (_hpOdd : Odd p) :
    H2Finite p (MaxUnramifiedProPGaloisGroup F p) ∧
      (open Classical in
       relationRank p (MaxUnramifiedProPGaloisGroup F p) ≤
        generatorRank (MaxUnramifiedProPGaloisGroup F p) +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  sorry

Informal solution sketch

Compute the cohomology of the pro-p group G = Gal(F^{un,p}/F) via class field theory. The generator rank d(G) = dim H¹(G; 𝔽_p) is the p-rank of the ray/Hilbert class field data, and the relation rank r(G) = dim H²(G; 𝔽_p) is bounded using the global Euler-characteristic / Poitou–Tate duality for the maximal unramified pro-p extension: the difference r(G) - d(G) is controlled by the unit group and the p-th roots of unity, giving r(G) - d(G) ≤ (r₁ + r₂ - 1) + δ_p(F) (the Dirichlet unit rank plus the δ-term recording whether ζ_p ∈ F). Faithful to Mayer's Theorem 5.1 with empty ramification set S.

Source

D. C. Mayer, New number fields with known p-class tower, Tatra Mt. Math. Publ. 64 (2015), 21–57 (Theorem 5.1, S=∅; arXiv:1510.00565); H. Koch, Galois Theory of p-Extensions, Springer 2002 (Theorems 11.5 and 11.8); I. R. Shafarevich, Extensions with prescribed ramification points (1963). Lean hypothesis: https://github.com/logical-intelligence/erdos-unit-distance (Hyp_ShafarevichRelationRankBound).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: shafarevich_relation_rank_bound
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.