Proving $\sum_{k=1}^n\vert\cos(k)\vert\ge \frac{n}{4}$ for all $n>0$ 
Show that for all $n\in\mathbb{N}^* \quad \sum_{k=1}^n\vert\cos(k)\vert\ge \frac{n}{4}.$

I can do it using the fact that $\vert\cos(x)\vert\ge \cos(x)^2$
\begin{equation}
\sum_{k=1}^n\vert\cos(k)\vert\ge \sum_{k=1}^n\cos(k)^2=\frac{n}{2}+\frac1{2}\Re\big(e^{2i}\frac{1-e^{2in}}{1-e^{2i}}\big)\\
=\frac{n}{2}+\frac{1}{2}\Re\big(e^{i(n+1)}\frac{\sin(n)}{\sin{1}}\big)=\frac{n}{2}+\frac{\cos(n+1)\sin(n)}{2\sin(1)}\ge\frac{n}{2}-\frac{1}{2\sin(1)}
\end{equation}
I can finish by using "calculator" or by hand but I would rather like a "direct" proof not using the value of $\sin(1).$
Other methods can be very interesting too.
 A: You do not need great accuracy for $\sin 1$. In fact, to show
$$ \frac n2-\frac1{2\sin1}\ge \frac n4$$
it suffices to have $$ n\ge \frac2{\sin1}.$$
From $\pi<4$, we have $\sin1>\sin\frac\pi4=\frac12\sqrt 2$, and hance are doen for all $n\ge 2\sqrt2$, so (as $\sqrt 2<\sqrt{\frac 94}=\frac32$) certainly for all $n\ge3$. A high precision calculator would not have helped you better than that.
For $n=2$, the claim is $|\cos 1|+|\cos 2|\ge \frac12$ and for $n=1$, it is $|\cos 1|\ge \frac14$. This time we use $1<\frac\pi 3$, hence $\cos 1>\cos\frac\pi3=\frac12$.
A: Since
$$ \left|\cos x\right|=\frac{2}{\pi}+\frac{4}{\pi}\sum_{m\geq 1}\frac{\cos(2mx)(-1)^{m+1}}{4m^2-1} $$
and
$$ \left|\sum_{n=1}^{N}\cos(2mn)\right|\leq \frac{1}{\left|\sin m\right|}\leq \frac{\pi/2}{d(m,\pi\mathbb{Z})} $$
we have
$$ \left|-\frac{2n}{\pi}+\sum_{k=1}^{n}\left|\cos k\right|\right|\leq \frac{1}{2}\sum_{m\geq 1}\frac{1}{(4m^2-1)\,d(m,\pi\mathbb{Z})}. \tag{A}$$
Once we prove that the series in the RHS of $(A)$ is convergent we have $\sum_{k=1}^{n}\left|\cos k\right|=\frac{2n}{\pi}+O(1)$, which is way stronger than the original inequality. Now $m^2\,d(m,\pi\mathbb{Z})$ may be as small as $\Theta(m)$, but by Lagrange's theorem that happens iff $m$ is the numerator of a convergent of $\pi$, i.e. an element of the sequence $\{\eta_n\}_{n\geq 1}=\{3,22,333,355,103993,\ldots\}$. Since $\pi$ is irrational this sequence has at least an exponential growth and the series $\sum_{n\geq 1}\frac{1}{\eta_n}$ is convergent. As a consequence, the RHS of $(A)$ is convergent too. An approximated value for it is $0.6$. Here it is a graph of the LHS of $(A)$ for $n\in[1,1000]$:
$\hspace{1cm}$
A: I shall prove that
$$\sum_{k=1}^n\,\big|\cos(k)\big|>\frac{n}{2}\tag{*}$$
for all $n\geq 3$.  For $n=3$, you can simply use some software, or make some clever close estimates of $\cos(1)$, $\cos(2)$, and $\cos(3)$ to finish the job.  For $n\geq 4$, I shall refer to the OP's work, with a small twist:
$$\begin{align}\sum_{k=1}^n\,\big|\cos(k)\big|&\geq \sum_{k=1}^n\,\cos^2(k)+\sum_{k=1}^4\,\Big(\big|\cos(k)\big|-\cos^2(k)\Big)\\&\geq \frac{n}{2}-\frac{1}{2\sin(1)}+\sum_{k=1}^4\,\Big(\big|\cos(k)\big|-\cos^2(k)\Big)\,,\end{align}$$
where I have applied exactly the same idea as the OP's marvellous work.  Now, it can be seen (via using software or making good approximations) that
$$\sum_{k=1}^4\,\Big(\big|\cos(k)\big|-\cos^2(k)\Big)>\frac{1}{2\sin(1)}\,.$$
That is, (*) holds for all $n\geq 4$ as well.  (In fact, (*) holds for every positive integer $n$ except when $n=2$.)
In fact, we have
$$\lim_{n\to\infty}\,\frac1n\,\sum_{k=1}^n\,\big|\cos(k)\big|=\frac{2}{\pi}\,.$$
Thus, for any positive real number $r<\dfrac{2}{\pi}$, there exists a positive integer $N_r$ such that
$$\sum_{k=1}^n\,\big|\cos(k)\big|>rn$$
for every integer $n\geq N_r$.  As you can see, $N_{1/4}=1$ and $N_{1/2}=3$.  Likewise, for any real number $s>\dfrac{2}{\pi}$, there exists a positive integer $M_s$ such that $$\sum_{k=1}^n\,\big|\cos(k)\big|<sn$$
for every integer $n\geq M_s$.  (Well, we have this obvious result: $M_s=1$ for all $s\geq 1$.  A less obvious result is $M_{3/4}=1$.)
