∑_{n ≤ m} n χ(n) has no positive zero for q = 179 and q = 227

Let χ : ℕ → ℤ be completely multiplicative with χ(n) = (n | q) (Legendre symbol) for q ∤ n and χ(q) = 1. For q = 179 and q = 227, S(m) = ∑_{n ≤ m} n χ(n) never vanishes for m ≥ 1. The proof is a finite certificate (a cone U, rays H, a set R of states) whose validity is a decidable proposition checked by decide +kernel; a general theorem turns a valid certificate into the non-vanishing of S, through the digit recursion of SegmentoII.digit_recursion.

The certificate data in the file are witnesses only: everything about them is checked in the kernel. Negative controls (q = 59, which has zeros, and corrupted certificates) are rejected by the checker.

Main results

• SegmentoIISinCeros.no_zero_of_valid: a valid certificate gives S χ m ≠ 0 for all m ≥ 1.
• SegmentoIISinCeros.valid179, SegmentoIISinCeros.valid227: the certificates, by decide +kernel.
• SegmentoIISinCeros.S_ne_zero_179, SegmentoIISinCeros.S_ne_zero_227: the theorem for every χ satisfying the hypotheses (names as cited by the paper's blueprint).
• SegmentoIISinCeros.leg_eq_legendreSym: the computable symbol leg is Mathlib's legendreSym off the multiples of q (Euler's criterion).
• SegmentoIISinCeros.chi0_spec: the explicit chi0 q satisfies the hypotheses, so they are not vacuous; S_ne_zero_179_legendreSym, S_chi0_ne_zero_179 and their 227 versions.

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.

§1 Digit recursion

The sums S, C, T, Tq and the digit recursion are those of Formalizations.NumberTheory.WeightedCharacterSums.DigitRecursion.

§2 Computable Legendre symbol and the residue table

def SegmentoIISinCeros.legRes (q x : ℕ) : ℤ

Legendre symbol of a residue x (0 ≤ x < q) by Euler's criterion x^((q-1)/2) mod q.

Equations

• SegmentoIISinCeros.legRes q x = if x = 0 then 0 else if x.pow ((q - 1) / 2) % q = 1 then 1 else -1

def SegmentoIISinCeros.leg (q n : ℕ) : ℤ

leg q n = (n | q) computed on the residue n % q.

Equations

• SegmentoIISinCeros.leg q n = SegmentoIISinCeros.legRes q (n % q)

theorem SegmentoIISinCeros.leg_periodic (q j r : ℕ) : leg q (j * q + r) = leg q r

def SegmentoIISinCeros.chain (q : ℕ) : ℕ → ℤ → ℤ → List (ℕ × ℤ × ℤ) → Bool

The table tab lists (r, C r - h, T r) for r = r₀, r₀+1, …, q-1, built incrementally from leg. chain q r d t tab = true checks it starting at (r, d, t).

Equations

• One or more equations did not get rendered due to their size.
• SegmentoIISinCeros.chain q x✝² x✝¹ x✝ [] = (x✝² == q)

theorem SegmentoIISinCeros.chain_sound (q : ℕ) (χ : ℕ → ℤ) (hleg : ∀ (n : ℕ), n % q ≠ 0 → χ n = leg q n) (h : ℤ) (l : List (ℕ × ℤ × ℤ)) (r : ℕ) : chain q r (SegmentoII.C χ r - h) (SegmentoII.T χ r) l = true → ∀ (r' : ℕ), r ≤ r' → r' < q → (r', SegmentoII.C χ r' - h, SegmentoII.T χ r') ∈ l

Soundness of the table: every (r, C χ r - h, T χ r), r₀ ≤ r < q, is in tab.

§3 The certificate predicate and the analytic lemmas

@[reducible, inline]

abbrev SegmentoIISinCeros.inU (a b : ℤ) : Prop

The cone U = {(a,b) : b(a+b) ≤ 0}.

Equations

• SegmentoIISinCeros.inU a b = (b * (a + b) ≤ 0)

@[reducible, inline]

abbrev SegmentoIISinCeros.inH (a b : ℤ) : Prop

The three rays H.

Equations

