import PaperX.NormResidueGeneratorAttachment import PaperX.NormResidueGeneratorSum import PaperX.NormResidueUnitCounting import PaperX.IdealNormCharacterBound /-! Arithmetic norm-character cancellation from a residue-unit witness. The cone estimate, both sign means, and the exact generator/ideal comparison are proved dependencies; the displayed arithmetic hypotheses remain supplied. -/ set_option autoImplicit false noncomputable section namespace PaperX.NormResidueLattice open Ideal NumberField open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.NormResidue open PaperX.IdealNormWeighted PaperX.IdealResidueUnitAction open scoped nonZeroDivisors Classical Pointwise Real variable (K : Type*) [Field K] [NumberField K] /-- The finite residue computation equals the actual bounded generator sum. -/ theorem normWeightedCount_eq_boundedGeneratorSum (M J : (Ideal (π“ž K))⁰) (m : β„•) (hM : (M : Ideal (π“ž K)) ≀ modulusIdeal (π“ž K) m) [Fintype (IdealResidues K M J)] (Ο‡ : ZMod m β†’ β„‚) {t : ℝ} (ht : 0 < t) : normWeightedCount K M J m hM Ο‡ t = boundedGeneratorSum K J (fun n => Ο‡ (n : ZMod m)) (t ^ Module.finrank β„š K) := by rw [normWeightedCount_eq_generatorPointSum K M J m hM Ο‡ ht] exact latticeGeneratorSum_eq_boundedGeneratorSum K J (fun n => Ο‡ (n : ZMod m)) ht /-- The canonical modulus count is independent of its chosen finite enumeration. -/ theorem modulusNormWeightedCount_eq_boundedGeneratorSum (J : (Ideal (π“ž K))⁰) (m : β„•) (hm : m β‰  0) (Ο‡ : ZMod m β†’ β„‚) {t : ℝ} (ht : 0 < t) : modulusNormWeightedCount K J m hm Ο‡ t = boundedGeneratorSum K J (fun n => Ο‡ (n : ZMod m)) (t ^ Module.finrank β„š K) := by let := Fintype.ofFinite (IdealResidues K (modulusTimesIdeal K J m hm) J) unfold modulusNormWeightedCount exact normWeightedCount_eq_boundedGeneratorSum K _ J m _ Ο‡ ht /-- The unit witness gives a power-saving estimate on actual algebraic generators, with all finite-mean and geometric estimates discharged. -/ theorem exists_boundedGeneratorSum_bound_of_unit (J : (Ideal (π“ž K))⁰) (m : β„•) (hm : m β‰  0) (Ο‡ : ZMod m β†’* β„‚) (u : (π“ž K β§Έ modulusIdeal (π“ž K) m)Λ£) (hu : Ο‡ (integerQuotientNorm K m (u : π“ž K β§Έ modulusIdeal (π“ž K) m)) β‰  1) : βˆƒ B : ℝ, 0 ≀ B ∧ βˆ€ Y : ℝ, 1 ≀ Y β†’ β€–boundedGeneratorSum K J (fun n => Ο‡ (n : ZMod m)) Yβ€– ≀ B * (Y ^ countExponent K + 1) := by obtain ⟨B, hB0, hB⟩ := exists_modulusNormWeightedCount_bound K J m hm Ο‡ u hu refine ⟨B, hB0, fun Y hY => ?_⟩ have hY0 : 0 < Y := lt_of_lt_of_le zero_lt_one hY have hd : Module.finrank β„š K β‰  0 := (Module.finrank_pos (R := β„š) (M := K)).ne' have ht : 1 ≀ Y ^ (Module.finrank β„š K : ℝ)⁻¹ := Real.one_le_rpow hY (by positivity) have H := hB (Y ^ (Module.finrank β„š K : ℝ)⁻¹) ht rw [modulusNormWeightedCount_eq_boundedGeneratorSum K J m hm Ο‡ (Real.rpow_pos_of_pos hY0 _), Real.rpow_inv_natCast_pow hY0.le hd, root_boundary_power K Y hY0.le] at H exact H /-- Actual ideal norm-character sums in a class have power-saving cancellation under a residue-unit witness and nonvanishing on the inverse-class representative. -/ theorem exists_classNormSum_bound_of_unit {C : ClassGroup (π“ž K)} {J : (Ideal (π“ž K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹) (m : β„•) (hm : m β‰  0) (Ο‡ : ZMod m β†’*β‚€ β„‚) (u : (π“ž K β§Έ modulusIdeal (π“ž K) m)Λ£) (hu : Ο‡ (integerQuotientNorm K m (u : π“ž K β§Έ modulusIdeal (π“ž K) m)) β‰  1) (hΟ‡J : Ο‡ (absNorm (J : Ideal (π“ž K)) : ZMod m) β‰  0) : βˆƒ B : ℝ, 0 ≀ B ∧ βˆ€ X : ℝ, 1 ≀ X β†’ β€–classNormSum K C (fun n => Ο‡ (n : ZMod m)) Xβ€– ≀ B * X ^ countExponent K := exists_classNormSum_bound_of_generator_bound K hJ m Ο‡ hΟ‡J (exists_boundedGeneratorSum_bound_of_unit K J m hm Ο‡.toMonoidHom u hu) end PaperX.NormResidueLattice