It it true that for all $p\in(0,1/3]$ and all real $t$ we have $$4 \ln(1-p +p\cosh t) \ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}} \le t^2 (1+c p) \sqrt{1-2p} ,$$ where $c:=2\sqrt{3}\, \ln(2+\sqrt{3})-3$?
If true, this inequality will provide an answer to this previous question.
Remark 1. Here is a proof. By plotting the function, I observed that the optimal $t$ is approximately equal to $\ln\frac{4}{p^2}$ when $p$ is small (in the notation below, that is to say, the $s$ with $\frac{\partial f(s, p)}{\partial s} = 0$ satisfies $s\le 4$ and $s \to 4$ when $p \to 0$). This inspires me.
Remark 2. It is a challenge problem.
Problem. Let $p \in (0, 1/3]$ and $t > 0$. Prove that $$4 \ln(1-p +p\cosh t) \ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}} \le t^2 (1+c p) \sqrt{1-2p} $$ where $c := 2\sqrt{3}\ln(2 + \sqrt{3}) - 3$.
Proof.
Let $s := p^2\mathrm{e}^t$. Then $t = \ln \frac{s}{p^2}$ and $s > p^2$. The desired inequality is written as $$f(s, p) \le g(p) \tag{1}$$ where $$f(s, p) := \frac{4 \ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right)}{\ln^2 \frac{s}{p^2}}, \quad g(p) := \frac{(1+c p) \sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}}.$$ The constraints are $0 < p \le 1/3$ and $s > p^2$.
We split into four cases.
Case 1. $1/6 < p \le 1/3$ and $s > p^2$
We have, for all $1/6 \le p \le 1/3$, $$\frac{(1+c p) \sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}} \ge \frac23 + \frac{6}{c + 3}(p - 1/3).$$ (Note. The proof is easy by taking derivative. By the way, the RHS is the first order Taylor approximation of the LHS around $p = 1/3$. )
It suffices to prove that $$\frac{4 \ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right)}{\ln^2 \frac{s}{p^2}} \le \frac23 + \frac{6}{c + 3}(p - 1/3),$$ or $$M(s) := \left(\frac23 + \frac{6}{c + 3}(p - 1/3)\right)\ln^2 \frac{s}{p^2} - 4 \ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right) \ge 0.$$ Since $M(p^2) = 0$, it suffices to prove that $M'(s) \ge 0$ for all $s > p^2$, or $$ \left(\frac23 + \frac{6}{c + 3}(p - 1/3)\right)\cdot \frac{2}{s}\ln \frac{s}{p^2} - \frac{4 \left(\frac{1}{2p} - \frac{p^3}{2s^2}\right)}{1-p + \frac{s}{2p} + \frac{p^3}{2s}}\ge 0.$$ Since $\frac{6}{c+3} < \frac{25}{19}$, it suffices to prove that $$ \left(\frac23 + \frac{25}{19}(p - 1/3)\right)\cdot \frac{2}{s}\ln \frac{s}{p^2} - \frac{4 \left(\frac{1}{2p} - \frac{p^3}{2s^2}\right)}{1-p + \frac{s}{2p} + \frac{p^3}{2s}}\ge 0.$$ Let $u := s/p^2 - 1$. It suffices to prove that, for all $u > 0$ and $1/6 \le p \le 1/3$, $$\ln (1 + u) - \frac{114u(u+2)}{75u^2p + \frac{26u + 26}{p} + 13u^2 + 150u + 150} \ge 0$$ which is true (smooth; Use the fact that $75u^2p + \frac{26u + 26}{p}$ attains the minimum when either $p = 1/6$, $p = 1/3$, or $75u^2 = \frac{26u + 26}{p^2}$).
Case 2. $0 < p \le 1/6$ and $p^2 < s \le 1$
Fact 1. If $p \in (0, 1/6]$ is given, then $\frac{\partial f(s,p)}{\partial s} \ge 0$ for all $p^2 < s \le 1$. (The proof is given at the end.)
By Fact 1, it suffices to prove that $f(1, p) \le g(p)$ or $$\frac{4 \ln\left(1-p + \frac{1}{2p} + \frac{p^3}{2}\right)}{\ln^2 \frac{1}{p^2}} \le \frac{(1+c p) \sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}}. \tag{2}$$
Since $u \mapsto \frac{u}{\ln \frac{1+u}{1-u}}$ is strictly decreasing on $(1/2, 1)$ and $\sqrt{1-2p} < 1 - p$, we have $$\frac{\sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}} \ge \frac{1 - p}{\ln \frac{1 + (1-p)}{1 - (1 - p)}} = \frac{1-p}{\ln\frac{1}{p} + \ln 2 + \ln(1 - p/2)} \ge \frac{1-p}{\ln\frac{1}{p} + \ln 2 - \frac{p}{2}}. \tag{3} $$ Also, we have \begin{align*} \ln\left(1-p + \frac{1}{2p} + \frac{p^3}{2}\right) &= \ln \frac{1}{p} - \ln 2 + \ln(1 + 2p - 2p^2 + p^4)\\ &\le \ln\frac{1}{p} - \ln 2 + 2p - 2p^2 + p^4. \tag{4} \end{align*}
From (2)-(4), using $c > 3/2$, it suffices to prove that $$\frac{(1+3p/2)(1-p)}{\ln\frac{1}{p} + \ln 2 - p/2} \ge \frac{\ln\frac{1}{p} - \ln 2 + 2p - 2p^2 + p^4}{\ln^2(1/p)}, $$ or \begin{align*} &\left( -3\,{p}^{2}+p \right) \ln^2(1/p) + \left( -2\,{p}^{4}+4\,{p}^{2}-3 \,p \right) \ln(1/p)\\ &\qquad +2\ln^2 2 + \left( -2\,{p}^{4}+4\,{p}^{2}-5\,p \right) \ln 2 +{p}^{5}-2\,{p}^{3}+2\,{p}^{2} \ge 0, \end{align*} or (using $11/16 < \ln 2 < 7/10$) \begin{align*} &\left( -3\,{p}^{2}+p \right) \ln^2(1/p) + \left( -2\,{p}^{4}+4\,{p}^{2}-3 \,p \right) \ln(1/p)\\ &\qquad + 2(11/16)^2 + \left( -2\,{p}^{4}+4\,{p}^{2}-5\,p \right) \cdot \frac{7}{10} +{p}^{5}-2\,{p}^{3}+2\,{p}^{2} \ge 0, \end{align*} which is true since \begin{align*} &4 \cdot (-3p^2 + p) \cdot \left(2(11/16)^2 + \left( -2\,{p}^{4}+4\,{p}^{2}-5\,p \right) \cdot \frac{7}{10} +{p}^{5}-2\,{p}^{3}+2\,{p}^{2}\right)\\ \ge{}& \left( -2\,{p}^{4}+4\,{p}^{2}-3 \,p \right) ^2. \end{align*}
Case 3. $0 < p \le 1/6$ and $s \ge 4$
We have \begin{align*} &\frac{\partial f(s,p)}{\partial s}\\ ={}& \frac{16p}{(p^4 - 2p^2s + 2ps + s^2)\ln^3 \frac{s}{p^2}}\\ &\quad \times \left[\left(\frac{p}{4} - \frac{p^5}{4s^2}\right) \frac{s}{p^2}\ln\frac{s}{p^2} - \left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right)\ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right)\right]\\ <{}& \frac{16p}{(p^4 - 2p^2s + 2ps + s^2)\ln^3 \frac{s}{p^2}} \left[\frac{p}{4} \cdot \frac{s}{p^2}\ln\frac{s}{p^2} - \frac{s}{2p}\ln \frac{s}{2p}\right]\\ ={}& \frac{16p}{(p^4 - 2p^2s + 2ps + s^2)\ln^3 \frac{s}{p^2}}\cdot \frac{s}{4p} \left[\ln\frac{s}{p^2} - \ln \frac{s^2}{4p^2}\right]\\ \le{}& 0. \tag{5} \end{align*}
Thus, it suffices to prove that $f(4, p) \le g(p)$ or $$\frac{4 \ln\left(1-p + \frac{2}{p} + \frac{p^3}{8}\right)}{\ln^2 \frac{4}{p^2}} \le \frac{(1+c p) \sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}}. \tag{6}$$
Since $u \mapsto \frac{u}{\ln \frac{1+u}{1-u}}$ is strictly decreasing on $(1/2, 1)$ and $\sqrt{1-2p} < 1 - p$, we have $$\frac{\sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}} \ge \frac{1 - p}{\ln \frac{1 + (1-p)}{1 - (1 - p)}} = \frac{1-p}{\ln\frac{2}{p} + \ln(1 - p/2)} \ge \frac{1-p}{\ln\frac{2}{p} - \frac{p}{2}}. \tag{7} $$ Also, we have $$\ln\left(1-p + \frac{2}{p} + \frac{p^3}{8}\right) \le \ln(1 + 2/p) = \ln\frac{2}{p} + \ln(1 + p/2) \le \ln\frac{2}{p} + \frac{p}{2}. \tag{8}$$
From (6)-(8), using $c > 3/2$, it suffices to prove that $$\frac{4 \ln \frac{2}{p} + 2p}{\ln^2 \frac{4}{p^2}} \le \frac{(1+3 p/2)(1-p)}{\ln\frac{2}{p} - \frac{p}{2}},$$ or $$\frac{p}{(4 \ln \frac{2}{p} - 2p)\ln^2 \frac{2}{p}} \left(p + (2-6p)\ln^2 \frac{2}{p}\right) \ge 0$$ which is true.
Case 4. $0 < p \le \frac16$ and $1 < s < 4$
Since $u \mapsto \frac{u}{\ln \frac{1+u}{1-u}}$ is strictly decreasing on $(1/2, 1)$ and $\sqrt{1-2p} < 1 - p$, we have $$\frac{\sqrt{1-2p}}{\ln\frac{1+\sqrt{1-2p}}{1-\sqrt{1-2p}}} \ge \frac{1 - p}{\ln \frac{1 + (1-p)}{1 - (1 - p)}} = \frac{1-p}{\ln\frac{2}{p} + \ln(1 - p/2)} \ge \frac{1-p}{\ln\frac{2}{p} - \frac{p}{2}}. \tag{9} $$ Also, we have \begin{align*} \ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right) &\le \ln(1 + s/(2p))\\ &= \ln\frac{s}{2p} + \ln (1 + 2p/s)\\ &\le \ln\frac{s}{2p} + \frac{2p(s+p)}{s(s+2p)} \tag{10} \end{align*} where we use $\ln(1 + u) \le \frac{u}{2}\cdot \frac{2+u}{1+u}$ for all $u\ge 0$.
From (9) and (10), using $c > 3/2$, it suffices to prove that $$\frac{4 \left(\ln\frac{s}{2p} + \frac{2p(s+p)}{s(s+2p)}\right)}{\ln^2 \frac{s}{p^2}} \le \frac{(1+3p/2)(1-p)}{\ln\frac{2}{p} - \frac{p}{2}},$$ or $$\frac{4 \left(\ln\frac{1}{p} - \ln 2 + \ln s + \frac{2p(s+p)}{s(s+2p)}\right)}{(\ln s + 2\ln\frac{1}{p} )^2} \le \frac{(1+3p/2)(1-p)}{\ln\frac{1}{p} + \ln 2 - \frac{p}{2}},$$ or (using $(1+3p/2)(1-p) - (1+p/4) = p(1-6p)/4 \ge 0$) $$\frac{4 \left(\ln\frac{1}{p} - \ln 2 + \ln s + \frac{2p(s+p)}{s(s+2p)}\right)}{(\ln s + 2\ln\frac{1}{p} )^2} \le \frac{1 + p/4}{\ln\frac{1}{p} + \ln 2 - \frac{p}{2}},$$ or (clearing the denominators) $$m_2 \ln^2 \frac{1}{p} + m_1 \ln\frac{1}{p} + m_0 \ge 0 \tag{11}$$ where \begin{align*} m_2 &= 8\,{p}^{2}s+4\,p{s}^{2}, \\ m_1 &= \left( 8\,{p}^{2}s+4\,p{s}^{2} \right) \ln s +16\,{p}^{2}s+8\,p{s}^{2}-32 \,{p}^{2}-32\,ps\\ m_0 &= \left( 2\,{p}^{2}s+p{s}^{2}+8\,ps+4\,{s}^{2} \right) \ln^2 s + \left[ \left( -32\,ps-16\,{s}^{2} \right) \ln 2 + 16\,{p}^{2}s+8\,p{s}^{2} \right] \ln s \\ &\quad + \left( 32\,ps+16\,{s}^{2} \right) \ln^2 2 + \left( -16\,{p} ^{2}s-8\,p{s}^{2}-32\,{p}^{2}-32\,ps \right) \ln 2 +16\,{p}^{3}+16\,{p}^{2} s. \end{align*}
We have $$\ln \frac{1}{p} = \ln\frac{1}{6p} + \ln 6 \ge \frac{2 - 12p}{6p + 1} + \frac{43}{24} \tag{12}$$ where we use $\ln (1 + u) \ge \frac{2u}{2+u}$ for all $u \ge 0$, and $\ln 6 \ge \frac{43}{24}$.
From (11) and (12), it suffices to prove that $$m_2 \cdot \left(\frac{2 - 12p}{6p + 1} + \frac{43}{24}\right)\ln \frac{1}{p} + m_1 \ln \frac{1}{p} + m_0 \ge 0,$$ or $$\left(m_2 \cdot \left(\frac{2 - 12p}{6p + 1} + \frac{43}{24}\right) + m_1\right)\ln\frac{1}{p} + m_0 \ge 0. \tag{13}$$
Fact 2. $m_0 \ge 0$. (The proof is given at the end.)
By Fact 2, we only need to prove the case $m_2 \cdot (\frac{2 - 12p}{6p + 1} + \frac{43}{24}) + m_1 < 0$.
Also, we have $$\ln \frac{1}{p} = \ln \frac{1}{6p} + \ln 6 \le \frac{1}{6p} - 1 + \frac{9}{5} \tag{14}$$ where we use $\ln(1 + u) \le u$ for all $u \ge 0$, and $\ln 6 < \frac95$.
Thus, from (13) and (14), it suffices to prove that $$\left(m_2 \cdot \left(\frac{2 - 12p}{6p + 1} + \frac{43}{24}\right) + m_1\right)\cdot \left(\frac{1}{6p} - 1 + \frac{9}{5}\right) + m_0 \ge 0$$ or $$q_2 \ln^2{s} + q_1 \ln{s} + q_0 \ge 0$$ where \begin{align*} q_2 &= 180\,s \left( p+4 \right) \left( 6\,p+1 \right) \left( 2\,p+s \right) \\ q_1 &= -24\,s \left( 6\,p+1 \right) \left( 2\,p+s \right) \left( 120\ln{2} - 84 \,p-5 \right) \\ q_0 &= 2880\,s \left( 6\,p+1 \right) \left( 2\,p+s \right) \ln^2{2}\\ &\qquad -1440\,p \left( 6\,p+1 \right) \left( 2\,ps+{s}^{2}+4\,p+4\,s \right) \ln{2} \\ &\qquad +17280 \,{p}^{4}+29664\,{p}^{3}s+6192\,{p}^{2}{s}^{2}-24768\,{p}^{3}-15516\,{ p}^{2}s\\ &\qquad +4626\,p{s}^{2} -10368\,{p}^{2}-8978\,ps+695\,{s}^{2}-960\,p-960 \,s. \end{align*}
We have, for all $s\ge 1$, $$\ln s \ge \frac{3(s^2 - 1)}{s^2 + 4s + 1}.$$
It suffices to prove that $$q_2 \cdot \frac{3(s^2 - 1)}{s^2 + 4s + 1}\ln{s} + q_1\ln s + q_0 \ge 0,$$ or $$\left(q_2 \cdot \frac{3(s^2 - 1)}{s^2 + 4s + 1} + q_1\right)\ln{s} + q_0 \ge 0.$$
It is easy to prove that $q_0 \ge 0$ for all $p\in (0, 1/6]$ and $s \in [1, 4]$. We only need to prove the case $q_2 \cdot \frac{3(s^2 - 1)}{s^2 + 4s + 1} + q_1 < 0$.
We have (easy), for all $s \ge 1$, $$\ln{s} \le \frac{s^2 - 1}{2s}.$$
It suffices to prove that $$\left(q_2 \cdot \frac{3(s^2 - 1)}{s^2 + 4s + 1} + q_1\right)\cdot \frac{s^2 - 1}{2s} + q_0 \ge 0$$ or $$T_2 \ln^2{2} + T_1\ln{2} + T_0 \ge 0$$ where \begin{align*} T_2 &= 2880\,s \left( {s}^{2}+4\,s+1 \right) \left( 6\,p+1 \right) \left( 2 \,p+s \right),\\ T_1 &= -1440\, \left( {s}^{2}+4\,s+1 \right) \left( 6\,p+1 \right) \left( 2 \,{p}^{2}s+3\,p{s}^{2}+{s}^{3}+4\,{p}^{2}+4\,ps-2\,p-s \right) ,\\ T_0 &= 15336\,{p}^{3}{s}^{4}+7668\,{p}^{2}{s}^{5}+17280\,{p}^{4}{s}^{2}+78048 \,{p}^{3}{s}^{3}+46620\,{p}^{2}{s}^{4}\\ &\qquad +8118\,p{s}^{5}+69120\,{p}^{4}s+ 87408\,{p}^{3}{s}^{2}+16956\,{p}^{2}{s}^{3}+12378\,p{s}^{4}\\ &\qquad +1140\,{s}^ {5}+17280\,{p}^{4}-117792\,{p}^{3}s-117432\,{p}^{2}{s}^{2}-3494\,p{s}^ {3}\\ &\qquad +935\,{s}^{4}-33624\,{p}^{3}-72360\,{p}^{2}s-42038\,p{s}^{2}-340\,{ s}^{3}+396\,{p}^{2}\\ &\qquad -7916\,ps-3385\,{s}^{2}+1080\,p+60\,s. \end{align*}
Using $\ln 2 > \frac{192}{277}$, it suffices to prove that $$T_2\cdot \frac{192}{277} \ln{2} + T_1 \ln 2 + T_0 \ge 0,$$ or $$\left(T_2\cdot \frac{192}{277} + T_1\right)\ln{2} + T_0 \ge 0.$$
If $T_2\cdot \frac{192}{277} + T_1 \ge 0$, using $\ln 2 > \frac{192}{277}$, it suffices to prove that $$\left(T_2\cdot \frac{192}{277} + T_1\right)\frac{192}{277} + T_0 \ge 0$$ which is true for all $p\in (0, 1/6]$ and $s\in [1, 4]$.
If $T_2\cdot \frac{192}{277} + T_1 < 0$, using $\ln 2 < \frac{61}{88}$, it suffices to prove that $$\left(T_2\cdot \frac{192}{277} + T_1\right)\frac{61}{88} + T_0 \ge 0$$ which is true for all $p\in (0, 1/6]$ and $s\in [1, 4]$.
We are done.
Proof of Fact 1.
It suffices to prove that (see (5) for $\frac{\partial f(s,p)}{\partial s}$), for all $p^2 < s \le 1$, $$\left(\frac{p}{4} - \frac{p^5}{4s^2}\right) \frac{s}{p^2}\ln\frac{s}{p^2} - \left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right)\ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right) \ge 0.$$
We split into two cases.
(i) $p^2 < s \le p$
Using $u\ln u \ge \frac{(u - 1)(10u^2 + 19u + 1)}{3u^2 + 18u + 9}$ for all $u \ge 1$ (easy), we have $$\frac{s}{p^2}\ln\frac{s}{p^2} \ge \frac{(s-p^2)(p^4 + 19p^2 s + 10s^2)}{9p^6 + 18p^4 s + 3p^2s^2}.$$
It suffices to prove that \begin{align*} &\left(\frac{p}{4} - \frac{p^5}{4s^2}\right) \cdot \frac{(s-p^2)(p^4 + 19p^2 s + 10s^2)}{9p^6 + 18p^4 s + 3p^2s^2} \\ &\qquad - \left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right)\ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2s}\right) \ge 0 \end{align*} which is true (smooth, by taking derivative).
(ii) $p < s \le 1$
It suffices to prove that $$\left(\frac{p}{4} - \frac{p^5}{4p^2}\right) \frac{s}{p^2}\ln\frac{s}{p^2} - \left(1-p + \frac{s}{2p} + \frac{p^3}{2p}\right)\ln\left(1-p + \frac{s}{2p} + \frac{p^3}{2p}\right) \ge 0.$$ Denote the LHS by $H(s)$. We have $$H''(s) = \frac{(p-p^3)(p^2-2p+2) - s(1 + p^2)}{4ps(p^3 - 2p^2 + 2p + s)}.$$ Let $s_0 = \frac{(p-p^3)(p^2 - 2p + 2)}{1 + p^2}$. It is easy to prove that $s_0 > 0$, and $H''(s) > 0 $ on $(p, s_0)$, and $H''(s) < 0$ on $(s_0, 1]$. It is easy to prove that $H'(p) > 0$ and $H(1) > 0$. Thus, we have $H(s) \ge 0$ on $(p, 1)$. This completes the proof of Fact 1.
Proof of Fact 2.
We have $$\ln s = \ln \frac{s}{4} + 2\ln 2 \ge \frac{s^2 - 16}{8s} + 2\ln 2$$ where we use $\ln(1 + u) \ge \frac{u}{2}\cdot \frac{2+u}{1+u}$ for all $u\in (-1, 0]$.
It suffices to prove that \begin{align*} &\left( 2\,{p}^{2}s+p{s}^{2}+8\,ps+4\,{s}^{2} \right)\cdot \left(\frac{s^2 - 16}{8s} + 2\ln 2\right) \ln{s}\\ &\quad + \left[ \left( -32\,ps-16\,{s}^{2} \right) \ln 2 + 16\,{p}^{2}s+8\,p{s}^{2} \right] \ln s \\ &\quad + \left( 32\,ps+16\,{s}^{2} \right) \ln^2 2 + \left( -16\,{p} ^{2}s-8\,p{s}^{2}-32\,{p}^{2}-32\,ps \right) \ln 2 +16\,{p}^{3}+16\,{p}^{2}\\ &\ge 0 \end{align*} or $$n_1\ln{s} + n_0 \ge 0$$ where \begin{align*} n_1 &= \left( 2\,p+s \right) \left( \left( 16\,ps-64\,s \right) \ln{2} + p{s}^{2} +64\,ps+4\,{s}^{2}-16\,p-64 \right) , \\ n_0 &= 64\, \left( 2\ln{2} - p \right) \Big( \left( 2\,ps+{s}^{2} \right) \ln{2} - 2\, {p}^{2}-2\,ps \Big). \end{align*}
Since $n_0 \ge 0$ (easy), we only need to prove the case $n_1 < 0$.
We have (easy), for all $s \in [1, 4]$, $$\ln{s} \le \frac{(3 + 2\ln{2})s^2 + 32s\ln{2} + 32\ln{2} - 48}{s^2 + 16s + 16}.$$ (Note: It is the $(2,2)$-Pade approximation at $s = 4$.)
It suffices to prove that $$n_1 \cdot \frac{(3 + 2\ln{2})s^2 + 32s\ln{2} + 32\ln{2} - 48}{s^2 + 16s + 16} + n_0 \ge 0,$$ or $$k_2\ln^2{2} + k_1\ln{2} + k_0 \ge 0$$ where \begin{align*} k_2 &= 64\,{p}^{2}{s}^{3}+32\,p{s}^{4}+1024\,{p}^{2}{s}^{2}+512\,p{s}^{3}+ 1024\,{p}^{2}s+512\,p{s}^{2},\\ k_1 &= 4\,{p}^{2}{s}^{4}+2\,p{s}^{5}+288\,{p}^{2}{s}^{3}+160\,p{s}^{4}+8\,{s} ^{5}+1792\,{p}^{2}{s}^{2}+640\,p{s}^{3}-64\,{s}^{4}\\ &\qquad-4608\,{p}^{2}s- 4352\,p{s}^{2}-5120\,{p}^{2}-2560\,ps+1024\,{s}^{2}-4096\,p-2048\,s\\ k_0 &= 6\,{p}^{2}{s}^{4}+3\,p{s}^{5}+128\,{p}^{3}{s}^{2}+512\,{p}^{2}{s}^{3}+ 216\,p{s}^{4}+12\,{s}^{5}\\ &\qquad +2048\,{p}^{3}s+1856\,{p}^{2}{s}^{2} -96\,p{s} ^{3}+2048\,{p}^{3} -4096\,{p}^{2}s-3840\,p{s}^{2}-384\,{s}^{3}\\ &\qquad +1536\,{p }^{2}+768\,ps+6144\,p+3072\,s. \end{align*}
Using $\ln{2} > \frac{192}{277}$, it suffices to prove that $$k_2 \cdot \frac{192}{277} \ln{2} + k_1 \ln{2} + k_0 \ge 0$$ or $$\left(k_2 \cdot \frac{192}{277} + k_1\right)\ln{2} + k_0 \ge 0.$$
Since $k_0 \ge 0$ (easy), we only need to prove the case $k_2 \cdot \frac{192}{277} + k_1 < 0$. Using $\ln{2} < \frac{61}{88}$, it suffices to prove that $$\left(k_2 \cdot \frac{192}{277} + k_1\right)\frac{61}{88} + k_0 \ge 0$$ or \begin{align*} &106922\,{p}^{2}{s}^{4}+53461\,p{s}^{5}+1560064\,{p}^{3}{s}^{2}+9048208 \,{p}^{2}{s}^{3}+4171760\,p{s}^{4}\\ &\quad +213844\,{s}^{5}+24961024\,{p}^{3}s+ 43757184\,{p}^{2}{s}^{2}+7235264\,p{s}^{3}\\ &\quad -540704\,{s}^{4}+24961024\,{ p}^{3}-82856192\,{p}^{2}s-80571520\,p{s}^{2}-4680192\,{s}^{3}\\ &\quad -24535552 \,{p}^{2}-12267776\,ps+8651264\,{s}^{2}+40278016\,p+20139008\,s\\ &\ge 0 \end{align*} which is true for all $p\in [0, 1/6]$ and $s \in [1, 4]$. This completes the proof of Fact 2.
