Paper X: Universal Residual Seeds and Conditional Occupied-System Completion

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \clearpage
2 \section{Retained residue-counting continuation}
3 \label{sec:historical-residue-continuation}
4 The following continuation is retained at its original checkpoint scope. Its 17/20 status and the statement that Claims 9.1, 9.2 and 11.1 remain partial are historical descriptions of that checkpoint. Section~\ref{sec:conditional-final} supplies the later amended conditional completion. The counting formulas, hypotheses and remaining norm-image obligations below are preserved.
5 \providecommand{\OO}{\mathcal O}
6 \providecommand{\ZZ}{\mathbb Z}
7 \providecommand{\RR}{\mathbb R}
8 \providecommand{\CC}{\mathbb C}
9 \providecommand{\NN}{\mathbb N}
10 \providecommand{\Cl}{\operatorname{Cl}}
11 \providecommand{\Nm}{\operatorname N}
12 \providecommand{\vol}{\operatorname{vol}}
13 \providecommand{\covol}{\operatorname{covol}}
14 \providecommand{\absn}[1]{\lvert #1\rvert}
15 
16 
17 
18 
19 \paragraph{Scope and notation.}
20 Let $K$ be a number field of degree $d\geq1$, with ring of integers
21 $\OO=\OO_K$. Write $\Nm I=\#(\OO/I)$ for the absolute norm of a nonzero
22 integral ideal and $n(x)=\Nm_{K/\mathbb Q}(x)\in\ZZ$ for $x\in\OO$.
23 Thus $\Nm(x)=\absn{n(x)}$. Let $\iota$ be the mixed embedding in its
24 Euclidean coordinates, $L(J)=\iota(J)$, and $D$ the actual unit-norm
25 fundamental cone used in the preceding counting block. Its norm function
26 scales by $t^d$ under a positive real dilation $t$.
27 The full-paper ledger remains \textbf{17 checked claims and 3 partial claims}.
28 
29 \paragraph{Actual additive residues.}
30 Fix nonzero integral ideals $M\subseteq J$, and put $q=[J:M]=\#(J/M)$.
31 The formal quotient of ideal lattices is identified with the additive
32 congruence relation $x-a\in M$ on actual elements of $J$. In particular,
33 the residue label is not an independent parameter attached to a count.
34 
Statement: Proposition: prop:residue-count35 \begin{proposition}\label{prop:residue-count}
36 There is a constant $B\geq0$, depending on $K,M,J$, such that, for every
37 $a\in J/M$ and every real $t\geq1$,
38 \[
39  \left|\#\{x\in J:x\bmod M=a,\ \iota(x)\in tD\}
40  -\frac{\vol(D)}{q\,\covol(L(J))}t^d\right|
41  \leq B(t^{d-1}+1).
42 \]
43 The same constant works for all residues $a$.
44 \end{proposition}
45 
46 The estimate is proved from the actual boundary charts and the fixed-lattice
47 discrepancy theorem. The index factor comes from the covolume identity
48 $\covol(L(M))=q\,\covol(L(J))$.
49 For a complex weight $w:J/M\to\CC$, summing the estimates gives the leading
50 term
51 \[
52  \frac{\vol(D)t^d}{q\,\covol(L(J))}\sum_{a\in J/M}w(a),
53 \]
54 with error at most $B\sum_a\absn{w(a)}(t^{d-1}+1)$.
55 If the finite sum of weights is zero, only that error remains.
56 Writing $Y=t^d$ gives an error $O(Y^{1-1/d}+1)$ for the actual norm threshold.
57 These assertions include $d=1$.
58 
59 \smallskip
60 \noindent\emph{Lean attachment:}
61 \nolinkurl{ResidueLatticeIdeal}, \nolinkurl{ResidueLatticeIdealPoints},
62 \nolinkurl{ResidueLatticeIdealWeights}, and \nolinkurl{ResidueLatticeNormCounts}.
63 
64 \newpage
65 \paragraph{The residue norm and its sign.}
66 For $m\in\NN$, reducing the multiplication matrices of $\OO$ modulo $m$
67 and taking their determinants constructs a monoid homomorphism
68 \[
69  \overline n:\OO/m\OO\longrightarrow\ZZ/m\ZZ,
70  \qquad \overline n([x])=n(x)\bmod m.
71 \]
72 The construction is proved independent of the integral basis.
73 For $m\ne0$, its source is finite of cardinality $m^d$.
74 Consequently $x-y\in m\OO$ implies $n(x)\equiv n(y)\pmod m$.
75 No surjectivity of $\overline n$ is asserted.
76 
77 The relation to the geometric sign is also proved. If $\sigma$ ranges over
78 real embeddings and $\tau$ over one embedding from each complex pair, then
79 \[
80  n(x)=\prod_{\sigma}\sigma(x)\prod_{\tau}\absn{\tau(x)}^2.
81 \]
82 For $x\ne0$, the second factor is positive. Thus the sign of $n(x)$ is
83 exactly the sign of the real-coordinate product. Cutting $D$ into its
84 positive and negative portions $D_+,D_-$ adds no boundary outside the
85 existing frontier, and both portions retain the proved boundary atlas.
86 They are disjoint and their union is $D$.
87 
88 For $\varepsilon\in\{1,-1\}$ define
89 $\overline n_{\varepsilon}(a)=\varepsilon\overline n(a)$.
90 On the corresponding sign portion,
91 \[
92  \Nm(x)\bmod m=\overline n_{\varepsilon}([x]).
93 \]
94 The sign cannot be dropped: $-1\equiv2\pmod3$, whereas
95 $\Nm(-1)=1$ and $\Nm(2)=2$ for principal ideals of $\ZZ$.
96 
97 \paragraph{The exact ideal filter.}
98 Suppose $IJ=(x)$, $n(x)$ has the indicated sign, and
99 $\gcd(\Nm J,m)=1$. For $c\in\ZZ/m\ZZ$,
100 \[
101  \Nm I\equiv c\pmod m
102  \quad\Longleftrightarrow\quad
103  \overline n_{\varepsilon}([x])=c(\Nm J\bmod m).
104 \]
105 This gives an actual finite residue target, which is allowed to be empty.
106 The product identity before cancellation does not require coprimality.
107 
108 Let $[J]=C^{-1}$ in $\Cl(\OO)$, and let $\mathcal G(J)$ denote the
109 actual fundamental-cone generator set. For every predicate $P:\RR\to\mathrm{Prop}$
110 and every real $X$, the norm-preserving correspondence gives
111 \begin{align*}
112  &\#\{x\in\mathcal G(J):\Nm(x)\leq X\Nm J,\ P(\Nm(x))\}\\
113  &\qquad=\#\mu(K)\,
114  \#\{I\ne0:[I]=C,\ \Nm I\leq X,\ P(\Nm I\,\Nm J)\}.
115 \end{align*}
116 The same norm-preserving equivalence carries arbitrary complex weights.
117 In particular, write $G_{J,\chi}(Y)$ for the sum of
118 $\chi(\Nm(x)\bmod m)$ over these generators with $\Nm(x)\leq Y$, and
119 $T_{C,\chi}(X)$ for the corresponding sum over ideals in class $C$.
120 For multiplicative $\chi$ preserving $0$ and $1$, the exact identity is
121 \begin{equation}\label{eq:weighted-torsion}
122  G_{J,\chi}(X\Nm J)
123  =\#\mu(K)\,\chi(\Nm J\bmod m)\,T_{C,\chi}(X).
124 \end{equation}
125 Both signs are included before applying this full roots-of-unity factor.
126 A root of unity can interchange the sign portions, so that factor is not
127 automatically valid for either portion separately.
128 
129 \smallskip
130 \noindent\emph{Lean attachment:}
131 \nolinkurl{NormResidueArithmetic}, \nolinkurl{NormResidueIdealFilter},
132 \nolinkurl{NormSignArithmetic}, \nolinkurl{IdealNormFilterAttachment}, and
133 \nolinkurl{IdealNormWeightedAttachment}.
134 
135 \newpage
136 \paragraph{Ordinary class characters: an unconditional power saving.}
137 The preceding block proved, for every ordinary ideal class $C$,
138 \[
139  A_C(X)=c_KX+O_{K,C}(X^{1-1/d}),\qquad
140  c_K=\frac{2^{r_1}(2\pi)^{r_2}R_K}{\#\mu(K)\sqrt{\absn{\Delta_K}}}.
141 \]
142 Here $A_C$ counts actual nonzero integral ideals, $r_1,r_2$ count the real
143 and complex places, $R_K$ is the regulator, and $\Delta_K$ is the discriminant. For a weight
144 $w:\Cl(\OO)\to\CC$, define the actual finite ideal sum
145 \[
146  S_w(X)=\sum_{\substack{I\ne0\\\Nm I\leq X}}w([I]).
147 \]
148 Exact grouping by ideal class gives $S_w(X)=\sum_C w(C)A_C(X)$.
149 If $\sum_Cw(C)=0$, the common leading coefficient cancels, so there is
150 $B_w\geq0$ such that
151 \[
152  \absn{S_w(X)}\leq B_wX^{1-1/d}\qquad(X\geq1).
153 \]
154 For every nontrivial character $\chi:\Cl(\OO)\to\CC^{\times}$,
155 the finite character sum is zero. Thus the displayed estimate applies
156 without an additional arithmetic cancellation hypothesis.
157 This conclusion concerns ordinary class characters; it does not identify
158 them with the further norm-residue characters needed for Frobenius separation.
159 
160 \paragraph{An actual Mellin endpoint.}
161 The counting functions are constant on the integer norm steps. Their
162 measurability, and hence that of $S_w$, is proved from this fact.
163 For zero-sum $w$, define
164 \[
165  F_w(h)=(1+h)\int_1^{\infty}x^{-2-h}S_w(x)\,dx
166  \qquad(h\geq0).
167 \]
168 Since $1-1/d<1$, the logarithmic first moment
169 \[
170  M_w=\int_1^{\infty}(1+\log x)\,\absn{x^{-2}S_w(x)}\,dx
171 \]
172 is finite. Lean proves the explicit estimate
173 $\absn{F_w(h)-F_w(0)}\leq hM_w$ for every $h\geq0$, and therefore
174 $F_w(h)=F_w(0)+O(h)$ as $h\downarrow0$.
175 The function here is the displayed integral of the actual ideal sum.
176 Its identification with the intended arithmetic Euler product is a separate step.
177 
178 For a finite family of nontrivial ordinary class characters, suppose functions
179 $p,Z$ satisfy $h\,p(h)\to P\ne0$, $h\,Z(h)\to Q\ne0$, and, for all sufficiently
180 small $h>0$,
181 \[
182  Z(h)=\left(p(h)\prod_i F_{\chi_i}(h)\right)^e,
183  \qquad e\in\NN.
184 \]
185 The checked real-axis criterion then gives $e=1$ and
186 $F_{\chi_i}(0)\ne0$ for every $i$. The pole limits and product identity
187 remain hypotheses of this application.
188 
189 \smallskip
190 \noindent\emph{Lean attachment:}
191 \nolinkurl{IdealClassCharacterBound}, \nolinkurl{IdealCharacterMellinMeasurable},
192 \nolinkurl{IdealCharacterMellin}, and \nolinkurl{IdealCharacterMellinPole}.
193 
194 \newpage
195 \paragraph{An actual unit action on ideal residues.}
196 Fix $m>0$ and a nonzero integral ideal $J$.
197 Multiplication by $u\in(\OO/m\OO)^{\times}$ gives a proved permutation of
198 $J/mJ$. Its inverse follows from $(ab-1)x\in mJ$ when
199 $ab-1\in m\OO$ and $x\in J$. No surjectivity of
200 $J/mJ\to\OO/m\OO$ or coprimality condition on $J$ is used.
201 The well-defined residue norm on this quotient satisfies
202 \[
203  \overline n_J(u\cdot a)=\overline n(u)\,\overline n_J(a).
204 \]
205 For a multiplicative $\chi:\ZZ/m\ZZ\to\CC$ preserving $1$, an exhibited
206 unit with
207 \begin{equation}\label{eq:unit-witness}
208  u\in(\OO/m\OO)^{\times},\qquad \chi(\overline n(u))\ne1
209 \end{equation}
210 therefore forces
211 \[
212  \sum_{a\in J/mJ}\chi\bigl(s\,\overline n_J(a)\bigr)=0
213  \qquad(s\in\ZZ/m\ZZ).
214 \]
215 Taking $s=1,-1$ gives the two finite means needed by the sign-corrected
216 norm weights. Their vanishing follows from the actual permutation.
217 
218 \paragraph{The assembled ideal norm-character estimate.}
Statement: Proposition: prop:norm-character219 \begin{proposition}\label{prop:norm-character}
220 Let $C\in\Cl(\OO)$, let $J\ne0$ be an integral ideal with $[J]=C^{-1}$,
221 and let $m>0$. Let $\chi:\ZZ/m\ZZ\to\CC$ preserve multiplication,
222 $0$, and $1$. Assume a residue-ring unit satisfying
223 \eqref{eq:unit-witness}, and assume
224 $\chi(\Nm J\bmod m)\ne0$. Then
225 \[
226  T_{C,\chi}(X)
227  =\sum_{\substack{I\ne0,\ [I]=C\\\Nm I\leq X}}
228        \chi(\Nm I\bmod m)
229  =O_{K,J,m,\chi}(X^{1-1/d}).
230 \]
231 More precisely, some $B\geq0$ bounds its absolute value by
232 $BX^{1-1/d}$ for every real $X\geq1$.
233 \end{proposition}
234 
235 The assembly identifies the residue sum with the sum over actual generators,
236 recombines the sign portions, and uses $Y=t^d$ to obtain
237 $\absn{G_{J,\chi}(Y)}\leq B_0(Y^{1-1/d}+1)$.
238 Equation~\eqref{eq:weighted-torsion} then permits division by the nonzero
239 factor $\#\mu(K)\chi(\Nm J\bmod m)$.
240 The final theorem supplies its finite means and counting estimates internally.
241 For $d=1$ the exponent is zero and the conclusion is a bounded sum, so the
242 argument does not require $d>1$.
243 
244 \paragraph{What remains open.}
245 Nontriviality of $\chi$ on the larger residue ring does not supply
246 \eqref{eq:unit-witness}: its restriction to the image of the norm on units
247 may be trivial. Witness existence for the intended characters, their
248 remaining norm-image cases, and suitable inverse-class representatives with
249 $\chi(\Nm J)\ne0$ are still arithmetic obligations.
250 Measurability and the Mellin attachment for these norm-character sums remain
251 to be checked. The compiled Mellin results above concern ordinary class characters.
252 The resulting estimates must also be attached to the required Euler-product
253 identities and prime-occurrence argument. The conditional pole criterion
254 does not supply those identities. Claims 9.1, 9.2, and 11.1 remain partial,
255 including the separate local compatibility obligations. The ledger stays
256 \textbf{17 checked / 3 partial}.
257 
258 \smallskip
259 \noindent\emph{Lean attachment:}
260 \nolinkurl{IdealResidueUnitActionMean}, \nolinkurl{NormResidueUnitCounting},
261 \nolinkurl{NormResidueGeneratorAttachment}, \nolinkurl{IdealNormCharacterBound},
262 and \nolinkurl{NormResidueCharacterCounting}.

Back to source controls

Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion