About the inequality $x^{x^{x^{x^{x^x}}}} \ge \frac12 x^2 + \frac12$ 
Problem: Let $x > 0$. Prove that
$$x^{x^{x^{x^{x^x}}}} \ge \frac12 x^2 + \frac12.$$

Remark 1: The problem was posted on MSE (now closed).
Remark 2: I have a proof (see below). My proof is not nice.
For example, we need to prove that
$\frac{3x^2 - 3}{x^2 + 4x + 1} + \frac{12}{7} - \frac{24x^{17/12}}{7x^2 + 7} \le 0$ for all $0 < x < 1$ for which my proof is not nice.
I want to know if there are some nice proofs. Also, I want my proof reviewed for its correctness.
Any comments and solutions are welcome and appreciated.
My proof (sketch):
We split into cases:
i) $x \ge 1$:
Clearly, $x^{x^{x^{x^{x^x}}}}\ge x^x$.
By Bernoulli's inequality, we have
$x^x = (1 + (x - 1))^x \ge 1 + (x - 1)x = x^2 - x + 1 \ge \frac12 x^2 + \frac12$. The inequality is true.
ii) $0 < x < 1$:
It suffices to prove that
$$x^{x^{x^{x^x}}}\ln x \ge \ln \frac{x^2 + 1}{2}$$
or
$$x^{x^{x^{x^x}}} \le \frac{\ln \frac{x^2 + 1}{2}}{\ln x}$$
or
$$x^{x^{x^x}}\ln x \le \ln \frac{\ln \frac{x^2 + 1}{2}}{\ln x}$$
or
$$x^{x^{x^x}}\ge \frac{1}{\ln x}\ln \frac{\ln \frac{x^2 + 1}{2}}{\ln x}.$$
It suffices to prove that
$$x^{x^{x^x}}\ge \frac{7}{12} \ge \frac{1}{\ln x}\ln \frac{\ln \frac{x^2 + 1}{2}}{\ln x}. \tag{1}$$
First, it is easy to prove that $$x^x \ge \mathrm{e}^{-1/\mathrm{e}}
\ge \frac{1}{\ln x}\ln\frac{\ln\frac{7}{12}}{\ln x}.$$
Thus, the left inequality in (1) is true.
Second, let $f(x) = x^{7/12}\ln x - \ln \frac{x^2 + 1}{2}$. We have
\begin{align*}
 f'(x) &= \frac{7}{12x^{5/12}}
 \left(\ln x + \frac{12}{7} - \frac{24x^{17/12}}{7x^2 + 7}\right)\\
 &\le \frac{7}{12x^{5/12}}
 \left(\frac{3x^2 - 3}{x^2 + 4x + 1} + \frac{12}{7} - \frac{24x^{17/12}}{7x^2 + 7}\right)\\
 &\le 0 \tag{2}
\end{align*}
where we have used
$\ln x \le \frac{3x^2 - 3}{x^2 + 4x + 1}$ for all $x$ in $(0, 1]$.
Also, $f(1) = 0$. Thus, $f(x) \ge 0$ for all $x$ in $(0, 1)$.
Thus, the right inequality in (1) is true.
Note: For the inequality $\frac{3x^2 - 3}{x^2 + 4x + 1} + \frac{12}{7} - \frac{24x^{17/12}}{7x^2 + 7} \le 0$ for all $0 < x < 1$,
we let $x = y^{12}$ and it suffices to prove that
$11y^{47} + \cdots + 3 \ge 0$ (a polynomial of degree $47$, a long expression) for all $0 < y < 1$.
We are done.
 A: A  partial answer

First Fact :
For $x\in(0,1)$ we have :
$$x^{x^{x^{x^{x^{x}}}}}\geq x^{x^{x}}$$
Proof: see the Reference in my other answer .

Second Fact
For $x\in(0,1)$ we have :
$$ x^{x^{x}}\geq x^{\left(1+\left(x-1\right)x\right)}$$
Hint :use Bernoulli's inequality.

Third Fact
For $x\in[0.65,1]$ we have :
$$x^{\left(1+\left(x-1\right)x\right)}\geq b(x)=\left(x\left(1+\left(x-1\right)\cdot\left(\left(x-1\right)x\right)+0.5\left(x-1\right)^{2}\cdot\left(\left(x-1\right)x\right)\cdot\left(\left(\left(x-1\right)x\right)-1\right)\right)\right)$$
Rewrite $x^{\left(1+\left(x-1\right)x\right)}=xx^{\left(\left(x-1\right)x\right)}$ and use the binomial theorem for $p(x)=x^a$ at $x=1$ .We stop the power series at the second order .
Remains to show :
$$0.5 (x - 1)^2 (x^5 - 2 x^4 + 3 x^2 - 1)=b(x)-0.5x^2-0.5\geq0$$
Or
$$(x^5 - 2 x^4 + 3 x^2 - 1)\geq 0$$
Wich is left to the reader and easy using derivatives .

