1. ElevenTwelfths
  2. ConcreteFamily
import ElevenTwelfths.EisensteinFamily import OAI.NumberTheory.DirichletL.Arithmetic.IdealMobius import OAI.NumberTheory.DirichletL.MeanSquare.OutsideIdeals import OAI.NumberTheory.DirichletL.GaussSum.ReflectionBrackets

The concrete Eisenstein family used by the proof

The readable sum is indexed by the primary generator of each admissible ideal. Internally, the OpenAI estimates are stated for ideals. This file makes the conversion explicit and proves that the two finite sums agree.

The column ball and row ball are deliberately different, just as they are in the OpenAI formalization: columns are admissible primary generators, whereas Poisson summation runs over every Eisenstein integer in a norm ball.

namespace ElevenTwelfthsnoncomputable sectionopen scoped BigOperators Classicalopen OAIopen OAI.ActualEisensteinCubicopen OAI.CompletedGaussopen OAI.ConcretePrimeRowBridge hiding Oopen OAI.InitialMeanSquareopen OAI.PrimaryIdealUnitReindexopen OAI.ShortDraftHeckeBridge hiding O

The exact finite row ball. We insert zero because the OpenAI disk omits it; its summand vanishes under a cutoff supported in [1/2,1].

noncomputable def exactRowBall (H : β„•) : Finset π’ͺ := insert 0 (rowNormDisk H)theorem mem_exactRowBall {H : β„•} {h : π’ͺ} : h ∈ exactRowBall H ↔ 𝒩 h ≀ H := H:β„•h:π’ͺ⊒ h ∈ exactRowBall H ↔ 𝒩 h ≀ H classical H:β„•h:π’ͺ⊒ h = 0 ∨ h ∈ rowNormDisk H ↔ 𝒩 h ≀ H H:β„•h:π’ͺ⊒ h = 0 ∨ h ∈ rowNormDisk H β†’ 𝒩 h ≀ HH:β„•h:π’ͺ⊒ 𝒩 h ≀ H β†’ h = 0 ∨ h ∈ rowNormDisk H H:β„•h:π’ͺ⊒ h = 0 ∨ h ∈ rowNormDisk H β†’ 𝒩 h ≀ H H:β„•βŠ’ 𝒩 0 ≀ HH:β„•h:π’ͺhu:h ∈ rowNormDisk H⊒ 𝒩 h ≀ H H:β„•βŠ’ 𝒩 0 ≀ H All goals completed! πŸ™ H:β„•h:π’ͺhu:h ∈ rowNormDisk H⊒ 𝒩 h ≀ H All goals completed! πŸ™ H:β„•h:π’ͺ⊒ 𝒩 h ≀ H β†’ h = 0 ∨ h ∈ rowNormDisk H H:β„•h:π’ͺhu:𝒩 h ≀ H⊒ h = 0 ∨ h ∈ rowNormDisk H H:β„•h:π’ͺhu:𝒩 h ≀ Hhzero:h = 0⊒ h = 0 ∨ h ∈ rowNormDisk HH:β„•h:π’ͺhu:𝒩 h ≀ Hhzero:Β¬h = 0⊒ h = 0 ∨ h ∈ rowNormDisk H H:β„•h:π’ͺhu:𝒩 h ≀ Hhzero:h = 0⊒ h = 0 ∨ h ∈ rowNormDisk H All goals completed! πŸ™ H:β„•h:π’ͺhu:𝒩 h ≀ Hhzero:Β¬h = 0⊒ h = 0 ∨ h ∈ rowNormDisk H H:β„•h:π’ͺhu:𝒩 h ≀ Hhzero:Β¬h = 0⊒ h ∈ rowNormDisk H H:β„•h:π’ͺhu:𝒩 h ≀ Hhzero:Β¬h = 0⊒ 0 < Ideal.absNorm (Ideal.span {h}) ∧ Ideal.absNorm (Ideal.span {h}) ≀ H All goals completed! πŸ™

Admissible columns of norm at most X, represented by their canonical primary Eisenstein generators.

