feat: add Shafarevich relation-rank bound eval problem#387
Open
kim-em wants to merge 1 commit into
Open
Conversation
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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds Shafarevich's relation-rank bound for the maximal unramified pro-
pextension of a number field, in the odd-p, empty-Sspecialization, as an eval problem: withG = Gal(F^{un,p}/F), the relation rankr(G) = dim_{𝔽_p} H²(G; 𝔽_p)is finite andr(G) ≤ d(G) + (r₁ + r₂ - 1) + δ_p(F), whered(G)is the generator rank,r₁/r₂count the real/complex places ofF, andδ_p(F) = 1iffFcontains a primitivep-th root of unity. This is the second of the two external inputs taken as a hypothesis in Logical Intelligence's formalization of the disproof of Erdős's unit-distance conjecture (erdos-unit-distance,Hyp_ShafarevichRelationRankBound), and is not yet in Mathlib.Unlike the companion Martinet and Golod–Shafarevich problems, this one rests on substantial trusted scaffolding (non-holes): the bespoke construction
MaxUnramifiedProPGaloisGroup(withIsEverywhereUnramifiedandmaximalUnramifiedProPF) fixingGal(F^{un,p}/F), plus the rank definitionsgeneratorRank,relationRank,H2Finite. A solver proves the inequality about these definitions, so their correctness is part of the trusted statement — the manifest discloses this, and notes that the source development's maximality/universal-property lemmas are not shipped here. The statement was checked for faithfulness against Mayer's Theorem 5.1 (S = ∅) and Koch 11.5/11.8 by an independent review (the correctedr₁+r₂-1unit-rank term and theδ_proot-of-unity correction are present); the module builds with only the expectedsorry.🤖 Prepared with Claude Code