Unprovability of sharp versions of Friedman's sine-principle

For every $n\geq 1$ and every function $F$ of one argument, we introduce the statement $\SP_F^n$: ``for all $m$, there is $N$ such that for any set $A=\{a_1, a_2, \ldots, a_N\}$ of rational numbers, there is $H\subseteq A$ of size $m$ such that for any two $n$-element subsets $a_{i_1}< a_{i_2}<\cdots < a_{i_n}$ and $a_{i_1}< a_{k_2}< \cdots < a_{k_n}$ in $H$, we have

$\vert\sin(a_{i_1}\cdot a_{i_2} \cdots a_{i_n}) - \sin(a_{i_1}\cdot a_{k_2} \cdots a_{k_n} )\vert< F(i_1)''.$

We prove that for $n\geq 2$ and any function $F(x)$ eventually dominated by $({2 \over 3})^{\log^{(n-1)}(x)}$, the principle $\SP_F^{n+1}$ is not provable in $I\Sigma_n$. In particular, the statement $\forall n \SP_{({2 \over 3})^{\log^{(n-1)}}}^n$ is not provable in Peano Arithmetic. In dimension 2, the result is: $I\Sigma_1$ does not prove $\SP^2_F$, where $F(x)=({2 \over 3})^{\sqrt[A^{-1}(x)]{x}}$ and $A^{-1}$ is the inverse of the Ackermann function.