A lemma :
We have for $a,x\in(0,1)$:
$$x^{a^{a^{1.86a\left(1+a\left(a-1\right)\right)}}}\leq x^{a^{a^{a^{a^{a}}}}}\quad\quad(I)$$
Wich is a refinement if $x=a$
The inequality $(I)$ is equivalent to :
$$a^{a^{a}}\leq 1.86a\left(1+a\left(a-1\right)\right)$$
It seems that we have for $a\in(0.03,1)$
$$a^{a^{a}}\leq a^{0.86\left(1+\left(a-1\right)a\right)} \leq 1.87a\left(1+a\left(a-1\right)\right)$$
We start from :
$$a^{a^{a}}\leq a^{0.86\left(1+\left(a-1\right)a\right)}$$
Wich is equivalent to :
$$a^{a}\geq 0.86\left(1+\left(a-1\right)a\right)$$
The function $f(a)=a^{a}$ is convex so we have :
$$f(x)\geq f'(b)(x-b)+f(b)$$
Remains to choose judicious points wich is not hard using a graphic  so I let it  to the reader .
Also see the reference .
Now we start from :
$$a^{0.86\left(1+\left(a-1\right)a\right)} \leq 1.87a\left(1+a\left(a-1\right)\right)$$

A trick is : put $a$ in exponent on both side and the inequality have the form :
$$(1.87u)^v\geq v^{0.86u}$$
The inequality in $u,v$ reminds me the inequality :
Let $a,b>0$ and $k\in(0,1)$ then we have :
$$a(1-k)+bk\geq a^{1-k}b^{k}$$
Using this we have :
$$\left(1.87u\left(x\right)\right)^{-1}\left(v\left(x\right)^{\left(\frac{x}{\left(0.86u\left(x\right)\right)}\right)^{-1}}\left(x\right)+u\left(x\right)\cdot1.87\cdot\left(1-x\right)\right)\geq \left(\left(1.87u\left(x\right)\right)^{-x}\right)x^{\left(0.86u\left(x\right)\right)}$$
Where :
$$u(x)=x\left(1+\left(x-1\right)x\right)$$ and : $$v(x)=x$$ and $x\in(0.03,1)$

The rest is smooth using the lemma 7.1 (p.136 see the first reference for that) .
End lemma

Second lemma
Let $a,x\in(0,1)$ then we have :
$$x^{a^{\frac{7}{12}}}\leq x^{a^{a^{1.87a\left(1+\left(a-1\right)a\right)}}}$$
Proof :
It's equivalent to :
$$a^{1.87a\left(1+\left(a-1\right)a\right)}\geq \frac{7}{12}$$
The function :
$$n(a)=a^{1.87a\left(1+\left(a-1\right)a\right)}$$
Is convex on $(0,1)$ so admits a global minimum on $(0,1)$. The rest is smooth again !

End Second lemma
Remains to show for $x,a\in(0,1)$ and $x\geq a$:
$$0.5a^{2}+0.5\leq x^{a^{\frac{7}{12}}}$$
I pursue it later thanks for advices or comments !
Reference :
Vasile Cirtoaje, "Proofs of three open inequalities with power-exponential functions",
The Journal of Nonlinear Sciences and its Applications (2011), Volume: 4, Issue: 2, page 130-137.
https://eudml.org/doc/223938
https://www.planetmath.org/convexfunctionslieabovetheirsupportinglines
A: Remarks: @Erik Satie considered $^6 x \ge \lim_{n\to \infty} {^n}x = -\frac{W(-\ln x)}{\ln x}$ for $(38/100, 1)$. I gave alternative
proof of $-\frac{W(-\ln x)}{\ln x} \ge \frac12 x^2 + \frac12$ for all $x$ in $(38/100, 1)$.

Case $x \in (38/100, 1)$:
According to Theorem in [1] (Page 240), we have
$\lim_{n\to \infty} {^n}x = -\frac{W(-\ln x)}{\ln x}$
where $W(\cdot)$ is the principal branch of the Lambert W function. Also, we have $^6 x \ge {^8}x
\ge {^{10}}x \ge \cdots$ which results in
$^6 x \ge \lim_{n\to \infty} {^n}x = -\frac{W(-\ln x)}{\ln x}$.
Let us prove that
$-\frac{W(-\ln x)}{\ln x} \ge \frac12 x^2 + \frac12$ for all $x$ in $(38/100, 1)$.
To this end, with the substitution $x = \mathrm{e}^{-y}$ for $y\in (0, -\ln\frac{38}{100})$, we need to prove that
$$\frac{W(y)}{y} \ge \frac12 \mathrm{e}^{-2y} + \frac12$$
or
$$W(y) \ge \frac12 y\mathrm{e}^{-2y} + \frac12 y.$$
Since $u \mapsto u\mathrm{e}^u$ is strictly increasing on $(0, \infty)$, it suffices to prove that
$$W(y)\mathrm{e}^{W(y)} \ge \left(\frac12 y\mathrm{e}^{-2y} + \frac12 y\right)
\mathrm{exp}\left({\frac12 y\mathrm{e}^{-2y} + \frac12 y}\right)$$
that is
$$y \ge \left(\frac12 y\mathrm{e}^{-2y} + \frac12 y\right)
\mathrm{exp}\left({\frac12 y\mathrm{e}^{-2y} + \frac12 y}\right)$$
where we have used the fact $W(y)\mathrm{e}^{W(y)} = y$ for all $y > 0$.
With the substitution $z = \mathrm{e}^{-2y}$, it suffices to prove that, for all $z$ in $(38^2/100^2, 1)$,
$$0 \ge \ln \frac{1 + z}{2} - \frac{1 + z}{4}\ln z.$$
The remaining is smooth.

Reference
[1] R. Arthur Knoebel, “Exponentials Reiterated,” The American Mathematical Monthly, No. 4, Vol. 88 (1981), pp. 235-252, Apr. 1981.
https://www.maa.org/programs/maa-awards/writing-awards/exponentials-reiterated-0
