Primes with deep Frobenius lifts

Mathematical statement

Put $S=\{3,5,7,11,13,17\}$ and $G=\operatorname{Gal}(M_{2,S}/\mathbb Q)$, where $M_{2,S}$ is the maximal totally real pro-$2$ extension of $\mathbb Q$ unramified at finite primes outside $S$.

There exist a five-generator minimal presentation $P:F_5\twoheadrightarrow G$ with at most six relators, primes $q_n$ and elements $f_n\in F_5$ such that $$q_n>n,\quad q_n\notin S,\quad q_n\equiv1\pmod4,\quad P(f_n)=\operatorname{Frob}_{q_n},\quad f_n\in D_{n+5}(F_5).$$ Here $D_k$ is the pro-$2$ Zassenhaus filtration.

The Frobenius elements are the arithmetic elements supplied by the source’s decomposition-group construction. The theorem chooses a presentation together with the sequence; the depth condition is imposed on lifts in that very free source.

Lean code

`ClassFieldTower.Sawin.exists_sawinDeepFrobenius_sequence`

Published library source ↗Same source in NYLL ↗

theorem exists_sawinDeepFrobenius_sequence :
    ∃ sourceData : FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{0, 0}
      (FiniteGroupClass.pGroup 2),
      ∃ r : ℕ, ∃ P : FiniteProPPresentation 2 5 r sourceData
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport),
        P.IsMinimal ∧ r ≤ 6 ∧
        ∃ primes : ℕ → Nat.Primes, ∃ f : ℕ → sourceData.carrier, ∀ n : ℕ,
          n < (primes n).val ∧
          (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n) ∉
            sawinRationalPrimeSupport ∧
          (primes n).val % 4 = 1 ∧
          P.quotient (f n) = maximalRealProPArithmeticFrobenius 2 sawinRationalPrimeSupport
            ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n)) ∧
          ZassenhausDepthAtLeast 2 (sawinFrobeniusDepth n) (f n)

In-scope Lean context

open scoped NumberField

open NumberField IsDedekindDomain

namespace ClassFieldTower.Sawin

open ProCGroups ProCGroups.Presentations ClassFieldTower.ProP

private local instance frobeniusSequencePrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩

private local instance frobeniusSequenceIsGalois :
    IsGalois ℚ (maximalRealProPOutside 2 sawinRationalPrimeSupport) :=
  maximalRealProPOutside_isGalois 2 sawinRationalPrimeSupport

Full declaration and proof

/-- The same actual minimal presentation admits a sequence of deep source
lifts of arithmetic Frobenius at primes escaping every initial interval. -/
theorem exists_sawinDeepFrobenius_sequence :
    ∃ sourceData : FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{0, 0}
      (FiniteGroupClass.pGroup 2),
      ∃ r : ℕ, ∃ P : FiniteProPPresentation 2 5 r sourceData
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport),
        P.IsMinimal ∧ r ≤ 6 ∧
        ∃ primes : ℕ → Nat.Primes, ∃ f : ℕ → sourceData.carrier, ∀ n : ℕ,
          n < (primes n).val ∧
          (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n) ∉
            sawinRationalPrimeSupport ∧
          (primes n).val % 4 = 1 ∧
          P.quotient (f n) = maximalRealProPArithmeticFrobenius 2 sawinRationalPrimeSupport
            ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n)) ∧
          ZassenhausDepthAtLeast 2 (sawinFrobeniusDepth n) (f n) := by
  classical
  obtain ⟨sourceData, r, P, hP, hr⟩ := exists_sawinInitialProTwo_minimalPresentation
  choose primes hbad hsupport hmod f hf hdepth using fun n : ℕ ↦
    exists_sawinPrime_with_deep_frobenius_lift
      P.source_topologicallyFinitelyGenerated P.quotient P.quotient_surjective
      (sawinFrobeniusDepth n) (Finset.range (n + 1))
  refine ⟨sourceData, r, P, hP, hr, primes, f, fun n ↦ ?_⟩
  refine ⟨?_, hsupport n, hmod n, hf n, hdepth n⟩
  have hnot : ¬(primes n).val < n + 1 := fun h ↦ hbad n (Finset.mem_range.mpr h)
  omega

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood. Remarks on the disproof of the unit distance conjecture. 2026. Proposition 2.3 states the bounded-root-discriminant totally real tower with infinitely many completely split primes congruent to one modulo four.
Farshid Hajir, Christian Maire, and Ravi Ramakrishna. Cutting towers of number fields. 2019. Cited as the arXiv preprint; develops cutting methods with refined Golod–Shafarevich estimates.