ElevenTwelfths.Voronoi

ElevenTwelfths
Voronoi

import ElevenTwelfths.ThetaSums
import ElevenTwelfths.ActualFixedShellModels

Voronoi for the completed sums in the guide

This specializes the actual fixed-shell identity to conductor one and the public smooth dyadic weights. Auxiliary ray twists, cusp branches, common divisors and local masks are still present: suppressing them is appropriate in the introductory heuristic, but not in the exact theorem.

The left side uses the very same thetaSum as cube inversion. The right side is the upstream reflected fiber, not a newly postulated coefficient system.

namespace ElevenTwelfths.Thetanoncomputable sectionopen scoped BigOperators Classicalopen OAI OAI.ActualEisensteinCubicopen OAI.CompletedGauss hiding Oopen OAI.CanonicalRowCompletionopen OAI.CanonicalRowCompletion.ActualFiberopen OAI.CanonicalCoefficientClassopen OAI.CubicEisenstein hiding O

local instance : Fintype (O ⧸ Ideal.span {reflectionConductor 1}) := by⊢ Fintype (O ⧸ Ideal.span {reflectionConductor 1})
  let : Finite (O ⧸ Ideal.span {reflectionConductor 1}) :=
    OAI.ConcreteTraceCRT.finite_quotient_span (reflectionConductor_ne_zero 1 (by⊢ 1 ≠ 0 norm_numAll goals completed! 🐙))this:Finite (O ⧸ Ideal.span {reflectionConductor 1}) := ···⊢ Fintype (O ⧸ Ideal.span {reflectionConductor 1})
  exact Fintype.ofFinite _All goals completed! 🐙

variable (m : O) (hm : m ≠ 0)
    (rows : Finset (Ideal O)) (R F : Ideal O) (hR : R ≠ 0)
    (hF : Squarefree F) (hrows : ∀ I ∈ rows, I ≠ 0) (v : Oˣ)

The exact cubic Voronoi identity, specialized to zeta and [1/2,1]. Its row-dependent source twist and reflected cusp fiber remain explicit.

theorem theta_voronoi
    (Ψ : O →* ℂ) (hperiod : FactorsModulo (fixedBaseConductor 1) Ψ)
    (hΨ : ∀ n, ‖Ψ n‖ ≤ 1)
    (L : ℝ) (hshell : ∀ I ∈ rows,
      L / 2 ≤ (Ideal.absNorm I : ℝ) ∧ (Ideal.absNorm I : ℝ) ≤ L)
    (ℓ : RowIndex 1 m rows R F)
    (W : SmoothDyadicWeight ℂ) (X : ℝ) (hX : 0 < X) :
    thetaSum
        (rowTwist Ψ (maskElement 1 m)
          (OAI.ConcretePrimeRowBridge.idealGenerator F)
          (v.val * OAI.ConcretePrimeRowBridge.idealGenerator ℓ.val)) W X =
      ActualFixedShellModels.actualReflectionScale *
        (reflectedFiber 1 (bym:Ohm:m ≠ 0rows:Finset (Ideal O)R:Ideal OF:Ideal OhR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:OˣΨ:O →* ℂhperiod:FactorsModulo (fixedBaseConductor 1) ΨhΨ:∀ (n : O), ‖Ψ n‖ ≤ 1L:ℝhshell:∀ I ∈ rows, L / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ Lℓ:↥(RowIndex 1 m rows R F)W:SmoothDyadicWeight ℂX:ℝhX:0 < X⊢ 1 ≠ 0 norm_numAll goals completed! 🐙) m hm rows R F hR hF hrows v L Ψ hΨ).idealValue
          W X 1 completedRamifiedStep (rowResidualPart ℓ.val (maskIdeal 1 m F)) := bym:Ohm:m ≠ 0rows:Finset (Ideal O)R:Ideal OF:Ideal OhR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:OˣΨ:O →* ℂhperiod:FactorsModulo (fixedBaseConductor 1) ΨhΨ:∀ (n : O), ‖Ψ n‖ ≤ 1L:ℝhshell:∀ I ∈ rows, L / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ Lℓ:↥(RowIndex 1 m rows R F)W:SmoothDyadicWeight ℂX:ℝhX:0 < X⊢ thetaSum
    (rowTwist Ψ (maskElement 1 m) (ConcretePrimeRowBridge.idealGenerator F)
      (↑v * ConcretePrimeRowBridge.idealGenerator ↑ℓ))
    W X =
  ActualFixedShellModels.actualReflectionScale *
    (reflectedFiber 1 ⋯ m hm rows R F hR hF hrows v L Ψ hΨ).idealValue W.toFun X 1 completedRamifiedStep
      (rowResidualPart (↑ℓ) (maskIdeal 1 m F))
  exact ActualFixedShellModels.completedT_eq_reflectedFiber_idealValue_local
    1 (bym:Ohm:m ≠ 0rows:Finset (Ideal O)R:Ideal OF:Ideal OhR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:OˣΨ:O →* ℂhperiod:FactorsModulo (fixedBaseConductor 1) ΨhΨ:∀ (n : O), ‖Ψ n‖ ≤ 1L:ℝhshell:∀ I ∈ rows, L / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ Lℓ:↥(RowIndex 1 m rows R F)W:SmoothDyadicWeight ℂX:ℝhX:0 < X⊢ 1 ≠ 0 norm_numAll goals completed! 🐙) m hm rows R F hR hF hrows v Ψ hperiod hΨ L hshell ℓ
    W (1 / 2) 1 (bym:Ohm:m ≠ 0rows:Finset (Ideal O)R:Ideal OF:Ideal OhR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:OˣΨ:O →* ℂhperiod:FactorsModulo (fixedBaseConductor 1) ΨhΨ:∀ (n : O), ‖Ψ n‖ ≤ 1L:ℝhshell:∀ I ∈ rows, L / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ Lℓ:↥(RowIndex 1 m rows R F)W:SmoothDyadicWeight ℂX:ℝhX:0 < X⊢ 0 < 1 / 2 norm_numAll goals completed! 🐙) W.support_subset W.contDiff X hX

endend ElevenTwelfths.Theta