• SegmentoIISinCeros.inH a b = (23 ≤ a ∧ (b = 0 ∨ b = -a) ∨ a ≤ -23 ∧ 2 * b = -a)

@[reducible, inline]

abbrev SegmentoIISinCeros.inW (R : List (ℤ × ℤ)) (a b : ℤ) : Prop

W = R ∪ H.

Equations

• SegmentoIISinCeros.inW R a b = ((a, b) ∈ R ∨ SegmentoIISinCeros.inH a b)

@[reducible, inline]

abbrev SegmentoIISinCeros.EntryOK (q : ℕ) (h P : ℤ) (c : ℕ) (e : ℕ × ℤ × ℤ) : Prop

Per-entry facts of the residue table e = (r, D r, T r).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev SegmentoIISinCeros.StripPt (q : ℕ) (tab : List (ℕ × ℤ × ℤ)) (padres : List (ℤ × ℤ)) (a b : ℤ) : Prop

Strip point (a,b): every integral transition stays in U; accepting edges are listed.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev SegmentoIISinCeros.StripOK (q : ℕ) (tab : List (ℕ × ℤ × ℤ)) (padres : List (ℤ × ℤ)) (P : ℤ) : Prop

The finite strip -12 < a < P, |b| ≤ 11 (enough: U forces b between 0 and -a).

Equations

• SegmentoIISinCeros.StripOK q tab padres P = ∀ i ∈ List.range 24, ∀ j ∈ List.range 23, -11 + ↑i < P → SegmentoIISinCeros.StripPt q tab padres (-11 + ↑i) (-11 + ↑j)

@[reducible, inline]

abbrev SegmentoIISinCeros.BackOK (q : ℕ) (tab : List (ℕ × ℤ × ℤ)) (R : List (ℤ × ℤ)) : Prop

Backward closure of R inside U: every U-predecessor G_r(p) of p ∈ R is in R ∪ H.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev SegmentoIISinCeros.Valid (q : ℕ) (h P : ℤ) (c : ℕ) (tab : List (ℕ × ℤ × ℤ)) (R padres : List (ℤ × ℤ)) : Prop

The whole certificate.

Equations

• One or more equations did not get rendered due to their size.

def SegmentoIISinCeros.check (q : ℕ) (h P : ℤ) (c : ℕ) (tab : List (ℕ × ℤ × ℤ)) (R padres : List (ℤ × ℤ)) : Bool

The Bool checker is the decision procedure of Valid.

Equations

• SegmentoIISinCeros.check q h P c tab R padres = decide (SegmentoIISinCeros.Valid q h P c tab R padres)

theorem SegmentoIISinCeros.check_sound {q : ℕ} {h P : ℤ} {c : ℕ} {tab : List (ℕ × ℤ × ℤ)} {R padres : List (ℤ × ℤ)} (hc : check q h P c tab R padres = true) : Valid q h P c tab R padres

theorem SegmentoIISinCeros.U_pos {a b : ℤ} (hU : inU a b) (ha : 0 ≤ a) : b ≤ 0 ∧ 0 ≤ a + b

theorem SegmentoIISinCeros.U_neg {a b : ℤ} (hU : inU a b) (ha : a ≤ 0) : 0 ≤ b ∧ a + b ≤ 0

theorem SegmentoIISinCeros.strip_of {q : ℕ} {tab : List (ℕ × ℤ × ℤ)} {padres : List (ℤ × ℤ)} {P a b : ℤ} (hS : StripOK q tab padres P) (hP : P ≤ 12) (hU : inU a b) (h1 : -12 < a) (h2 : a < P) : StripPt q tab padres a b

Strip coordinates.

theorem SegmentoIISinCeros.emod_div_of_mul {q : ℕ} (hq : 0 < q) {x y : ℤ} (hx : ↑q * y = x) : x % ↑q = 0 ∧ x / ↑q = y

theorem SegmentoIISinCeros.fwd {q : ℕ} {h P : ℤ} {c : ℕ} {tab : List (ℕ × ℤ × ℤ)} {R padres : List (ℤ × ℤ)} (hV : Valid q h P c tab R padres) {r : ℕ} {d t a b b' : ℤ} (he : (r, d, t) ∈ tab) (hU : inU a b) (hstep : ↑q * b' = b - t - a * ↑r) : inU (a + d) b'

Forward invariance of U.

theorem SegmentoIISinCeros.acc {q : ℕ} {h P : ℤ} {c : ℕ} {tab : List (ℕ × ℤ × ℤ)} {R padres : List (ℤ × ℤ)} (hV : Valid q h P c tab R padres) {r : ℕ} {d t a b : ℤ} (he : (r, d, t) ∈ tab) (hr : r ≠ 0) (hU : inU a b) (hstep : ↑q * 0 = b - t - a * ↑r) : inW R a b

Accepting edges start in R ∪ H.

theorem SegmentoIISinCeros.back_H {q : ℕ} {h P : ℤ} {c : ℕ} {tab : List (ℕ × ℤ × ℤ)} {R padres : List (ℤ × ℤ)} (hV : Valid q h P c tab R padres) {r : ℕ} {d t a b A B : ℤ} (he : (r, d, t) ∈ tab) (hU : inU a b) (hA : A = a + d) (hstep : ↑q * B = b - t - a * ↑r) (hH : inH A B) : inH a b

Backward closure of the rays H relative to U.

theorem SegmentoIISinCeros.back {q : ℕ} {h P : ℤ} {c : ℕ} {tab : List (ℕ × ℤ × ℤ)} {R padres : List (ℤ × ℤ)} (hV : Valid q h P c tab R padres) {r : ℕ} {d t a b A B : ℤ} (he : (r, d, t) ∈ tab) (hU : inU a b) (hA : A = a + d) (hstep : ↑q * B = b - t - a * ↑r) (hW : inW R A B) : inW R a b

Backward closure of R ∪ H relative to U.

§4 Valid certificate ⇒ no positive zero

theorem SegmentoIISinCeros.no_zero_of_valid (q : ℕ) (hq : 2 ≤ q) (χ : ℕ → ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hleg : ∀ (n : ℕ), n % q ≠ 0 → χ n = leg q n) (hχq : χ q = 1) {h P : ℤ} {c : ℕ} {tab : List (ℕ × ℤ × ℤ)} {R padres : List (ℤ × ℤ)} (hV : Valid q h P c tab R padres) (m : ℕ) (hm : 0 < m) : SegmentoII.S χ m ≠ 0

§5 Data and the kernel-checked certificates

def SegmentoIISinCeros.R179 : List (ℤ × ℤ)

Equations

• One or more equations did not get rendered due to their size.

def SegmentoIISinCeros.padres179 : List (ℤ × ℤ)

Equations

• SegmentoIISinCeros.padres179 = [(-10, 5), (-6, 1), (-4, 2), (-3, 0), (-3, 2), (-2, 1), (-2, 2), (-1, 0), (1, -1), (1, 0), (2, -2), (2, 0), (5, -5)]

def SegmentoIISinCeros.R227 : List (ℤ × ℤ)

Equations

• One or more equations did not get rendered due to their size.

def SegmentoIISinCeros.padres227 : List (ℤ × ℤ)

Equations

• SegmentoIISinCeros.padres227 = [(-10, 5), (-7, 1), (-6, 2), (-6, 3), (-3, 0), (-3, 1), (-2, 2), (-1, 0), (5, -5), (7, -4)]

def SegmentoIISinCeros.tab179 : List (ℕ × ℤ × ℤ)

Equations

• One or more equations did not get rendered due to their size.

def SegmentoIISinCeros.tab227 : List (ℕ × ℤ × ℤ)

Equations

• One or more equations did not get rendered due to their size.

theorem SegmentoIISinCeros.valid179 : Valid 179 5 7 89 tab179 R179 padres179

theorem SegmentoIISinCeros.valid227 : Valid 227 5 8 113 tab227 R227 padres227

theorem SegmentoIISinCeros.S_ne_zero_179 (χ : ℕ → ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hleg : ∀ (n : ℕ), n % 179 ≠ 0 → χ n = leg 179 n) (hq : χ 179 = 1) (m : ℕ) (hm : 1 ≤ m) : SegmentoII.S χ m ≠ 0