noncomputable def outsidePrimaryBall (S : Finset (Ideal π’ͺ)) (X : β„•) : Finset π’ͺ := (outsideIdealsUpTo S X).image primaryGeneratorprivate theorem outside_primaryGenerator_ne_zero (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (X : β„•) {I : Ideal π’ͺ} (hI : I ∈ outsideIdealsUpTo S X) : primaryGenerator I β‰  0 := primaryGenerator_ne_zero_of_good_factors I (outsideIdealsUpTo_ne_bot S X I hI) (outside_good S X hbad I hI)theorem outsidePrimaryBall_primary (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (X : β„•) {n : π’ͺ} (hn : n ∈ outsidePrimaryBall S X) : primary n := S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SX:β„•n:π’ͺhn:n ∈ outsidePrimaryBall S X⊒ primary n classical S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhn:primaryGenerator I ∈ outsidePrimaryBall S X⊒ primary (primaryGenerator I) S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhn:primaryGenerator I ∈ outsidePrimaryBall S Xhgen:primaryGenerator I β‰  0⊒ primary (primaryGenerator I) S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhn:primaryGenerator I ∈ outsidePrimaryBall S Xhgen:primaryGenerator I β‰  0⊒ 𝔓 ^ 2 ∣ primaryGenerator I - 1 All goals completed! πŸ™

The actual product of local sextic characters attached to the column generated by n.

noncomputable def outsideSexticTwist (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (X : β„•) (h n : π’ͺ) : β„‚ := idealSexticRow (outsideIdealsUpTo S X) (outsideIdealsUpTo_ne_bot S X) (outside_good S X hbad) (Ideal.span {n}) h

The concrete public M_h(X). Its summand visibly contains primaryness, ideal MΓΆbius, the sextic twist, and the [1/2,1] smooth cutoff.

noncomputable def outsideM (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (W : SmoothDyadicWeight β„‚) (h : π’ͺ) (X : β„•) : β„‚ := βˆ‘ n ∈ outsidePrimaryBall S X, if primary n then (ΞΌ_K n : β„‚) * outsideSexticTwist S hbad X h n * W ((𝒩 n : ℝ) / (X : ℝ)) else 0theorem outsideM_eq_eisensteinM (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (W : SmoothDyadicWeight β„‚) (h : π’ͺ) (X : β„•) : outsideM S hbad W h X = eisensteinM (outsidePrimaryBall S) (outsideSexticTwist S hbad X) W h X := rfl

The readable primary-element sum is exactly the ideal row consumed by Poisson summation and the mean-square theorem.

theorem outsideM_eq_idealRowSum (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (W : SmoothDyadicWeight β„‚) (h : π’ͺ) (X : β„•) : outsideM S hbad W h X = idealRowSum (outsideIdealsUpTo S X) (outsideIdealsUpTo_ne_bot S X) (outside_good S X hbad) (1 : DirichletCharacter β„‚ 1) (fun n ↦ W ((n : ℝ) / (X : ℝ))) h := S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ outsideM S hbad W h X = idealRowSum (outsideIdealsUpTo S X) β‹― β‹― 1 (fun n => W.toFun (↑n / ↑X)) h classical S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ (βˆ‘ n ∈ Finset.image primaryGenerator (outsideIdealsUpTo S X), if primary n then ↑(ΞΌ_K n) * outsideSexticTwist S hbad X h n * W.toFun (↑(𝒩 n) / ↑X) else 0) = βˆ‘ I ∈ outsideIdealsUpTo S X, baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ (βˆ‘ x ∈ outsideIdealsUpTo S X, if primary (primaryGenerator x) then ↑(ΞΌ_K (primaryGenerator x)) * outsideSexticTwist S hbad X h (primaryGenerator x) * W.toFun (↑(𝒩 (primaryGenerator x)) / ↑X) else 0) = βˆ‘ I ∈ outsideIdealsUpTo S X, baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I hS:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ Set.InjOn primaryGenerator ↑(outsideIdealsUpTo S X) S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ (βˆ‘ x ∈ outsideIdealsUpTo S X, if primary (primaryGenerator x) then ↑(ΞΌ_K (primaryGenerator x)) * outsideSexticTwist S hbad X h (primaryGenerator x) * W.toFun (↑(𝒩 (primaryGenerator x)) / ↑X) else 0) = βˆ‘ I ∈ outsideIdealsUpTo S X, baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ βˆ€ x ∈ outsideIdealsUpTo S X, (if primary (primaryGenerator x) then ↑(ΞΌ_K (primaryGenerator x)) * outsideSexticTwist S hbad X h (primaryGenerator x) * W.toFun (↑(𝒩 (primaryGenerator x)) / ↑X) else 0) = baseChangeWeight 1 x * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm x) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― x h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S X⊒ (if primary (primaryGenerator I) then ↑(ΞΌ_K (primaryGenerator I)) * outsideSexticTwist S hbad X h (primaryGenerator I) * W.toFun (↑(𝒩 (primaryGenerator I)) / ↑X) else 0) = baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0⊒ (if primary (primaryGenerator I) then ↑(ΞΌ_K (primaryGenerator I)) * outsideSexticTwist S hbad X h (primaryGenerator I) * W.toFun (↑(𝒩 (primaryGenerator I)) / ↑X) else 0) = baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0hspan:Ideal.span {primaryGenerator I} = I⊒ (if primary (primaryGenerator I) then ↑(ΞΌ_K (primaryGenerator I)) * outsideSexticTwist S hbad X h (primaryGenerator I) * W.toFun (↑(𝒩 (primaryGenerator I)) / ↑X) else 0) = baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0hspan:Ideal.span {primaryGenerator I} = Ihprimary:primary (primaryGenerator I)⊒ (if primary (primaryGenerator I) then ↑(ΞΌ_K (primaryGenerator I)) * outsideSexticTwist S hbad X h (primaryGenerator I) * W.toFun (↑(𝒩 (primaryGenerator I)) / ↑X) else 0) = baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0hspan:Ideal.span {primaryGenerator I} = Ihprimary:primary (primaryGenerator I)⊒ ↑(ΞΌ_K (primaryGenerator I)) * outsideSexticTwist S hbad X h (primaryGenerator I) * W.toFun (↑(𝒩 (primaryGenerator I)) / ↑X) = baseChangeWeight 1 I * (fun n => W.toFun (↑n / ↑X)) (Ideal.absNorm I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0hspan:Ideal.span {primaryGenerator I} = Ihprimary:primary (primaryGenerator I)⊒ ↑(UniqueFactorizationMonoid.moebius I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h * W.toFun (↑(Ideal.absNorm I) / ↑X) = baseChangeWeight 1 I * W.toFun (↑(Ideal.absNorm I) / ↑X) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0hspan:Ideal.span {primaryGenerator I} = Ihprimary:primary (primaryGenerator I)hchar:1 ↑(Ideal.absNorm I) = 1⊒ ↑(UniqueFactorizationMonoid.moebius I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h * W.toFun (↑(Ideal.absNorm I) / ↑X) = baseChangeWeight 1 I * W.toFun (↑(Ideal.absNorm I) / ↑X) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ outsideIdealsUpTo S Xhgen:primaryGenerator I β‰  0hspan:Ideal.span {primaryGenerator I} = Ihprimary:primary (primaryGenerator I)hchar:1 ↑(Ideal.absNorm I) = 1⊒ ↑(UniqueFactorizationMonoid.moebius I) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h * W.toFun (↑(Ideal.absNorm I) / ↑X) = ↑(UniqueFactorizationMonoid.moebius I) * W.toFun (↑(Ideal.absNorm I) / ↑X) * idealSexticRow (outsideIdealsUpTo S X) β‹― β‹― I h All goals completed! πŸ™ S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•βŠ’ Set.InjOn primaryGenerator ↑(outsideIdealsUpTo S X) S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ ↑(outsideIdealsUpTo S X)J:Ideal CompletedGauss.OhJ:J ∈ ↑(outsideIdealsUpTo S X)hIJ:primaryGenerator I = primaryGenerator J⊒ I = J S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ ↑(outsideIdealsUpTo S X)J:Ideal CompletedGauss.OhJ:J ∈ ↑(outsideIdealsUpTo S X)hIJ:primaryGenerator I = primaryGenerator JhIgen:primaryGenerator I β‰  0⊒ I = J S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚h:π’ͺX:β„•I:Ideal CompletedGauss.OhI:I ∈ ↑(outsideIdealsUpTo S X)J:Ideal CompletedGauss.OhJ:J ∈ ↑(outsideIdealsUpTo S X)hIJ:primaryGenerator I = primaryGenerator JhIgen:primaryGenerator I β‰  0hJgen:primaryGenerator J β‰  0⊒ I = J All goals completed! πŸ™

The finite, smoothly weighted mean square attached to outsideM.

noncomputable def outsideS (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (W : SmoothDyadicWeight β„‚) (V : SmoothDyadicCutoff) (X H : β„•) : ℝ := βˆ‘ h ∈ exactRowBall H, V ((𝒩 h : ℝ) / (H : ℝ)) * β€–outsideM S hbad W h Xβ€– ^ 2

Immediately before Poisson summation, the finite row sum becomes a whole-lattice tsum.

theorem outsideS_eq_tsum (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (W : SmoothDyadicWeight β„‚) (V : SmoothDyadicCutoff) (X H : β„•) : outsideS S hbad W V X H = βˆ‘' h : π’ͺ, V ((𝒩 h : ℝ) / (H : ℝ)) * β€–outsideM S hbad W h Xβ€– ^ 2 := S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•βŠ’ outsideS S hbad W V X H = βˆ‘' (h : π’ͺ), V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 classical S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•βŠ’ βˆ‘ h ∈ exactRowBall H, V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = βˆ‘' (h : π’ͺ), V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•βŠ’ βˆ€ b βˆ‰ exactRowBall H, V.toFun (↑(𝒩 b) / ↑H) * β€–outsideM S hbad W b Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall H⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 h⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:H = 0⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:Β¬H = 0⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:H = 0⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:H = 0hV:V.toFun 0 = 0⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 All goals completed! πŸ™ S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:Β¬H = 0⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:Β¬H = 0hHpos:0 < ↑H⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺhu:h βˆ‰ exactRowBall Hhnorm:H < 𝒩 hhH:Β¬H = 0hHpos:0 < ↑Hhratio:1 < ↑(𝒩 h) / ↑H⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = 0 All goals completed! πŸ™

The same conversion, now with the ideal row exposed in exactly the form used by the OpenAI Poisson and mean-square modules.

theorem outsideS_eq_idealRowSum_tsum (S : Finset (Ideal π’ͺ)) (hbad : OAI.CanonicalQuadraticSieve.fixedBadPrimes βŠ† S) (W : SmoothDyadicWeight β„‚) (V : SmoothDyadicCutoff) (X H : β„•) : outsideS S hbad W V X H = βˆ‘' h : π’ͺ, V ((𝒩 h : ℝ) / (H : ℝ)) * β€–idealRowSum (outsideIdealsUpTo S X) (outsideIdealsUpTo_ne_bot S X) (outside_good S X hbad) (1 : DirichletCharacter β„‚ 1) (fun n ↦ W ((n : ℝ) / (X : ℝ))) hβ€– ^ 2 := S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•βŠ’ outsideS S hbad W V X H = βˆ‘' (h : π’ͺ), V.toFun (↑(𝒩 h) / ↑H) * β€–idealRowSum (outsideIdealsUpTo S X) β‹― β‹― 1 (fun n => W.toFun (↑n / ↑X)) hβ€– ^ 2 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•βŠ’ βˆ‘' (h : π’ͺ), V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = βˆ‘' (h : π’ͺ), V.toFun (↑(𝒩 h) / ↑H) * β€–idealRowSum (outsideIdealsUpTo S X) β‹― β‹― 1 (fun n => W.toFun (↑n / ↑X)) hβ€– ^ 2 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•βŠ’ βˆ€ (b : π’ͺ), V.toFun (↑(𝒩 b) / ↑H) * β€–outsideM S hbad W b Xβ€– ^ 2 = V.toFun (↑(𝒩 b) / ↑H) * β€–idealRowSum (outsideIdealsUpTo S X) β‹― β‹― 1 (fun n => W.toFun (↑n / ↑X)) bβ€– ^ 2 S:Finset (Ideal π’ͺ)hbad:CanonicalQuadraticSieve.fixedBadPrimes βŠ† SW:SmoothDyadicWeight β„‚V:SmoothDyadicCutoffX:β„•H:β„•h:π’ͺ⊒ V.toFun (↑(𝒩 h) / ↑H) * β€–outsideM S hbad W h Xβ€– ^ 2 = V.toFun (↑(𝒩 h) / ↑H) * β€–idealRowSum (outsideIdealsUpTo S X) β‹― β‹― 1 (fun n => W.toFun (↑n / ↑X)) hβ€– ^ 2 All goals completed! πŸ™endend ElevenTwelfths