FormalConjectures.OEIS.«317940»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Nonnegativity of the Dirichlet square root of A046644

A317940 is the integer sequence whose value a n is the numerator of the rational sequence f n, where the Dirichlet convolution square of f is A046644. The auxiliary sequence A046644 is multiplicative and takes the value $2^{\operatorname{A005187}(e)}$ on a prime power $p^e$.

The conjecture asks whether f n is nonnegative for every positive n. The proof reduces the problem to prime powers and constructs positive rational coefficients $c(e)$ satisfying

$$\sum_{i=0}^e c(i)c(e-i)=2^{\operatorname{A005187}(e)}.$$

The coefficients are obtained from formal power series. A positive series $A$ is defined by the first-order differential equation $A' = \frac12 D A$. A second explicitly defined series $B$ satisfies $B' = D B$ and has the same constant term as $A^2$; uniqueness of the coefficient recurrence therefore gives $A^2=B$. After rescaling the coefficients by $4^e$, this becomes the displayed prime-power convolution identity.

Extending $c(e)$ multiplicatively over prime factorizations gives a positive arithmetic function root with root * root = a046644. Finally, the recursive definition of f is shown to be the unique Dirichlet square root with value one at $1$, so f = root and every positive-index value of f is positive.

This route was found by first exploiting the multiplicativity recorded in the OEIS entry, reducing the recurrence to the exponent of a single prime, and then recognizing the resulting coefficient identities as a formal-power-series differential equation.

References:

A317940

A046644

A005187

namespace OeisA317940open Nat Finset

A005187: the sum of $\lfloor e / 2^k \rfloor$ over $k \ge 0$.

noncomputable def a005187 (e : ℕ) : ℕ :=
  Finset.sum (Finset.range (e + 1)) fun k ↦ e / (2 ^ k)

A046644: the multiplicative function whose value at each prime power $p^e$ is $2^{\operatorname{A005187}(e)}$.

noncomputable def a046644 (n : ℕ) : ℚ :=
  if n = 0 then 0
  else n.factorization.prod fun _ e ↦ (2 : ℚ) ^ (a005187 e)

The rational sequence whose Dirichlet convolution square is A046644, written using the defining recurrence from the OEIS entry.

noncomputable def f : ℕ → ℚ :=
  WellFounded.fix (measure id).wf fun n IH ↦
    if n = 0 then 0
    else if n = 1 then 1
    else
      let target : ℚ := a046644 n
      let interiorSum : ℚ := Finset.sum (divisors n) fun d ↦
        if h : d > 1 ∧ d < n then
          have d_lt_n : d < n := h.2
          let q := n / d
          have q_lt_n : q < n := Nat.div_lt_self (Nat.pos_of_ne_zero (byn:ℕIH:(y : ℕ) → WellFoundedRelation.rel y n → ℚtarget:ℚ := a046644 nd:ℕh:d > 1 ∧ d < nd_lt_n:d < nq:ℕ := n / d⊢ n ≠ 0 omegaAll goals completed! 🐙)) h.1
          IH d d_lt_n * IH q q_lt_n
        else 0
      (target - interiorSum) / 2

A317940: the numerator of f n.

noncomputable def a (n : ℕ) : ℤ :=
  (f n).num

The defining recurrence of f, with the recursive calls folded back to f.

@[category API, AMS 11]
private lemma f_eq (n : ℕ) :
    f n = if n = 0 then 0 else if n = 1 then 1 else
      (a046644 n -
        ∑ d ∈ n.divisors, if _h : 1 < d ∧ d < n then f d * f (n / d) else 0) / 2 := byn:ℕ⊢ f n =
  if n = 0 then 0
  else if n = 1 then 1 else (a046644 n - ∑ d ∈ n.divisors, if _h : 1 < d ∧ d < n then f d * f (n / d) else 0) / 2
  conv_lhs => rw [f, WellFounded.fix_eq]n:ℕ| if n = 0 then 0
