Digit recursion over a commutative ring, and its corollaries for quadratic characters

The digit recursion of SegmentoII.digit_recursion, for χ : ℕ → R with values in any commutative ring R (the hypotheses are bundled in DigitosII.Hyp), and the consequences drawn from it for real characters: families of zeros of S m = ∑_{n ≤ m} n χ(n), the block construction, and the identities behind the weighted half sum. Where the paper uses the class number h(−q), the statements here use T_q = ∑_{r<q} r χ(r) (which is q B_{1,χ}).

Main results

• DigitosII.digit_recursion, DigitosII.zero_step, DigitosII.zeros_from_digits: the digit recursion and the propagation of zeros, over R.
• DigitosII.cor_digitos_a – DigitosII.cor_digitos_f_neg: the corollaries (a)–(f) of the digit recursion (counts and explicit families of zeros, values at (q^j − 1)/2).
• DigitosII.prop_bloques: concatenation of digit blocks, with T_q = −q h as a hypothesis.
• DigitosII.diag: the two identities 4 χ(2) T = 2 (1 − χ(2)) T_f and f χ(2) C = (1 − 2 χ(2)) T_f for f = 2c + 1 and χ odd.
• DigitosII.cor_orden_iff, DigitosII.cor_orden_zeros, DigitosII.cor_orden_trivial_on_two: for χ with values in a domain with 2 ≠ 0 and B_{1,χ} ≠ 0 as a hypothesis.

References

• C. Marín, Zeros of weighted partial sums of completely multiplicative functions: Dirichlet characters, the Euler factor at 2 and Conrey's sine series, Zenodo (2026), doi:10.5281/zenodo.22847374.

Objects (those of SegmentoII, generalised from ℤ to a commutative ring)

def DigitosII.S {R : Type u_1} [CommRing R] (χ : ℕ → R) (m : ℕ) : R

S m = ∑_{n=1}^{m} n χ(n).

Equations

• DigitosII.S χ m = ∑ n ∈ Finset.Icc 1 m, ↑n * χ n

def DigitosII.C {R : Type u_1} [CommRing R] (χ : ℕ → R) (r : ℕ) : R

C r = ∑_{n=1}^{r} χ(n).

Equations

• DigitosII.C χ r = ∑ n ∈ Finset.Icc 1 r, χ n

def DigitosII.T {R : Type u_1} [CommRing R] (χ : ℕ → R) (r : ℕ) : R

T r = ∑_{n=1}^{r} n χ(n) (same as S; used for r < q).

Equations

• DigitosII.T χ r = ∑ n ∈ Finset.Icc 1 r, ↑n * χ n

def DigitosII.Tq {R : Type u_1} [CommRing R] (χ : ℕ → R) (q : ℕ) : R

T_q = T (q-1) = ∑_{r<q} r χ(r); for a Dirichlet character modulo q this is q B_{1,χ}.

Equations

• DigitosII.Tq χ q = DigitosII.T χ (q - 1)

structure DigitosII.Hyp {R : Type u_1} [CommRing R] (q : ℕ) (χ : ℕ → R) (s : R) : Prop

The hypotheses of thm:digitos: χ completely multiplicative, periodic modulo q on the residues 1, …, q-1, χ(q) = s, and ∑_{r=1}^{q-1} χ(r) = 0.

• two_le : 2 ≤ q
• mul (a b : ℕ) : χ (a * b) = χ a * χ b
• per (j r : ℕ) : 1 ≤ r → r < q → χ (j * q + r) = χ r
• at_q : χ q = s
• sum0 : C χ (q - 1) = 0

theorem DigitosII.S_zero {R : Type u_1} [CommRing R] (χ : ℕ → R) : S χ 0 = 0

theorem DigitosII.T_zero {R : Type u_1} [CommRing R] (χ : ℕ → R) : T χ 0 = 0

theorem DigitosII.C_zero {R : Type u_1} [CommRing R] (χ : ℕ → R) : C χ 0 = 0

theorem DigitosII.S_succ {R : Type u_1} [CommRing R] (χ : ℕ → R) (n : ℕ) : S χ (n + 1) = S χ n + (↑n + 1) * χ (n + 1)

theorem DigitosII.T_succ {R : Type u_1} [CommRing R] (χ : ℕ → R) (n : ℕ) : T χ (n + 1) = T χ n + (↑n + 1) * χ (n + 1)

