C. Retained residue-counting continuation

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 Section D supplies the later amended conditional completion. The counting formulas, hypotheses and remaining norm-image obligations below are preserved.

Permalink · Source line 4

Let \(K\) be a number field of degree \(d\geq1\), with ring of integers \({\mathcal O}={\mathcal O}_K\). Write \({\operatorname N} I=\#({\mathcal O}/I)\) for the absolute norm of a nonzero integral ideal and \(n(x)={\operatorname N}_{K/\mathbb Q}(x)\in{\mathbb Z}\) for \(x\in{\mathcal O}\). Thus \({\operatorname N}(x)={\lvert n(x)\rvert}\). Let \(\iota\) be the mixed embedding in its Euclidean coordinates, \(L(J)=\iota(J)\), and \(D\) the actual unit-norm fundamental cone used in the preceding counting block. Its norm function scales by \(t^d\) under a positive real dilation \(t\). The full-paper ledger remains 17 checked claims and 3 partial claims.

Permalink · Source line 20

Fix nonzero integral ideals \(M\subseteq J\), and put \(q=[J:M]=\#(J/M)\). The formal quotient of ideal lattices is identified with the additive congruence relation \(x-a\in M\) on actual elements of \(J\). In particular, the residue label is not an independent parameter attached to a count.

Permalink · Source line 30

The estimate is proved from the actual boundary charts and the fixed-lattice discrepancy theorem. The index factor comes from the covolume identity \({\operatorname{covol}}(L(M))=q\,{\operatorname{covol}}(L(J))\). For a complex weight \(w:J/M\to{\mathbb C}\), summing the estimates gives the leading term

with error at most \(B\sum_a{\lvert w(a)\rvert}(t^{d-1}+1)\). If the finite sum of weights is zero, only that error remains. Writing \(Y=t^d\) gives an error \(O(Y^{1-1/d}+1)\) for the actual norm threshold. These assertions include \(d=1\).

Lean attachment: ResidueLatticeIdeal, ResidueLatticeIdealPoints, ResidueLatticeIdealWeights, and ResidueLatticeNormCounts.

Permalink · Source line 46

For \(m\in{\mathbb N}\), reducing the multiplication matrices of \({\mathcal O}\) modulo \(m\) and taking their determinants constructs a monoid homomorphism

The construction is proved independent of the integral basis. For \(m\ne0\), its source is finite of cardinality \(m^d\). Consequently \(x-y\in m{\mathcal O}\) implies \(n(x)\equiv n(y)\pmod m\). No surjectivity of \(\overline n\) is asserted.

The relation to the geometric sign is also proved. If \(\sigma\) ranges over real embeddings and \(\tau\) over one embedding from each complex pair, then

For \(x\ne0\), the second factor is positive. Thus the sign of \(n(x)\) is exactly the sign of the real-coordinate product. Cutting \(D\) into its positive and negative portions \(D_+,D_-\) adds no boundary outside the existing frontier, and both portions retain the proved boundary atlas. They are disjoint and their union is \(D\).

For \(\varepsilon\in\{1,-1\}\) define \(\overline n_{\varepsilon}(a)=\varepsilon\overline n(a)\). On the corresponding sign portion,

The sign cannot be dropped: \(-1\equiv2\pmod3\), whereas \({\operatorname N}(-1)=1\) and \({\operatorname N}(2)=2\) for principal ideals of \({\mathbb Z}\).

Permalink · Source line 66

Suppose \(IJ=(x)\), \(n(x)\) has the indicated sign, and \(\gcd({\operatorname N} J,m)=1\). For \(c\in{\mathbb Z}/m{\mathbb Z}\),

This gives an actual finite residue target, which is allowed to be empty. The product identity before cancellation does not require coprimality.

Let \([J]=C^{-1}\) in \({\operatorname{Cl}}({\mathcal O})\), and let \(\mathcal G(J)\) denote the actual fundamental-cone generator set. For every predicate \(P:{\mathbb R}\to\mathrm{Prop}\) and every real \(X\), the norm-preserving correspondence gives

The same norm-preserving equivalence carries arbitrary complex weights. In particular, write \(G_{J,\chi}(Y)\) for the sum of \(\chi({\operatorname N}(x)\bmod m)\) over these generators with \({\operatorname N}(x)\leq Y\), and \(T_{C,\chi}(X)\) for the corresponding sum over ideals in class \(C\). For multiplicative \(\chi\) preserving \(0\) and \(1\), the exact identity is

Both signs are included before applying this full roots-of-unity factor. A root of unity can interchange the sign portions, so that factor is not automatically valid for either portion separately.

Lean attachment: NormResidueArithmetic, NormResidueIdealFilter, NormSignArithmetic, IdealNormFilterAttachment, and IdealNormWeightedAttachment.

Permalink · Source line 98

The preceding block proved, for every ordinary ideal class \(C\),

Here \(A_C\) counts actual nonzero integral ideals, \(r_1,r_2\) count the real and complex places, \(R_K\) is the regulator, and \(\Delta_K\) is the discriminant. For a weight \(w:{\operatorname{Cl}}({\mathcal O})\to{\mathbb C}\), define the actual finite ideal sum

Exact grouping by ideal class gives \(S_w(X)=\sum_C w(C)A_C(X)\). If \(\sum_Cw(C)=0\), the common leading coefficient cancels, so there is \(B_w\geq0\) such that

For every nontrivial character \(\chi:{\operatorname{Cl}}({\mathcal O})\to{\mathbb C}^{\times}\), the finite character sum is zero. Thus the displayed estimate applies without an additional arithmetic cancellation hypothesis. This conclusion concerns ordinary class characters; it does not identify them with the further norm-residue characters needed for Frobenius separation.

Permalink · Source line 137

The counting functions are constant on the integer norm steps. Their measurability, and hence that of \(S_w\), is proved from this fact. For zero-sum \(w\), define

Since \(1-1/d<1\), the logarithmic first moment

is finite. Lean proves the explicit estimate \({\lvert F_w(h)-F_w(0)\rvert}\leq hM_w\) for every \(h\geq0\), and therefore \(F_w(h)=F_w(0)+O(h)\) as \(h\downarrow0\). The function here is the displayed integral of the actual ideal sum. Its identification with the intended arithmetic Euler product is a separate step.

For a finite family of nontrivial ordinary class characters, suppose functions \(p,Z\) satisfy \(h\,p(h)\to P\ne0\), \(h\,Z(h)\to Q\ne0\), and, for all sufficiently small \(h>0\),

The checked real-axis criterion then gives \(e=1\) and \(F_{\chi_i}(0)\ne0\) for every \(i\). The pole limits and product identity remain hypotheses of this application.

Lean attachment: IdealClassCharacterBound, IdealCharacterMellinMeasurable, IdealCharacterMellin, and IdealCharacterMellinPole.

Permalink · Source line 161

Fix \(m>0\) and a nonzero integral ideal \(J\). Multiplication by \(u\in({\mathcal O}/m{\mathcal O})^{\times}\) gives a proved permutation of \(J/mJ\). Its inverse follows from \((ab-1)x\in mJ\) when \(ab-1\in m{\mathcal O}\) and \(x\in J\). No surjectivity of \(J/mJ\to{\mathcal O}/m{\mathcal O}\) or coprimality condition on \(J\) is used. The well-defined residue norm on this quotient satisfies

For a multiplicative \(\chi:{\mathbb Z}/m{\mathbb Z}\to{\mathbb C}\) preserving \(1\), an exhibited unit with

therefore forces

Taking \(s=1,-1\) gives the two finite means needed by the sign-corrected norm weights. Their vanishing follows from the actual permutation.

Permalink · Source line 196

The assembly identifies the residue sum with the sum over actual generators, recombines the sign portions, and uses \(Y=t^d\) to obtain \({\lvert G_{J,\chi}(Y)\rvert}\leq B_0(Y^{1-1/d}+1)\). Equation (1) then permits division by the nonzero factor \(\#\mu(K)\chi({\operatorname N} J\bmod m)\). The final theorem supplies its finite means and counting estimates internally. For \(d=1\) the exponent is zero and the conclusion is a bounded sum, so the argument does not require \(d>1\).

Permalink · Source line 235

Nontriviality of \(\chi\) on the larger residue ring does not supply (2): its restriction to the image of the norm on units may be trivial. Witness existence for the intended characters, their remaining norm-image cases, and suitable inverse-class representatives with \(\chi({\operatorname N} J)\ne0\) are still arithmetic obligations. Measurability and the Mellin attachment for these norm-character sums remain to be checked. The compiled Mellin results above concern ordinary class characters. The resulting estimates must also be attached to the required Euler-product identities and prime-occurrence argument. The conditional pole criterion does not supply those identities. Claims 9.1, 9.2, and 11.1 remain partial, including the separate local compatibility obligations. The ledger stays 17 checked / 3 partial.

Lean attachment: IdealResidueUnitActionMean, NormResidueUnitCounting, NormResidueGeneratorAttachment, IdealNormCharacterBound, and NormResidueCharacterCounting.

Permalink · Source line 245