else
  if n = 1 then 1
  else
    have target := a046644 n;
    have interiorSum :=
      ∑ d ∈ n.divisors,
        if h : d > 1 ∧ d < n then
          have d_lt_n := ⋯;
          let q := n / d;
          have q_lt_n := ⋯;
          (fun y x ↦
                f._proof_2.fix
                  (fun n IH ↦
                    if n = 0 then 0
                    else
                      if n = 1 then 1
                      else
                        have target := a046644 n;
                        have interiorSum :=
                          ∑ d ∈ n.divisors,
                            if h : d > 1 ∧ d < n then
                              have d_lt_n := ⋯;
                              let q := n / d;
                              have q_lt_n := ⋯;
                              IH d d_lt_n * IH q q_lt_n
                            else 0;
                        (target - interiorSum) / 2)
                  y)
              d d_lt_n *
            (fun y x ↦
                f._proof_2.fix
                  (fun n IH ↦
                    if n = 0 then 0
                    else
                      if n = 1 then 1
                      else
                        have target := a046644 n;
                        have interiorSum :=
                          ∑ d ∈ n.divisors,
                            if h : d > 1 ∧ d < n then
                              have d_lt_n := ⋯;
                              let q := n / d;
                              have q_lt_n := ⋯;
                              IH d d_lt_n * IH q q_lt_n
                            else 0;
                        (target - interiorSum) / 2)
                  y)
              q q_lt_n
        else 0;
    (target - interiorSum) / 2
  rflAll goals completed! 🐙



@[category API, AMS 11]
private lemma f_one : f 1 = 1 := by⊢ f 1 = 1
  rw [f_eq⊢ (if 1 = 0 then 0
  else if 1 = 1 then 1 else (a046644 1 - ∑ d ∈ divisors 1, if _h : 1 < d ∧ d < 1 then f d * f (1 / d) else 0) / 2) =
  1⊢ (if 1 = 0 then 0
  else if 1 = 1 then 1 else (a046644 1 - ∑ d ∈ divisors 1, if _h : 1 < d ∧ d < 1 then f d * f (1 / d) else 0) / 2) =
  1]⊢ (if 1 = 0 then 0
  else if 1 = 1 then 1 else (a046644 1 - ∑ d ∈ divisors 1, if _h : 1 < d ∧ d < 1 then f d * f (1 / d) else 0) / 2) =
  1; norm_numAll goals completed! 🐙

At a prime p every divisor is 1 or p, so the interior sum is empty.


@[category API, AMS 11]
private lemma f_prime {p : ℕ} (hp : p.Prime) : f p = a046644 p / 2 := byp:ℕhp:Nat.Prime p⊢ f p = a046644 p / 2
  rw [f_eq,p:ℕhp:Nat.Prime p⊢ (if p = 0 then 0
  else if p = 1 then 1 else (a046644 p - ∑ d ∈ p.divisors, if _h : 1 < d ∧ d < p then f d * f (p / d) else 0) / 2) =
  a046644 p / 2p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0 if_neg hp.ne_zero,p:ℕhp:Nat.Prime p⊢ (if p = 1 then 1 else (a046644 p - ∑ d ∈ p.divisors, if _h : 1 < d ∧ d < p then f d * f (p / d) else 0) / 2) =
  a046644 p / 2p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0 if_neg hp.ne_one,p:ℕhp:Nat.Prime p⊢ (a046644 p - ∑ d ∈ p.divisors, if _h : 1 < d ∧ d < p then f d * f (p / d) else 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0
    Finset.sum_eq_zero (fun x hx => ?_)p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0]p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0
  ·p:ℕhp:Nat.Prime p⊢ (a046644 p - 0) / 2 = a046644 p / 2 ringAll goals completed! 🐙
  ·p:ℕhp:Nat.Prime px:ℕhx:x ∈ p.divisors⊢ (if _h : 1 < x ∧ x < p then f x * f (p / x) else 0) = 0 rcases hp.eq_one_or_self_of_dvd x (Nat.mem_divisors.mp hx).1 with rfl | rflinlp:ℕhp:Nat.Prime phx:1 ∈ p.divisors⊢ (if _h : 1 < 1 ∧ 1 < p then f 1 * f (p / 1) else 0) = 0inrx:ℕhp:Nat.Prime xhx:x ∈ x.divisors⊢ (if _h : 1 < x ∧ x < x then f x * f (x / x) else 0) = 0
    ·inlp:ℕhp:Nat.Prime phx:1 ∈ p.divisors⊢ (if _h : 1 < 1 ∧ 1 < p then f 1 * f (p / 1) else 0) = 0 exact dif_neg (byp:ℕhp:Nat.Prime phx:1 ∈ p.divisors⊢ ¬(1 < 1 ∧ 1 < p) omegaAll goals completed! 🐙)
    ·inrx:ℕhp:Nat.Prime xhx:x ∈ x.divisors⊢ (if _h : 1 < x ∧ x < x then f x * f (x / x) else 0) = 0 exact dif_neg (byx:ℕhp:Nat.Prime xhx:x ∈ x.divisors⊢ ¬(1 < x ∧ x < x) omegaAll goals completed! 🐙)



@[category API, AMS 11]
private lemma f_two : f 2 = 1 := by⊢ f 2 = 1
  rw [f_prime Nat.prime_two⊢ a046644 2 / 2 = 1⊢ a046644 2 / 2 = 1]⊢ a046644 2 / 2 = 1; norm_num [a046644, a005187]All goals completed! 🐙



@[category API, AMS 11]
private lemma f_three : f 3 = 1 := by⊢ f 3 = 1
  rw [f_prime Nat.prime_three⊢ a046644 3 / 2 = 1⊢ a046644 3 / 2 = 1]⊢ a046644 3 / 2 = 1; norm_num [a046644, a005187]All goals completed! 🐙



@[category API, AMS 11]
private lemma f_five : f 5 = 1 := by⊢ f 5 = 1
  rw [f_prime (by⊢ Nat.Prime 5⊢ a046644 5 / 2 = 1 norm_numAll goals completed! 🐙⊢ a046644 5 / 2 = 1)]⊢ a046644 5 / 2 = 1; norm_num [a046644, a005187]All goals completed! 🐙

4 = 2 ^ 2 is the only case here with a nonempty interior sum, contributing f 2 * f 2.


@[category API, AMS 11]
private lemma f_four : f 4 = 7 / 2 := by⊢ f 4 = 7 / 2
  rw [f_eq 4⊢ (if 4 = 0 then 0
  else if 4 = 1 then 1 else (a046644 4 - ∑ d ∈ divisors 4, if _h : 1 < d ∧ d < 4 then f d * f (4 / d) else 0) / 2) =
  7 / 2⊢ (if 4 = 0 then 0
  else if 4 = 1 then 1 else (a046644 4 - ∑ d ∈ divisors 4, if _h : 1 < d ∧ d < 4 then f d * f (4 / d) else 0) / 2) =
  7 / 2]⊢ (if 4 = 0 then 0
  else if 4 = 1 then 1 else (a046644 4 - ∑ d ∈ divisors 4, if _h : 1 < d ∧ d < 4 then f d * f (4 / d) else 0) / 2) =
  7 / 2
  norm_num only⊢ (if False then 0
  else if False then 1 else (a046644 4 - ∑ d ∈ divisors 4, if _h : 1 < d ∧ d < 4 then f d * f (4 / d) else 0) / 2) =
  7 / 2
  rw [show (Nat.divisors 4) = {1, 2, 4} from rfl,⊢ (if False then 0
  else if False then 1 else (a046644 4 - ∑ d ∈ {1, 2, 4}, if _h : 1 < d ∧ d < 4 then f d * f (4 / d) else 0) / 2) =
  7 / 2⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8
    Finset.sum_insert (by⊢ 1 ∉ {2, 4}⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8 decideAll goals completed! 🐙⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8), Finset.sum_insert (by⊢ 2 ∉ {4}⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8 decideAll goals completed! 🐙⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8), Finset.sum_singleton,⊢ (if False then 0
  else
    if False then 1
    else
      (a046644 4 -
          ((if _h : 1 < 1 ∧ 1 < 4 then f 1 * f (4 / 1) else 0) +
            ((if _h : 1 < 2 ∧ 2 < 4 then f 2 * f (4 / 2) else 0) +
              if _h : 1 < 4 ∧ 4 < 4 then f 4 * f (4 / 4) else 0))) /
        2) =
  7 / 2⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8
    dif_neg (by⊢ ¬(1 < 1 ∧ 1 < 4)⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8 omegaAll goals completed! 🐙⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8), dif_pos (by⊢ 1 < 2 ∧ 2 < 4⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8 omegaAll goals completed! 🐙⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8), dif_neg (by⊢ ¬(1 < 4 ∧ 4 < 4)⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8 omegaAll goals completed! 🐙⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8),
    show a046644 4 = 8 from ?_⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8]⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2⊢ a046644 4 = 8
  ·⊢ (if False then 0 else if False then 1 else (8 - (0 + (f 2 * f (4 / 2) + 0))) / 2) = 7 / 2 rw [f_two⊢ (if False then 0 else if False then 1 else (8 - (0 + (1 * 1 + 0))) / 2) = 7 / 2⊢ (if False then 0 else if False then 1 else (8 - (0 + (1 * 1 + 0))) / 2) = 7 / 2]⊢ (if False then 0 else if False then 1 else (8 - (0 + (1 * 1 + 0))) / 2) = 7 / 2; norm_numAll goals completed! 🐙
  ·⊢ a046644 4 = 8 rw [a046644,⊢ (if 4 = 0 then 0 else (Nat.factorization 4).prod fun x e ↦ 2 ^ a005187 e) = 8⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8 if_neg (by⊢ ¬4 = 0⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8 norm_numAll goals completed! 🐙⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8), show (4 : ℕ) = 2 ^ 2 by⊢ f 4 = 7 / 2⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8 norm_numAll goals completed! 🐙⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8,
      Nat.Prime.factorization_pow Nat.prime_two⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8]⊢ ((fun₀ | 2 => 2).prod fun x e ↦ 2 ^ a005187 e) = 8
    norm_num [Finsupp.prod_single_index, a005187, Finset.sum_range_succ]All goals completed! 🐙

f 1 = 1 is the base case of the recurrence, so a 1 = 1.


@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1
  rw [a,⊢ (f 1).num = 1⊢ Rat.num 1 = 1 f_one⊢ Rat.num 1 = 1⊢ Rat.num 1 = 1]⊢ Rat.num 1 = 1
  rflAll goals completed! 🐙

2 is prime, so the interior sum is empty and f 2 = a046644 2 / 2 = 1.


@[category test, AMS 11]
theorem a_2 : a 2 = 1 := by⊢ a 2 = 1
  rw [a,⊢ (f 2).num = 1⊢ Rat.num 1 = 1 f_two⊢ Rat.num 1 = 1⊢ Rat.num 1 = 1]⊢ Rat.num 1 = 1
  rflAll goals completed! 🐙

3 is prime, so the interior sum is empty and f 3 = a046644 3 / 2 = 1.


@[category test, AMS 11]
theorem a_3 : a 3 = 1 := by⊢ a 3 = 1
  rw [a,⊢ (f 3).num = 1⊢ Rat.num 1 = 1 f_three⊢ Rat.num 1 = 1⊢ Rat.num 1 = 1]⊢ Rat.num 1 = 1
  rflAll goals completed! 🐙

4 is the first index with a nonempty interior sum, giving f 4 = 7 / 2.


@[category test, AMS 11]
theorem a_4 : a 4 = 7 := by⊢ a 4 = 7
  rw [a,⊢ (f 4).num = 7⊢ (7 / 2).num = 7 f_four⊢ (7 / 2).num = 7⊢ (7 / 2).num = 7]⊢ (7 / 2).num = 7
  norm_numAll goals completed! 🐙

5 is prime, so the interior sum is empty and f 5 = a046644 5 / 2 = 1.


@[category test, AMS 11]
theorem a_5 : a 5 = 1 := by⊢ a 5 = 1
  rw [a,⊢ (f 5).num = 1⊢ Rat.num 1 = 1 f_five⊢ Rat.num 1 = 1⊢ Rat.num 1 = 1]⊢ Rat.num 1 = 1
  rflAll goals completed! 🐙

"No negative terms among the first 2^20 terms. Is the sequence nonnegative?"

Equivalently, the rational Dirichlet square root f is nonnegative at every positive index. Informally, the proof constructs a strictly positive multiplicative square root prime-power by prime-power using formal power series, and then identifies it with the recursively defined sequence f.

The proof was obtained by exploiting the multiplicativity of A046644 and reducing the problem to its values on prime powers. The resulting convolution recurrence for the prime-power coefficients was recognized as a formal-power-series identity. A positive coefficient sequence was constructed through a differential equation for the generating series, extended multiplicatively to all positive integers, and finally identified with the recursively defined Dirichlet square root by uniqueness.

@[category research solved, AMS 11,
  formal_proof using lean4 at
    "https://domthedeveloper.github.io/crl/math/a317940/proof/A317940_verified.lean"]
theorem f_nonnegative (n : ℕ) (h : n > 0) : f n ≥ 0 := byn:ℕh:n > 0⊢ f n ≥ 0
  sorryAll goals completed! 🐙

end OeisA317940