theorem DigitosII.C_succ {R : Type u_1} [CommRing R] (χ : ℕ → R) (n : ℕ) : C χ (n + 1) = C χ n + χ (n + 1)

theorem DigitosII.S_eq_T {R : Type u_1} [CommRing R] (χ : ℕ → R) (n : ℕ) : S χ n = T χ n

theorem DigitosII.T_range {R : Type u_1} [CommRing R] (χ : ℕ → R) (n : ℕ) : T χ n = ∑ i ∈ Finset.range n, (↑i + 1) * χ (i + 1)

theorem DigitosII.C_range {R : Type u_1} [CommRing R] (χ : ℕ → R) (n : ℕ) : C χ n = ∑ i ∈ Finset.range n, χ (i + 1)

Theorem thm:digitos over a commutative ring

theorem DigitosII.digit_recursion {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {s : R} (h : Hyp q χ s) (k r : ℕ) (hr : r < q) : S χ (q * k + r) = s * ↑q * S χ k + ↑k * (Tq χ q + ↑q * C χ r) + T χ r

thm:digitos (4.1), for χ with values in a commutative ring. For r < q: S (q k + r) = s q S k + k (T_q + q C r) + T r.

theorem DigitosII.digit_zero {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {s : R} (h : Hyp q χ s) (k : ℕ) : S χ (q * k) = s * ↑q * S χ k + ↑k * Tq χ q

The case r = 0: S (q k) = s q S k + k T_q.

def DigitosII.InR {R : Type u_1} [CommRing R] (χ : ℕ → R) (q r : ℕ) : Prop

The digit set R_q = {r < q : T_q + q C r = 0 = T r}.

Equations

• DigitosII.InR χ q r = (r < q ∧ DigitosII.Tq χ q + ↑q * DigitosII.C χ r = 0 ∧ DigitosII.T χ r = 0)

theorem DigitosII.zero_step {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {s : R} (h : Hyp q χ s) (k r : ℕ) (hk : S χ k = 0) (hR : InR χ q r) : S χ (q * k + r) = 0

First statement of cor:digitos, one step.

theorem DigitosII.zeros_from_digits {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {s : R} (h : Hyp q χ s) (m : ℕ) (hm : ∀ d ∈ q.digits m, InR χ q d) : S χ m = 0

First statement of cor:digitos: every m whose base-q digits all lie in R_q has S m = 0, for every value of s.

cor:digitos (d) and (e)

theorem DigitosII.cor_digitos_d {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {s : R} (h : Hyp q χ s) {k r : ℕ} (hr : r < q) (hk : S χ (q * k) = 0) (hC : C χ r = 0) (hT : T χ r = 0) : S χ (q * k + r) = 0

cor:digitos (d), first sentence: for every q and s, if S(q k) = 0 and C r = T r = 0, then S(q k + r) = 0.

theorem DigitosII.cor_digitos_d_four {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {s : R} (h : Hyp q χ s) (hq : 4 < q) (h1 : χ 1 = 1) (h2 : χ 2 = -1) (h3 : χ 3 = -1) {k : ℕ} (hk : S χ (q * k) = 0) : S χ (q * k + 4) = 0

cor:digitos (d), second sentence: when q > 4 (the paper: q > 3, q an odd prime) and χ(2) = χ(3) = -1, the digit r = 4 qualifies, since 1 - 2 - 3 + 4 = 0.

theorem DigitosII.cor_digitos_e {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} (h : Hyp q χ (-1)) (m : ℕ) : S χ (q ^ 2 * m) = ↑q ^ 2 * S χ m

cor:digitos (e): if s = -1, then S(q² m) = q² S(m).

theorem DigitosII.cor_digitos_e_zeros {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} (h : Hyp q χ (-1)) {m : ℕ} (hm : S χ m = 0) (i : ℕ) : S χ (q ^ (2 * i) * m) = 0

cor:digitos (e), second clause: a single zero of S gives infinitely many, S(q^{2i} m) = 0 for every i.

prop:bloques

theorem DigitosII.digit_D {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {h : R} (H : Hyp q χ 1) (hT : Tq χ q = -↑q * h) (k r : ℕ) (hr : r < q) : S χ (q * k + r) = ↑q * S χ k + ↑q * ↑k * (C χ r - h) + T χ r

With s = 1 and T_q = -q h, thm:digitos reads S(q k + r) = q S k + q k D(r) + T r, D(r) = C(r) - h.

theorem DigitosII.block_append {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {h : R} (H : Hyp q χ 1) (hT : Tq χ q = -↑q * h) (ds : List ℕ) (hds : ∀ d ∈ ds, d < q) (k : ℕ) : S χ (q ^ ds.length * k + Nat.ofDigits q ds) = ↑q ^ ds.length * S χ k + ↑q ^ ds.length * ↑k * (List.map (fun (d : ℕ) => C χ d - h) ds).sum + S χ (Nat.ofDigits q ds)

Appending the digits of B (little-endian list ds, B = ofDigits q ds, L = |ds|) to k: S(q^L k + B) = q^L S k + q^L k ∑ D(d_i) + S(B).

theorem DigitosII.prop_bloques {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {h : R} (H : Hyp q χ 1) (hT : Tq χ q = -↑q * h) (ds : List ℕ) (hds : ∀ d ∈ ds, d < q) (hD : (List.map (fun (d : ℕ) => C χ d - h) ds).sum = 0) (hB : S χ (Nat.ofDigits q ds) = h * ↑(Nat.ofDigits q ds)) (t : ℕ) : S χ (q * (Nat.ofDigits q ds * ∑ i ∈ Finset.range t, (q ^ ds.length) ^ i)) = 0

prop:bloques (4.4). Let s = 1 and T_q = -q h (for q ≡ 3 mod 4, q > 3, h = h(-q) this is the class number formula). If the base-q digits ds of B (little-endian, leading zeros allowed) have ∑ D(d_i) = 0 and S(B) = h B, then, with Q = q^L, every m_t = q B (1 + Q + … + Q^{t-1}) is a zero of S.

The identities of thm:diag

theorem DigitosII.reflect {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} {ε : R} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hε : χ (q - 1) = ε) {b : ℕ} (hb1 : 1 ≤ b) (hbq : b < q) : χ (q - b) = ε * χ b

Reflection: if χ(q-1) = ε, then χ(q-b) = ε χ(b) for 1 ≤ b < q.

theorem DigitosII.sum_range_two_mul {M : Type u_2} [AddCommMonoid M] (g : ℕ → M) (c : ℕ) : ∑ i ∈ Finset.range (2 * c), g i = ∑ j ∈ Finset.range c, (g (2 * j) + g (2 * j + 1))

theorem DigitosII.diag {R : Type u_1} [CommRing R] {c : ℕ} {χ : ℕ → R} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < 2 * c + 1 → χ (j * (2 * c + 1) + r) = χ r) (hodd : χ (2 * c) = -1) : 4 * χ 2 * T χ c = 2 * (1 - χ 2) * Tq χ (2 * c + 1) ∧ (2 * ↑c + 1) * χ 2 * C χ c = (1 - 2 * χ 2) * Tq χ (2 * c + 1) ∧ C χ (2 * c) = 0

The identities in the proof of thm:diag (Kanemitsu–Kuzumaki, Kučera), for f = 2c+1 odd and χ completely multiplicative, periodic modulo f on the residues and odd (χ(f-1) = -1), with values in any commutative ring. Here T c = ∑_{n ≤ (f-1)/2} n χ(n), C c = ∑_{n ≤ (f-1)/2} χ(n) and T_f = ∑_{a<f} a χ(a) = f B_{1,χ}: 4 χ(2) T = 2 (1 - χ(2)) T_f (i.e. T = (f/2) B_{1,χ} (χ(2)^{-1} - 1)), f χ(2) C = (1 - 2 χ(2)) T_f (i.e. C = (χ(2)^{-1} - 2) B_{1,χ}), and ∑_{a<f} χ(a) = 0.

theorem DigitosII.two_half_pow (c j : ℕ) : 2 * (((2 * c + 1) ^ j - 1) / 2) + 1 = (2 * c + 1) ^ j

(f^j - 1)/2 with f = 2c+1: 2 m_j + 1 = f^j.

theorem DigitosII.half_pow_succ (c j : ℕ) : ((2 * c + 1) ^ (j + 1) - 1) / 2 = (2 * c + 1) * (((2 * c + 1) ^ j - 1) / 2) + c

m_{j+1} = f m_j + c: the base-f digits of (f^j - 1)/2 are all c = (f-1)/2.

cor:orden (4.5): χ with values in an integral domain

theorem DigitosII.hyp_of_odd {R : Type u_1} [CommRing R] {c : ℕ} (hc : 1 ≤ c) {χ : ℕ → R} {s : R} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < 2 * c + 1 → χ (j * (2 * c + 1) + r) = χ r) (hodd : χ (2 * c) = -1) (hs : χ (2 * c + 1) = s) : Hyp (2 * c + 1) χ s

The hypotheses of thm:digitos hold for an odd χ (the sum ∑ χ(r) = 0 is automatic).

theorem DigitosII.cor_orden_iff {R : Type u_1} [CommRing R] [IsDomain R] {q : ℕ} (hq : q % 2 = 1) {χ : ℕ → R} (h2R : 2 ≠ 0) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hodd : χ (q - 1) = -1) (hA : Tq χ q ≠ 0) : S χ ((q - 1) / 2) = 0 ↔ χ 2 = 1

cor:orden (4.5), the equivalence. q odd, χ completely multiplicative, periodic modulo q on the residues, odd (χ(q-1) = -1), with values in an integral domain where 2 ≠ 0, and T_q = q B_{1,χ} ≠ 0 (for a primitive odd character this is L(0,χ) ≠ 0; here a hypothesis). Then S((q-1)/2) = 0 ↔ χ(2) = 1.

theorem DigitosII.cor_orden_zeros {R : Type u_1} [CommRing R] [IsDomain R] {q : ℕ} (hq : q % 2 = 1) (hq3 : 3 ≤ q) {χ : ℕ → R} {s : R} (h2R : 2 ≠ 0) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hodd : χ (q - 1) = -1) (hs : χ q = s) (h2 : χ 2 = 1) (j : ℕ) : S χ ((q ^ j - 1) / 2) = 0

cor:orden (4.5), the zeros: if moreover χ(2) = 1, then (q-1)/2 ∈ R_q and S((q^j - 1)/2) = 0 for every j (for every value s = χ(q); B_{1,χ} ≠ 0 is not needed).

theorem DigitosII.cor_orden_trivial_on_two {R : Type u_1} [CommRing R] {χ : ℕ → R} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (h1 : χ 1 = 1) : χ 2 = 1 ↔ ∀ (k : ℕ), χ (2 ^ k) = 1

cor:orden (4.5), last sentence: given χ(1) = 1, χ(2) = 1 iff χ is trivial on the powers of 2.

theorem DigitosII.cor_digitos_d_three {χ : ℕ → ℤ} (h : Hyp 3 χ (-1)) (h1 : χ 1 = 1) (h2 : χ 2 = -1) {k : ℕ} (hk : S χ (3 * k) = 0) : S χ (3 * k + 4) = 0

cor:digitos (d), third sentence: for q = 3 and s = -1 (with χ(2) = -1), S(3k) = 0 implies S(3k + 4) = 0.

cor:digitos (a), (b), (c), (f), with T_q = q B_{1,χ} in place of h(-q)

def DigitosII.zseq (q : ℕ) : ℕ → ℕ

The sequence of cor:digitos (c): z_0 = q, z_{i+1} = q (z_i + 1).

Equations

• DigitosII.zseq q 0 = q
• DigitosII.zseq q i.succ = q * (DigitosII.zseq q i + 1)

theorem DigitosII.dvd_zseq (q i : ℕ) : q ∣ zseq q i

theorem DigitosII.S_one {R : Type u_1} [CommRing R] (χ : ℕ → R) : S χ 1 = χ 1

theorem DigitosII.cor_digitos_c {R : Type u_1} [CommRing R] {q : ℕ} {χ : ℕ → R} (H : Hyp q χ 1) (h1 : χ 1 = 1) (hT : Tq χ q = -↑q) (i : ℕ) : S χ (zseq q i) = 0

cor:digitos (c), q > 3: with s = 1, χ(1) = 1 and T_q = -q (that is B_{1,χ} = -1; for q ≡ 3 mod 4, q > 3 this is h(-q) = 1), S vanishes along z_0 = q, z_{i+1} = q (z_i + 1).

theorem DigitosII.cor_digitos_c_three {R : Type u_1} [CommRing R] {χ : ℕ → R} (H : Hyp 3 χ 1) (h1 : χ 1 = 1) (h2 : χ 2 = -1) (i : ℕ) : S χ (zseq 27 i) = 0

cor:digitos (c), q = 3: with s = 1, χ(1) = 1, χ(2) = -1, S vanishes along z_0 = 27, z_{i+1} = 27 (z_i + 1).

theorem DigitosII.Tq_even {q : ℕ} {χ : ℕ → ℤ} {s : ℤ} (H : Hyp q χ s) (heven : χ (q - 1) = 1) : Tq χ q = 0

An even χ (χ(q-1) = 1) with ∑ χ(r) = 0 has T_q = 0.

def DigitosII.G (q : ℕ) : ℕ → Finset ℕ

The numbers of at most J base-q digits, all in {0, q-1}.

Equations

• DigitosII.G q 0 = {0}
• DigitosII.G q i.succ = Finset.image (fun (p : ℕ × ℕ) => q * p.1 + p.2) (DigitosII.G q i ×ˢ {0, q - 1})

theorem DigitosII.zero_mem_G (q J : ℕ) : 0 ∈ G q J

theorem DigitosII.G_card {q : ℕ} (hq : 2 ≤ q) (J : ℕ) : (G q J).card = 2 ^ J

theorem DigitosII.cor_digitos_a_digits {q : ℕ} {χ : ℕ → ℤ} {s : ℤ} (H : Hyp q χ s) (heven : χ (q - 1) = 1) : InR χ q 0 ∧ InR χ q (q - 1)

cor:digitos (a), the digits: for χ even (χ(q-1) = 1; for a quadratic χ this is q ≡ 1 mod 4), 0, q-1 ∈ R_q.

theorem DigitosII.G_spec {q : ℕ} {χ : ℕ → ℤ} {s : ℤ} (H : Hyp q χ s) (heven : χ (q - 1) = 1) (J x : ℕ) : x ∈ G q J → x < q ^ J ∧ S χ x = 0

theorem DigitosII.cor_digitos_a {q : ℕ} {χ : ℕ → ℤ} {s : ℤ} (H : Hyp q χ s) (heven : χ (q - 1) = 1) (J : ℕ) : 2 ^ J - 1 ≤ {m ∈ Finset.Ioo 0 (q ^ J) | S χ m = 0}.card

cor:digitos (a), the count: for χ even, S has at least 2^J - 1 zeros in (0, q^J).

theorem DigitosII.cor_digitos_b {q : ℕ} (hq : q % 2 = 1) (hq3 : 3 ≤ q) {χ : ℕ → ℤ} {s : ℤ} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hodd : χ (q - 1) = -1) (hs : χ q = s) (h2 : χ 2 = 1) (j : ℕ) : S χ ((q ^ j - 1) / 2) = 0

cor:digitos (b): χ odd with χ(2) = 1 (for a quadratic χ: q ≡ 7 mod 8) has S((q^j - 1)/2) = 0 for every j, for every s. The case R = ℤ of cor_orden_zeros.

theorem DigitosII.cor_digitos_f {q : ℕ} (hq : q % 2 = 1) (hq3 : 3 ≤ q) {χ : ℕ → ℤ} {s : ℤ} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hodd : χ (q - 1) = -1) (hs : χ q = s) (h2 : χ 2 = -1) (j : ℕ) : S χ ((q ^ (j + 1) - 1) / 2) = -Tq χ q * ↑q ^ j * ∑ i ∈ Finset.range (j + 1), s ^ i

cor:digitos (f): χ odd with χ(2) = -1 (for a quadratic χ: q ≡ 3 mod 8): S((q^{j+1} - 1)/2) = -T_q q^j (1 + s + … + s^j). With T_q = -q h(-q) (and h(-3) = 1/3, where T_3 = -1) this is the paper's h(-q) q^{j+1} (1 + … + s^j).

theorem DigitosII.alt_sum (i : ℕ) : ∑ l ∈ Finset.range (2 * i), (-1) ^ l = 0

theorem DigitosII.cor_digitos_f_neg {q : ℕ} (hq : q % 2 = 1) (hq3 : 3 ≤ q) {χ : ℕ → ℤ} (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hper : ∀ (j r : ℕ), 1 ≤ r → r < q → χ (j * q + r) = χ r) (hodd : χ (q - 1) = -1) (hs : χ q = -1) (h2 : χ 2 = -1) (i : ℕ) : S χ ((q ^ (2 * i) - 1) / 2) = 0

cor:digitos (f), s = -1: S((q^{2i} - 1)/2) = 0 for every i.