From 395c154cc2b23493a706e16f0a2b72339a9a3a19 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 3 Jun 2026 08:37:21 +0000 Subject: [PATCH] feat: add Shafarevich relation-rank bound eval problem Add Shafarevich's relation-rank bound for the maximal unramified pro-p extension of a number field (odd p, empty-S specialization): with G = Gal(F^{un,p}/F), the relation rank r(G) = dim H^2(G; F_p) is finite and r(G) <= d(G) + (r_1 + r_2 - 1) + delta_p(F). This is the second of the two external inputs taken as a hypothesis in Logical Intelligence's formalization of the disproof of Erdos's unit-distance conjecture (Hyp_ShafarevichRelationRankBound), and is not yet available in Mathlib. The statement rests on substantial trusted scaffolding (non-holes): the construction MaxUnramifiedProPGaloisGroup fixing Gal(F^{un,p}/F), and the rank definitions generatorRank, relationRank, H2Finite. A solver proves the inequality about these definitions. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../NumberTheory/ShafarevichRelationRank.lean | 157 ++++++++++++++++++ .../shafarevich_relation_rank_bound.toml | 9 + 2 files changed, 166 insertions(+) create mode 100644 LeanEval/NumberTheory/ShafarevichRelationRank.lean create mode 100644 manifests/problems/shafarevich_relation_rank_bound.toml diff --git a/LeanEval/NumberTheory/ShafarevichRelationRank.lean b/LeanEval/NumberTheory/ShafarevichRelationRank.lean new file mode 100644 index 0000000..2e785b0 --- /dev/null +++ b/LeanEval/NumberTheory/ShafarevichRelationRank.lean @@ -0,0 +1,157 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace NumberTheory + +/-! +# Shafarevich's relation-rank bound + +`shafarevich_relation_rank_bound` bounds the relation rank of the Galois group +`G = Gal(F^{un,p}/F)` of the maximal unramified pro-`p` extension of a number +field `F`, for odd `p`: + +``` +r(G) ≀ d(G) + (r₁ + rβ‚‚ - 1) + Ξ΄_p(F), +``` + +where `d(G)` is the generator rank, `r(G) = dim_{𝔽_p} HΒ²(G; 𝔽_p)` the relation +rank, `r₁`/`rβ‚‚` the number of real/complex places of `F`, and `Ξ΄_p(F) = 1` iff +`F` contains a primitive `p`-th root of unity. The bound also asserts that +`r(G)` is finite (`H2Finite`). + +References: D. C. Mayer, *New number fields with known p-class tower*, Theorem +5.1 with `S = βˆ…`; H. Koch, *Galois Theory of p-Extensions*, Theorems 11.5 and +11.8; Shafarevich (1963). + +This is the second of the two external inputs of Logical Intelligence's +formalization of the disproof of ErdΕ‘s's unit-distance conjecture +(, +`Hyp_ShafarevichRelationRankBound`), where it is taken as a hypothesis. It is +not currently available in Mathlib. + +## Trusted scaffolding + +Everything below the statement's data β€” `IsEverywhereUnramified`, +`maximalUnramifiedProPF`, `MaxUnramifiedProPGaloisGroup` (with its group and +topology instances), and the rank definitions `generatorRank`, `relationRank`, +`H2Finite` β€” are **trusted helper definitions** (they are not holes). They fix +the meaning of `Gal(F^{un,p}/F)`, `d(G)`, and `r(G)`, following +`ErdosUnitDistance.Defs.MaxUnramifiedProPGaloisGroup` and +`ErdosUnitDistance.Defs.ProPGroups`. A solver must prove the inequality *about +these definitions*; their correctness is part of the trusted statement. + +`maximalUnramifiedProPF F p` is the compositum, inside `AlgebraicClosure F`, of +all finite Galois everywhere-unramified intermediate extensions with `p`-group +Galois group β€” the usual construction of the maximal unramified pro-`p` +extension. +-/ + +open NumberField CategoryTheory + +/-- `M/F` is everywhere unramified: every nonzero prime of `π“ž F` has +ramification index `1` in `π“ž M`, and every real place of `F` stays real in +`M`. -/ +def IsEverywhereUnramified + (F M : Type) [Field F] [Field M] [NumberField F] [NumberField M] + [Algebra F M] : Prop := + (βˆ€ (𝔭 : Ideal (π“ž F)) (𝔓 : Ideal (π“ž M)), + 𝔭.IsPrime β†’ 𝔭 β‰  βŠ₯ β†’ + 𝔓 ∈ 𝔭.primesOver (π“ž M) β†’ + Ideal.ramificationIdx 𝔭 𝔓 = 1) ∧ + (βˆ€ w : NumberField.InfinitePlace F, w.IsReal β†’ + βˆ€ w' : NumberField.InfinitePlace M, + w'.comap (algebraMap F M) = w β†’ w'.IsReal) + +/-- The maximal unramified pro-`p` extension `F^{un,p}` of `F`: the compositum +of all finite-dimensional Galois everywhere-unramified intermediate extensions +whose Galois group is a `p`-group. -/ +noncomputable def maximalUnramifiedProPF + (F : Type) [Field F] [NumberField F] + (p : β„•) [Fact (Nat.Prime p)] : + IntermediateField F (AlgebraicClosure F) := + ⨆ (M : IntermediateField F (AlgebraicClosure F)) + (_ : FiniteDimensional F M) + (_ : IsGalois F M) + (_ : IsPGroup p (M ≃ₐ[F] M)) + (_ : NumberField M) + (_ : IsEverywhereUnramified F M), + M + +/-- `Gal(F^{un,p}/F)`, the Galois group of the maximal unramified pro-`p` +extension. -/ +noncomputable def MaxUnramifiedProPGaloisGroup + (F : Type) [Field F] [NumberField F] (p : β„•) [Fact (Nat.Prime p)] : + Type := + (maximalUnramifiedProPF F p) ≃ₐ[F] (maximalUnramifiedProPF F p) + +noncomputable instance MaxUnramifiedProPGaloisGroup.instGroup + (F : Type) [Field F] [NumberField F] (p : β„•) [Fact (Nat.Prime p)] : + Group (MaxUnramifiedProPGaloisGroup F p) := + inferInstanceAs (Group ((maximalUnramifiedProPF F p) ≃ₐ[F] _)) + +noncomputable instance MaxUnramifiedProPGaloisGroup.instTopologicalSpace + (F : Type) [Field F] [NumberField F] (p : β„•) [Fact (Nat.Prime p)] : + TopologicalSpace (MaxUnramifiedProPGaloisGroup F p) := + inferInstanceAs (TopologicalSpace ((maximalUnramifiedProPF F p) ≃ₐ[F] _)) + +instance MaxUnramifiedProPGaloisGroup.instIsTopologicalGroup + (F : Type) [Field F] [NumberField F] (p : β„•) [Fact (Nat.Prime p)] : + IsTopologicalGroup (MaxUnramifiedProPGaloisGroup F p) := + inferInstanceAs (IsTopologicalGroup ((maximalUnramifiedProPF F p) ≃ₐ[F] _)) + +/-- The generator rank `d(G)`: the minimal cardinality of a (topological) +generating set of `G`. -/ +noncomputable def generatorRank + (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : β„• := + sInf {k : β„• | βˆƒ S : Finset G, S.card = k ∧ + (Subgroup.closure (S : Set G)).topologicalClosure = ⊀} + +/-- The trivial `ZMod p`-representation of `G`. -/ +noncomputable def trivialZModpRep + (p : β„•) (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : + Action (TopModuleCat (ZMod p)) G := + Action.trivial G (TopModuleCat.of (ZMod p) (ZMod p)) + +/-- The relation rank `r(G) = dim_{𝔽_p} HΒ²(G; 𝔽_p)`, via degree-`2` continuous +cohomology with trivial `ZMod p` coefficients. -/ +noncomputable def relationRank + (p : β„•) [Fact p.Prime] (G : Type) + [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : β„• := + Module.finrank (ZMod p) + ((continuousCohomology (ZMod p) G 2).obj (trivialZModpRep p G)) + +/-- `HΒ²(G; 𝔽_p)` is finite-dimensional, i.e. the relation rank is finite. -/ +def H2Finite (p : β„•) [Fact p.Prime] (G : Type) + [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop := + FiniteDimensional (ZMod p) + ((continuousCohomology (ZMod p) G 2).obj (trivialZModpRep p G)) + +/-- **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. -/ +@[eval_problem] +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 + +end NumberTheory +end LeanEval diff --git a/manifests/problems/shafarevich_relation_rank_bound.toml b/manifests/problems/shafarevich_relation_rank_bound.toml new file mode 100644 index 0000000..174869f --- /dev/null +++ b/manifests/problems/shafarevich_relation_rank_bound.toml @@ -0,0 +1,9 @@ +id = "shafarevich_relation_rank_bound" +title = "Shafarevich's relation-rank bound" +test = false +module = "LeanEval.NumberTheory.ShafarevichRelationRank" +holes = ["shafarevich_relation_rank_bound"] +submitter = "Kim Morrison" +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)." +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)." +informal_solution = "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."