I have given the following Theorem:
Let $A = (a_1,\dots,a_n) \in \mathbb{R}^{m \times n}$ such that the rank of A is known and every $a_i$ is nonzero. Then the following holds \begin{align*} [\neg (\exists p \in P_n) ( Ap = 0) ] \Longrightarrow [(\exists \xi) ( \xi A > 0)], \end{align*} where $P_n \in \mathbb{R}^n$ such that all entries in the vector are $> 0$ and sum up to $1$.
From this theorem I want to show LLPO: $\forall x \in \mathbb{R}^n x \ge 0 \vee x \le 0$.
Please notice that the proof should be constructive, in particular the use of the law of excluded middle is prohibited.
The obvious idea is to define a suitable matrix A and verify LLPO. Therefore let $x \in \mathbb{R}$. I have tried multiple matrices such as
i) $ A= \left[ {\begin{array}{cc} 1 & x \\ x & 0 \\ \end{array} } \right] $
Problem: rank(A) is not known; the reason for this is that constructively $ \neg (x=0) \Rightarrow \vert x \vert > 0$ does NOT hold.
In the following matrices the assumptions of the theorem are always fulfilled, but I am never able to verify LLPO.
ii) $ A= \left[ {\begin{array}{cc} 1 & x & 0 \\ x & 0 & 1\\ 0 & 1 & x \\ \end{array} } \right] $
Problem: rank(A) is known, all columns are unequal 0 , Ap = 0 has no solution if I assume $\vert x \vert < \frac{1}{2}$ (which is allowed); then I have that $( \xi_1 + \xi_2 x , \xi_1 x + \xi_3, \xi + \xi_3x ) > 0$. So there are three different cases: first entry is > 0 and the latter two are $\ge 0$; and the other two cases are given analogously. Now in the first case I have either $\xi_1 > 0 $ or $\xi_2 x > 0$. If the latter holds LLPO follows, but from the first I cannot show LLPO.
iii) $ A= \left[ {\begin{array}{cc} x & 1 \\ 1 & x \\ x & 1 \\ \end{array} } \right] $
iv) $ A= \left[ {\begin{array}{cc} 1 & x & x\\ x & x & 1 \\ x & 1 & x \\ \end{array} } \right] $
v) $ A= \left[ {\begin{array}{cc} x & 1 \\ 1 & x \\ x & x \\ \end{array} } \right] $
vi) $ A= \left[ {\begin{array}{cc} 1 & x \\ x & 1 \\ 0 & x \\ \end{array} } \right] $
To be honest, I have run out of ideas of reasonable matrices; whence I would appreciate some new input resp. any idea in order to proof the LLPO from this theorem.
Edit: As Carl Mummert mentioned, the problem can be also viewed from a geometric standpoint. In this course, I want to state a "suitable" separating lemma.
Consider the following lemma:
Let $Y$ be a located, convex and inhabited set such that $ 0 \notin \mathring{Y}$ and $ \mathring{Y}$ is still located, convex and inhabited. Fix elements $y_1,\dots,y_l \in Y$ such that at all elements are non-zero. Then we have \begin{align*} \exists \xi \in Y : (\langle \xi, y_1\rangle,\dots,\langle \xi, y_l\rangle) > 0. \end{align*}
I already know that this lemma implies the theorem above. I also know that LLPO implies this lemma. Notice that I think it is possible to demand that all entries in the vector are $ > 0$ in both the theorem and the lemma. This might simplify the verification of the LLPO.
Edit 2: I don't think it is possible to show LLPO in this case. In my opinion suitable matrices are such that they have at least one column with only $x's$ and $0's$. But in this case it is not possible to know the rank of the matrix.
I did think about this problem for quite some time now and I don't think its provable in this environment.
In order to know the rank of the matrix A, we need atleast one nonzero constant in every column. But if I have a nonzero constant in every column, I will come across a situation where I know that, f.e. $\xi_1 > 0$ and $\xi_1 x + \xi_2 \ge 0$. I this situation I cannot make any statements about the sign of x. Although this is only one example of a possible situation, it is rather obvious that any matrix A with known rank will lead to a problem like this. Hence I can't show LLPO.