No positive zero, q = 179.

theorem SegmentoIISinCeros.S_ne_zero_227 (χ : ℕ → ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hleg : ∀ (n : ℕ), n % 227 ≠ 0 → χ n = leg 227 n) (hq : χ 227 = 1) (m : ℕ) (hm : 1 ≤ m) : SegmentoII.S χ m ≠ 0

No positive zero, q = 227.

§6 Negative controls: the checker can fail

q = 59 has positive zeros; its backward set R59 (|R| = 43) contains the origin, and deleting the origin breaks closure. Corrupting one point of R179 or one table entry also makes the checker answer false.

def SegmentoIISinCeros.tab59 : List (ℕ × ℤ × ℤ)

Equations

• One or more equations did not get rendered due to their size.

def SegmentoIISinCeros.R59 : List (ℤ × ℤ)

Equations

• One or more equations did not get rendered due to their size.

def SegmentoIISinCeros.padres59 : List (ℤ × ℤ)

Equations

• SegmentoIISinCeros.padres59 = [(-6, 3), (-4, 1), (-2, 1), (-1, 0), (3, -3)]

§7 Bridge to Mathlib's legendreSym, and non-vacuity

theorem SegmentoIISinCeros.leg_eq_legendreSym (q : ℕ) [hq : Fact (Nat.Prime q)] (hq2 : q ≠ 2) (n : ℕ) (hn : n % q ≠ 0) : leg q n = legendreSym q ↑n

leg is Mathlib's Legendre symbol off the multiples of q (Euler's criterion).

def SegmentoIISinCeros.chi0 (q n : ℕ) : ℤ

The completely multiplicative extension: χ₀ n = leg q (n / q^{v_q(n)}), χ₀ 0 = 0.

Equations

• SegmentoIISinCeros.chi0 q n = if n = 0 then 0 else SegmentoIISinCeros.leg q (n / q ^ n.factorization q)

theorem SegmentoIISinCeros.chi0_spec (q : ℕ) [hq : Fact (Nat.Prime q)] (hq2 : q ≠ 2) : (∀ (a b : ℕ), chi0 q (a * b) = chi0 q a * chi0 q b) ∧ (∀ (n : ℕ), n % q ≠ 0 → chi0 q n = leg q n) ∧ chi0 q q = 1

Non-vacuity: chi0 q satisfies the hypotheses of the main theorem.

instance SegmentoIISinCeros.instFactPrimeOfNatNat_formalizations : Fact (Nat.Prime 179)

instance SegmentoIISinCeros.instFactPrimeOfNatNat_formalizations_1 : Fact (Nat.Prime 227)

theorem SegmentoIISinCeros.S_ne_zero_179_legendreSym (χ : ℕ → ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hleg : ∀ (n : ℕ), ¬179 ∣ n → χ n = legendreSym 179 ↑n) (hq : χ 179 = 1) (m : ℕ) (hm : 1 ≤ m) : SegmentoII.S χ m ≠ 0

No positive zero, q = 179, stated with Mathlib's legendreSym.

theorem SegmentoIISinCeros.S_ne_zero_227_legendreSym (χ : ℕ → ℤ) (hmul : ∀ (a b : ℕ), χ (a * b) = χ a * χ b) (hleg : ∀ (n : ℕ), ¬227 ∣ n → χ n = legendreSym 227 ↑n) (hq : χ 227 = 1) (m : ℕ) (hm : 1 ≤ m) : SegmentoII.S χ m ≠ 0

No positive zero, q = 227, stated with Mathlib's legendreSym.

theorem SegmentoIISinCeros.S_chi0_ne_zero_179 (m : ℕ) (hm : 1 ≤ m) : SegmentoII.S (chi0 179) m ≠ 0

The hypotheses are satisfiable: the theorem applies to the explicit chi0 179.

theorem SegmentoIISinCeros.S_chi0_ne_zero_227 (m : ℕ) (hm : 1 ≤ m) : SegmentoII.S (chi0 227) m ≠ 0

The hypotheses are satisfiable: the theorem applies to the explicit chi0 227.