20241011-decomposability-and-wlpo.tex

\documentclass[12pt,a4paper]{article}  % -*- coding: utf-8 -*-
\usepackage[a4paper,margin=1.5cm]{geometry}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{times}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
%
\usepackage{mathrsfs}
%\usepackage{bm}
%\usepackage{stmaryrd}
\usepackage{wasysym}
\usepackage{url}
\usepackage{graphicx}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage{tikz}
\usetikzlibrary{matrix,arrows,decorations.markings}
%\usepackage{hyperref}
%
%
%
\theoremstyle{definition}
\newtheorem{comcnt}{Anything}
\newcommand\thingy{%
\refstepcounter{comcnt}\medbreak\noindent\textparagraph\textbf{\thecomcnt.} }
\newtheorem{thm}[comcnt]{Theorem}
\newtheorem{prop}[comcnt]{Proposition}
\newtheorem{lem}[comcnt]{Lemma}
\newtheorem{ques}[comcnt]{Question}
%
%
%
\newcommand{\apart}{\mathrel{\#}}
%
%
%
\begin{document}
\pretolerance=8000
\tolerance=50000

\thingy We work in a constructive math setting in the absence of any
form of Choice (except Unique Choice; e.g., a topos with a natural
numbers object, or in $\mathsf{IZF}$).  We denote by $\mathbb{R}$ the
set of Dedekind reals, and by $x\apart y$ the relation $|x-y|>0$
(equivalently, “$x<y$ or $x>y$”); recall that $x=y$ means
$\neg(x\apart y)$ (but $x\apart y$ is \textit{a priori} stronger than
$\neg(x=y)$ which is just $\neg\neg(x\apart y)$).

\thingy\label{wlpo-and-friends} We consider the following principles,
the implications between which we wish to investigate:

\begin{itemize}
\item “$\mathbf{DEC}(\mathbb{R})$”: There exists subsets $A,B
  \subseteq \mathbb{R}$ such that $A$ and $B$ are inhabited, $A \cap B
  = \varnothing$ and $A \cup B = \mathbb{R}$.
\item “$\mathbf{WLPO}_{\mathbb{R}}$”: Every $c\in \mathbb{R}$
  satisfies $c=0$ or $\neg(c=0)$.
\item “$\mathbf{WLPO}_{\mathrm{seq}}$”: Every binary sequence $(p_n)$
  (i.e., element of $\{0,1\}^{\mathbb{R}}$) satisfies $\forall
  n.(p_n=0)$ or $\neg\forall n.(p_n=0)$.
\end{itemize}

\thingy\label{dec-vs-chi-function} Note that
$\mathbf{DEC}(\mathbb{R})$ is equivalent to the existence of a
function $\chi\colon\mathbb{R}\to\{0,1\}$ such that $\exists
a\in\mathbb{R}.(\chi(a)=0)$ and $\exists b\in\mathbb{R}.(\chi(b)=0)$.
Furthermore, replacing $\chi$ by $t \mapsto \chi(a+(b-a)t)$, we can
assume that in fact $\chi(0)=0$ and $\chi(1)=1$.  We will generally
work with this form.

\thingy\label{analytic-wlpo-implies-sequential-wlpo} It is a standard
fact that $\mathbf{WLPO}_{\mathbb{R}}$ implies
$\mathbf{WLPO}_{\mathrm{seq}}$.  This will be reproved incidentally in
the course of what follows, but a shorter argument goes as follows.
If $(p_n)$ is a binary sequence, we define a real sequence $z_n :=
\sum_{k=0}^n p_k\cdot 2^{-k}$.  Clearly this sequence is Cauchy with
modulus $|z_m-z_n| \leq 2^{-\min(m,n)}$, so it has a limit $z$.  If
there is $n$ such that $p_n = 1$, then $z \geq 2^{-n}$, so $z\apart
0$; so contrapositively, $z=0$ implies that $(p_n)$ is
identically $0$.  But conversely, if $(p_n)$ is identically $0$ then
trivially $z=0$.  This shows that $(p_n)$ is the zero sequence if and
only if $z=0$.  Now $\mathbf{WLPO}_{\mathbb{R}}$ tells us that $z=0$
or is not.  So we conclude that $(p_n)$ is the zero sequence or it is
not.  This gives $\mathbf{WLPO}_{\mathrm{seq}}$.\quad\qedsymbol

\begin{thm}\label{dec-r-equivalent-to-analytic-wlpo}
$\mathbf{DEC}(\mathbb{R})$ is equivalent to
  $\mathbf{WLPO}_{\mathbb{R}}$
\end{thm}

The implication $\mathbf{WLPO}_{\mathbb{R}} \; \Longrightarrow \;
\mathbf{DEC}(\mathbb{R})$ is trivial.  Indeed,
$\mathbf{WLPO}_{\mathbb{R}}$ asserts precisely that $\mathbb{R}$ is
the disjoint union of $\{0\}$ and $\mathbb{R}\setminus\{0\} := \{t :
\neg(t=0)\}$.

The converse follows immediately from lemmate
\ref{dec-r-implies-sequential-wlpo} and \ref{dec-r-and-sequential-wlpo-imply-analytic-wlpo}.

\begin{lem}[Mohammad Tahmasbi]\label{dec-r-implies-sequential-wlpo}
$\mathbf{DEC}(\mathbb{R})$ implies $\mathbf{WLPO}_{\mathrm{seq}}$
\end{lem}

\begin{proof}
Assume $\chi\colon\mathbb{R}\to\{0,1\}$ satisfies $\chi(0)=0$ and
$\chi(1)=1$.

Define real sequences $(u_n)$ and $(v_n)$ by induction as follows: put
$u_0=0$ and $v_0=1$, and then :
\begin{itemize}\setlength\itemsep{0pt}
\item when $\chi(\frac{u_n+v_n}{2})=0$ let $u_{n+1} =
  \frac{u_n+v_n}{2}$ and $v_{n+1} = v_n$,
\item when $\chi(\frac{u_n+v_n}{2})=1$ let $u_{n+1} = u_n$ and
  $v_{n+1} = \frac{u_n+v_n}{2}$.
\end{itemize}

Obviously we have $\chi(u_n)=0$ and $\chi(v_n)=1$ for all $n$ by
induction.  Furthermore, $(u_n)$ and $(v_n)$ satisfy $0\leq u_m\leq
u_n\leq v_n\leq v_m\leq 1$ when $m\leq n$, and $|u_n-v_n| \leq
2^{-n}$.  In particular, they are Cauchy with modulus $|u_m-u_n| \leq
2^{-\min(m,n)}$ and $|v_m-v_n| \leq 2^{-\min(m,n)}$, and they have the
same limit.  Call $w$ this common limit: we have $|w-u_n| \leq 2^{-n}$
and $|w-v_n| \leq 2^{-n}$.

We can assume without loss of generality that $\chi(w)=0$, the case
$\chi(w)=1$ being entirely symmetric.

Now let $(p_n)$ be a binary sequence.  We wish to show that $(p_n)$ is
the zero sequence or it is not.

Define a real sequence $(z_n)$ as follows:
\begin{itemize}\setlength\itemsep{0pt}
\item when $p_k=0$ for all $0\leq k\leq n$, let $z_n = w$,
\item when there exists an $0\leq k\leq n$ such that $p_k=1$, let $z_n
  = v_k$ where $k$ is the smallest such $k$.
\end{itemize}
(In other words, $z_n$ is constantly $w$ until the first $m$ where
$p_m$ takes the value $1$, at which point and after which $z_n$ equals
$v_m$.)  This sequence is well-defined.

We claim that $|z_m-z_n| \leq 2^{-\min(m,n)}$.  Indeed, with $m\leq n$
there are three possible cases, namely (1) $p_k=0$ for all $0\leq
k\leq n$ so that $z_m=z_n=w$, (2) $p_k=0$ for all $0\leq k\leq m$ but
there is $m+1\leq k\leq n$ such that $p_k=1$, so that $z_m=w$ and
$z_n=v_k$ for the smallest such $k$, and (3) there is $0\leq k\leq m$
such that $p_k=1$, so that $z_m=z_n=v_k$ for the smallest such $k$.
Cases (1) and (3) are trivial (we have $z_m=z_n$), and in case (2) we
have $|z_m-z_n| \leq |w-v_k| \leq 2^{-k}$ but $m\leq k\leq n$, so
$|z_m-z_n| \leq 2^{-m}$ as desired.  This concludes the claim.

We have just seen that $(z_n)$ is Cauchy with modulus $|z_m-z_n| \leq
2^{-\min(m,n)}$.  Therefore it has a limit $z$.  Note that $\chi(z)=0$
or $\chi(z)=1$.

If there is $k$ such that $p_k=1$ then $z_n$ is equal to $v_k$ for all
$n\geq k$ where $k$ is the smallest such $k$, and in particular, $z =
v_k$, which gives $\chi(z) = \chi(v_k) = 1$; so contrapositively,
$\chi(z) = 0$ implies that $(p_n)$ is identically $0$.  But
conversely, if $(p_n)$ is identically $0$ then $(z_n)$ is the constant
sequence with value $w$ so $z=w$, which gives $\chi(z) = \chi(w) = 0$.
This proves that $(p_n)$ is the zero sequence if and only if $\chi(z)
= 0$.  Therefore, $(p_n)$ is the zero sequence or it is not.

This gives $\mathbf{WLPO}_{\mathrm{seq}}$, as claimed.
\end{proof}

\begin{lem}\label{dec-r-and-sequential-wlpo-imply-analytic-wlpo}
$\mathbf{DEC}(\mathbb{R})$ and $\mathbf{WLPO}_{\mathrm{seq}}$ together
  imply $\mathbf{WLPO}_{\mathbb{R}}$
\end{lem}

\begin{proof}
Assume $\chi\colon\mathbb{R}\to\{0,1\}$ satisfies $\chi(0)=0$ and
$\chi(1)=1$.  Replacing $\chi$ by $t \mapsto \chi(\inf(1,|t|))$, we
can assume that in fact $\chi(t)=1$ whenever $|t|\geq 1$.

Now let $c$ be a real.  We wish to show that $c$ is zero or it is not.

Define a binary sequence $(p_n)$ by $p_n := \chi(2^n c)$.

If $c\apart 0$, that is $|c|>0$, then there is $n$ such that
$2^n\,|c|\geq 1$, so $p_n = 1$; so contrapositively, if $(p_n)$ is the
zero sequence then $c=0$.  But conversely, if $c=0$ then $p_n$ is
trivially constantly equal to $0$.  This proves that $(p_n)$ is the
zero sequence if and only if $c = 0$.  Now
$\mathbf{WLPO}_{\mathrm{seq}}$ tells us that $(p_n)$ is the zero
sequence or it is not.  So we conclude that $z$ is zero or it is not.

This gives $\mathbf{WLPO}_{\mathbb{R}}$, as claimed.
\end{proof}

\thingy\label{sequential-wlpo-does-not-imply-analytic-wlpo} We have
remarked in ¶\ref{analytic-wlpo-implies-sequential-wlpo} that
$\mathbf{WLPO}_{\mathbb{R}} \; \Longrightarrow \;
\mathbf{WLPO}_{\mathrm{seq}}$.  The converse generally does not hold.
To see this, (working in a classical universe) we consider the
topological model over $\mathbb{R}$, i.e., the topos of sheaves over
$\mathbb{R}$.

In this model, the statement $\mathbf{WLPO}_{\mathbb{R}}$ does not
hold, since it unwinds to saying that if $c$ is a continuous
real-valued function on an open subset $U$ of $\mathbb{R}$ then $U$ is
the union of the largest open set on which $c=0$ (i.e., the interior
of $\{x \in U : c(x) = 0\}$) and the largest open set on which $c\neq
0$ holds densely (i.e., the interior of the closure of $\{x \in U :
c(x) \neq 0\}$); but the function $\mathbb{R}\to\mathbb{R}$ given by
$x \mapsto \max(0,x)$ provides a counterexample to this.

However, $\mathbf{WLPO}_{\mathrm{seq}}$, and in fact even
$\mathbf{LPO}_{\mathrm{seq}}$, which asserts that every binary
sequence $(p_n)$ satisfies $\forall n.(p_n=0)$ or $\exists n.(p_n=1)$,
\emph{does} hold in the model.  Indeed, $\mathbf{LPO}_{\mathrm{seq}}$
unwinds to saying that if $U$ is an open subset of $\mathbb{R}$ and
$(p_n)$ a sequence of \emph{continuous} (= locally constant) functions
$U \to \{0,1\}$, then we can find open sets $V,W_n$ with $U = V\cup
\bigcup_n W_n$ such that all $p_n$ are identically zero on $V$ and
$p_n = 1$ on $W_n$.  But now since $\mathbb{R}$ is locally connected,
so we can write $U$ as a union of connected open sets, and it is
enough to prove the statement for any one of these, so we can assume
$U$ connected.  But when $U$ is connected, a locally constant function
$U \to \{0,1\}$ is constant, so each $p_n$ is just an element of
$\{0,1\}$ and the statement is trivial using the fact that the ambient
classical universe $\mathbf{LPO}_{\mathrm{seq}}$ holds trivially.

\thingy\label{sequential-wlpo-with-some-choice-implies-analytic-wlpo}
Despite ¶\ref{sequential-wlpo-does-not-imply-analytic-wlpo}, note that
a modicum of Choice suffices to give $\mathbf{WLPO}_{\mathbb{R}}$ from
$\mathbf{WLPO}_{\mathrm{seq}}$.  Indeed, assume the latter, and assume
that Choice holds for sequences of inhabited subsets of $\{0,1\}$
(that is: if $P_n \subseteq \{0,1\}$ and every $P_n$ is inhabited,
there exists $(p_n)$ such that $p_n \in P_n$ for all $n$).  We wish to
show $\mathbf{WLPO}_{\mathbb{R}}$.

Let $c\in\mathbb{R}$.  For every $n\in\mathbb{N}$, since $0 < 2^{-n}$,
we have either $|c| < 2^{-n}$ or $0 < |c|$.  By the Choice principle
we assumed (precisely, letting $P_n := \{0 : |c| < 2^{-n}\} \cup \{1 :
0 < |c|\}$, which is inhabited), we can find a binary sequence $(p_n)$
such that $|c| < 2^{-n}$ if $p_n=0$ and $0 < |c|$ if $p_n=1$.  If
there is $n$ such that $p_n=1$ then $|c|>0$, that is $c\apart 0$; so
contrapositively, $c=0$ implies that $(p_n)$ is identically $0$.  But
conversely, if $(p_n)$ is identically $0$ then $|c| < 2^{-n}$ for all
$n$ so that $c=0$.  This shows that $c=0$ if and only if $(p_n)$ is
the zero sequence.  Now $\mathbf{WLPO}_{\mathrm{seq}}$ tells us that
$(p_n)$ is the zero sequence or it is not.  So we conclude that $z$ is
zero or it is not.  This gives $\mathbf{WLPO}_{\mathbb{R}}$, as
claimed.\quad\qedsymbol

\hbox to\hsize{\hrulefill}\bigbreak

\thingy\label{wllpo-and-friends} Now let $\mathbb{R}\setminus\{0\} :=
\{t \in \mathbb{R} : \neg(t=0)\}$, and consider the following
principles:

\begin{itemize}
\item “$\mathbf{DEC}(\mathbb{R}\setminus\{0\})$”: There exists subsets
  $A,B \subseteq \mathbb{R}\setminus\{0\}$ such that $A$ and $B$ are
  inhabited, $A \cap B = \varnothing$ and $A \cup B =
  \mathbb{R}\setminus\{0\}$.
\item “$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$”: There exists
  subsets $A,B \subseteq \mathbb{R}\setminus\{0\}$ such $-1\in A$ and
  $1\in B$, and $A \cap B = \varnothing$ and $A \cup B =
  \mathbb{R}\setminus\{0\}$.
\item “$\mathbf{WLLPO}_{\mathbb{R}}$” (also known as
  $\mathbf{MP}^\vee_{\mathbb{R}}$): Every $c\in
  \mathbb{R}\setminus\{0\}$ satisfies $c\leq 0$ or $c\geq 0$.
\item “$\mathbf{WLLPO}_{\mathrm{seq}}$” (also known as
  $\mathbf{MP}^\vee_{\mathrm{seq}}$): If $(p_n)$ and $(q_n)$ are
  binary sequences not both identically zero then one of them is not
  identically zero (i.e., if $\neg(\forall n.(p_n=0) \land \forall
  n.(q_n=0))$, then $\neg\forall n.(p_n=0)$ or $\neg\forall
  n.(q_n=0)$).
\end{itemize}

\thingy Trivially, $\mathbf{DEC'}(\mathbb{R}\setminus\{0\}) \;
\Longrightarrow \; \mathbf{DEC}(\mathbb{R}\setminus\{0\})$.

As in ¶\ref{dec-vs-chi-function},
$\mathbf{DEC}(\mathbb{R}\setminus\{0\})$ can be rephrased as the
existence of a function $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$
such that $\chi(a) = 0$ and $\chi(b) = 1$ for some $a$ and $b$ in
$\mathbb{R}\setminus\{0\}$.  Unlike in ¶\ref{dec-vs-chi-function},
however, there is no obvious way to assume, say, $a = -1$ and $b = 1$,
which is why we introduce the perhaps more natural
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$, which can be rephrased as
the existence of a function
$\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that $\chi(-1) =
0$ and $\chi(1) = 1$.  We \emph{can}, however, do something with $b$:

\begin{lem}[Mohammad Tahmasbi]\label{dec-r0-reduction}
In the above formulation of $\mathbf{DEC}(\mathbb{R}\setminus\{0\})$,
we can additionally assume $a<b$ and $b=1$.  In other words,
$\mathbf{DEC}(\mathbb{R}\setminus\{0\})$ is equivalent to the
statement that there exists a function
$\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that $\chi(a) = 0$
for some $a<1$ in $\mathbb{R}\setminus\{0\}$ and $\chi(1) = 1$.
\end{lem}

(To point out a tempting mistake which the author made at one point,
we cannot get $b=1$ straightforwardly by replacing $\chi$ by $t
\mapsto \chi(bt)$: this is indeed defined on
$\mathbb{R}\setminus\{0\}$ since $\neg(b=0)$ and $\neg(t=0)$ imply
$\neg(bt=0)$, but after this replacement is then no longer clear that
there exists $a'$ such that $\chi(a') = 0$, since we cannot
constructively assert that the equation $bt=a$ has a solution when
$\neg(b=0)$.  We need to proceed with more care in the following
proof.)

\begin{proof}[Proof of lemma \ref{dec-r0-reduction}]
We assume the existence of a function
$\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that $\chi(a) = 0$
and $\chi(b) = 1$ for some $a$ and $b$ in $\mathbb{R}\setminus\{0\}$,
and our goal is to achieve the same conclusion with the additional
constraints $a<b$ and $b=1$.

Let us first achieve $a<b$ (still with $\chi(a)=0$ and $\chi(b)=1$).
To this effect, note that either $a<b$ or $b<a+1$.  In the first case
we are done.  In the latter case, note that $a+1<0$ or $0<a+2$.  In
the subcase $b<a+1<0$ (note in particular $\neg(a+1=0)$), let us
consider the value $\chi(a+1)$, which is either $0$ or $1$.  In the
sub-subcase $\chi(a+1)=0$, we redefine $a,b,\chi$ to be $b,a+1,1-\chi$
so we have achieved the required constraint; in the sub-subcase
$\chi(a+1)=1$, we redefine $a,b$ to be $a,a+1$ so we have achieved the
required constraint.  In the subcase $0<a+2$ (note in particular
$\neg(a+2=0)$), we similarly consider the value $\chi(a+2)$, which is
either $0$ or $1$.  In the sub-subcase $\chi(a+2)=0$, we redefine
$a,b,\chi$ to be $b,a+2,1-\chi$ so we have achieved the required
constraint (since $b<a+1<a+2$); in the sub-subcase $\chi(a+2)=1$, we
redefine $a,b$ to be $a,a+2$ so we have achieved the required
constraint.  Thus, we have proved in all cases the existence of a
function $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that
$\chi(a) = 0$ and $\chi(b) = 1$ for some $a<b$ in
$\mathbb{R}\setminus\{0\}$.

Now let us additionally achieve $b=1$ (still with $\chi(a)=0$ and
$\chi(b)=1$ and $a<b$).  Since $a<b$ we have either $0<b$ or $a<0$.
In the first case we redefine $a,b,\chi$ to be $a/b$, $1$ and
$t\mapsto \chi(bt)$ (note that $b$ is invertible as $b>0$) to obtain
the additional constraint $b=1$.  In the second case, we first
redefine $a,b,\chi$ to be $-b$, $-a$ and $t\mapsto 1-\chi(-t)$, which
reduces us to the first case.  Thus, we have proved in all cases the
existence of a function $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$
such that $\chi(a) = 0$ and $\chi(1) = 1$ for some $a<1$ in
$\mathbb{R}\setminus\{0\}$.
\end{proof}

Maybe the following could come in useful:

\begin{lem}\label{dec-r0-disjunction}
The statement $\mathbf{DEC}(\mathbb{R}\setminus\{0\})$ is equivalent
to the statement that
\begin{itemize}\setlength\itemsep{0pt}
\item\emph{either} $\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ holds,
  that is, there exists $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$
  such that $\chi(-1) = 0$ and $\chi(1) = 1$,
\item\emph{or} there exists
  $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that $\chi(1) =
  \chi(-1) = 1$ and $\chi(a) = \chi(-a) = 0$ for some $a \in
  \mathbb{R}\setminus\{0\}$ (we could call this
  $\mathbf{DEC''}(\mathbb{R}\setminus\{0\})$).
\end{itemize}
\end{lem}
\begin{proof}
It is trivial that each of the disjuncts
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ and
$\mathbf{DEC''}(\mathbb{R}\setminus\{0\})$ implies
$\mathbf{DEC}(\mathbb{R}\setminus\{0\})$.  So we are to prove the
converse.

We have just seen in the previous lemma that
$\mathbf{DEC}(\mathbb{R}\setminus\{0\})$ is equivalent to the
statement that there exists a function
$\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that $\chi(a) = 0$
for some $a<1$ in $\mathbb{R}\setminus\{0\}$ and $\chi(1) = 1$, so we
assume this.

Now consider $\chi(-1)$.  It is either $0$ or $1$.  If it is $0$ then
the first disjunct ($\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$) holds
trivially, and we are done.  If it is $1$, consider $\chi(-a)$ (noting
that $\neg(-a=0)$ since $\neg(a=0)$).  It is either $0$ or $1$.  If it
is $0$ then the second disjunct
($\mathbf{DEC''}(\mathbb{R}\setminus\{0\})$) holds trivially, and we
are done.  Finally, if $\chi(-a)=1$, then replacing $\chi$ by $t
\mapsto \chi(-at)$ brings us again to the first disjunct
($\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$).  So in any case we have
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ or
$\mathbf{DEC''}(\mathbb{R}\setminus\{0\})$, and this concludes the
proof.
\end{proof}

(To point out another tempting mistake which the author made at one
point, in $\mathbf{DEC''}(\mathbb{R}\setminus\{0\})$, the fact that
$\chi(a) = \chi(-a) = 0$ need not entail $\chi(|a|) = 0$.  If we
\emph{had} $\chi(|a|) = 0$ then we could redefine $\chi$ as $t \mapsto
\chi(\inf(1, |a| + |t|))$ to obtain $\mathbf{DEC}(\mathbb{R})$
from ¶\ref{wlpo-and-friends}–\ref{dec-vs-chi-function}, from which we
already know from theorem \ref{dec-r-equivalent-to-analytic-wlpo} that
$\mathbf{WLPO}_{\mathbb{R}}$ and in particular
$\mathbf{WLLPO}_{\mathbb{R}}$ follows as explained
in ¶\ref{analytic-wlpo-implies-analytic-wllpo}.  Alas!, one cannot
constructively conclude $\chi(|a|) = 0$ from $\chi(a) = \chi(-a) = 0$
unless one somehow already knew $\mathbf{WLLPO}_{\mathbb{R}}$.)

\thingy\label{analytic-wlpo-implies-analytic-wllpo} We point out the
standard fact that $\mathbf{WLPO}_{\mathbb{R}} \; \Longrightarrow \;
\mathbf{WLLPO}_{\mathbb{R}}$.  To see this, assume
$\mathbf{WLPO}_{\mathbb{R}}$ holds, and let $c \in
\mathbb{R}\setminus\{0\}$.  By $\mathbf{WLPO}_{\mathbb{R}}$, we have
either $\sup(x,0) = 0$ or $\neg(\sup(x,0) = 0)$.  Now $x\leq 0$ is
equivalent to $\sup(x,0) = 0$, so this says that $x\leq 0$ or
$\neg(x\leq 0)$.  But the latter implies $x\geq 0$ (because $x<0$
implies $x\leq 0$, so contrapositively, $\neg(x\leq 0)$ implies
$\neg(x<0)$ which is just $x\geq 0$).  So we have proved $x\leq 0$ or
$x\geq 0$.  This gives $\mathbf{WLLPO}_{\mathbb{R}}$.\quad\qedsymbol

\thingy\label{sequential-wlpo-implies-sequential-wllpo} Let us
similarly point out that $\mathbf{WLPO}_{\mathrm{seq}} \;
\Longrightarrow \; \mathbf{WLLPO}_{\mathrm{seq}}$.  To see this,
assume $\mathbf{WLPO}_{\mathrm{seq}}$ holds, and let $(p_n)$ and
$(q_n)$ be binary sequences such that $\neg(\forall n.(p_n=0) \land
\forall n.(q_n=0))$.  By $\mathbf{WLPO}_{\mathrm{seq}}$, we have
either $\forall n.(p_n=0)$ or $\neg\forall n.(p_n=0)$, and similarly
either $\forall n.(q_n=0)$ or $\neg\forall n.(q_n=0)$.  This gives us
four cases: the case where $\forall n.(p_n=0)$ and $\forall n.(q_n=0)$
is ruled out by our assumption, and in all three remaining cases, the
conclusion that $\neg\forall n.(p_n=0)$ or $\neg\forall n.(q_n=0)$ is
immediate.  So we have proved
$\mathbf{WLLPO}_{\mathrm{seq}}$.\quad\qedsymbol

\thingy There are various standard equivalent formulations of
$\mathbf{WLLPO}_{\mathrm{seq}}$.  Rather than using two binary
sequences $(p_n)$ and $(q_n)$, it is sometimes more convenient to
group them into a single one by $s_{2n} = p_n$ and $s_{2n+1} = q_n$;
the statement $\mathbf{WLLPO}_{\mathrm{seq}}$ is then seen to be
equivalent to the folllowing: “if a binary sequence is not identically
zero then either its even terms are not identically zero or its odd
terms are not identically zero”.

Furthermore, it is sometimes convenient to replace $(s_m)$ by the
sequence whose $m$-th term equals $s_m$ except if there exists $k<m$
such that $s_k=1$ in which case it equals $0$ (so that $(s_m)$ has at
most one term equal to $1$).  This shows that in
$\mathbf{WLLPO}_{\mathrm{seq}}$ we can assume that $(p_n)$ and $(q_n)$
jointly\footnote{To avoid any possible doubt, the clause “the binary
  sequences $(p_n)$ and $(q_n)$ jointly have at most one term equal
  to $1$” means that if one term of one of the sequences is $1$ then
  every other term of that sequence and every term of the other
  sequence are $0$.}  have at most one term equal to $1$ (as well as
not being both zero); furthermore, the conclusion can then be stated
as the fact that either $(p_n)$ is the zero sequence or $(q_n)$ is so.
In other words, $\mathbf{WLLPO}_{\mathrm{seq}}$ is equivalent to: “if
two binary sequences jointly have at most one term equal to $1$ and if
they are not both identically zero, then one of them is identically
zero”.

\thingy\label{analytic-wllpo-implies-sequential-wllpo} Similarly
to ¶\ref{analytic-wlpo-implies-sequential-wlpo}, let us prove the
standard fact that $\mathbf{WLLPO}_{\mathbb{R}}$ implies
$\mathbf{WLLPO}_{\mathrm{seq}}$.  If $(p_n)$ and $(q_n)$ are binary
sequence which jointly have at most one term equal to $1$ and which
are not both identically zero, we define a real sequence $z_n :=
\sum_{k=0}^n (p_k-q_k)\cdot 2^{-k}$.  Clearly this sequence is Cauchy
with modulus $|z_m-z_n| \leq 2^{-\min(m,n)}$, so it has a limit $z$.
If there is $n$ such that $p_n = 1$, then $z = 2^{-n}$, so $z > 0$,
and if there is $n$ such that $q_n = 1$, then $z = -2^{-n}$, so $z <
0$; so contrapositively, $z\leq 0$ implies that $(p_n)$ is
identically $0$, and $z\geq 0$ implies that $(q_n)$ is
identically $0$.  But conversely, if $(p_n)$ is identically $0$ then
trivially $z\leq 0$, and if $(q_n)$ is identically $0$ then trivially
$z\geq 0$.  This shows that $(p_n)$ is the zero sequence if and only
if $z\leq 0$, and $(q_n)$ is the zero sequence if and only if $z\geq
0$.  Now $\mathbf{WLLPO}_{\mathbb{R}}$ tells us that $\neg(z=0)$
implies $z\leq 0$ or $z\geq 0$.  So we conclude that $(p_n)$ is the
zero sequence or it is not.  This gives
$\mathbf{WLLPO}_{\mathrm{seq}}$.\quad\qedsymbol

\thingy As an aside, to see that the converse of
$\mathbf{WLLPO}_{\mathbb{R}} \; \Longrightarrow \;
\mathbf{WLLPO}_{\mathrm{seq}}$ generally does not hold, we use the
same topological model as
in ¶\ref{sequential-wlpo-does-not-imply-analytic-wlpo}, i.e., the
topos of sheaves over $\mathbb{R}$.  We have already pointed out there
that it satisfies $\mathbf{WLPO}_{\mathrm{seq}}$ (which is stronger
than $\mathbf{WLLPO}_{\mathrm{seq}}$
per ¶\ref{sequential-wlpo-implies-sequential-wllpo}).

But even $\mathbf{WLLPO}_{\mathbb{R}}$ does not hold in the model,
since it unwinds to saying that if $c$ is a continuous real-valued
function on an open subset $U$ of $\mathbb{R}$ which vanishes on no
nonempty open subset of $U$ then $U$ is the union of an open set on
which $c\leq 0$ one on which $c\geq 0$; but the function
$\mathbb{R}\to\mathbb{R}$ given by $x \mapsto x$ provides a
counterexample to this.

\thingy The implication $\mathbf{WLLPO}_{\mathbb{R}} \;
\Longrightarrow \; \mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ is
trivial.  Indeed, $\mathbf{WLLPO}_{\mathbb{R}}$ asserts precisely that
$\mathbb{R}\setminus\{0\}$ is the disjoint union of $\{t : t\gtrdot
0\}$ and $\{t : t\lessdot 0\}$ (here we write $x\gtrdot y$ for $(x\geq
y) \land \neg (x=y)$, or equivalently, $\neg(x\leq y)$), with of
course $1\gtrdot 0$ and $-1\lessdot 0$.

\thingy To summarize what has been said, the following implications
hold:
\begin{center}
\begin{tikzpicture}
\matrix(diag)[matrix of math nodes,column sep=2em,row sep=2ex]{
\mathbf{WLPO}_{\mathbb{R}}
&\mathbf{WLLPO}_{\mathbb{R}}
&\mathbf{DEC'}(\mathbb{R}\setminus\{0\})
&\mathbf{DEC}(\mathbb{R}\setminus\{0\})\\
\mathbf{WLPO}_{\mathrm{seq}}&\mathbf{WLLPO}_{\mathrm{seq}}&&\\};
\draw[->,double equal sign distance, -{implies[scale=1.5]}] (diag-1-1) -- (diag-1-2);
\draw[->,double equal sign distance, -{implies[scale=1.5]}] (diag-1-2) -- (diag-1-3);
\draw[->,double equal sign distance, -{implies[scale=1.5]}] (diag-1-3) -- (diag-1-4);
\draw[->,double equal sign distance, -{implies[scale=1.5]}] (diag-2-1) -- (diag-2-2);
\draw[->,double equal sign distance, -{implies[scale=1.5]}] (diag-1-1) -- (diag-2-1);
\draw[->,double equal sign distance, -{implies[scale=1.5]}] (diag-1-2) -- (diag-2-2);
\end{tikzpicture}
\end{center}

Neither of the vertical arrows is reversible in general.
Countermodels showing that the converse of both $\mathbf{WLPO} \;
\Longrightarrow \; \mathbf{WLLPO}$ implications does not hold in
general are also well known: Hyland's effective topos, for example,
satisfies all forms of $\mathbf{WLLPO}$ (as they follow from Markov's
principle) but no form of $\mathbf{WLPO}$: we do not elaborate here as
this is not our focus.

\begin{ques}\label{dec-r0-versus-wllpo-question}
Is $\mathbf{DEC}(\mathbb{R}\setminus\{0\})$ equivalent to
$\mathbf{WLLPO}_{\mathbb{R}}$?  Is
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ equivalent to
$\mathbf{WLLPO}_{\mathbb{R}}$?
\end{ques}

We at least have the following partial analogue of
lemma \ref{dec-r-implies-sequential-wlpo}:

\begin{lem}\label{decprime-r0-implies-sequential-wllpo}
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ implies $\mathbf{WLLPO}_{\mathrm{seq}}$
\end{lem}

\begin{proof}
Assume $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ satisfies
$\chi(-1)=0$ and $\chi(1)=1$.

Define real sequences $(u_n)$ and $(v_n)$ by induction as follows: put
$u_0=-1$ and $v_0=1$, and then :
\begin{itemize}\setlength\itemsep{0pt}
\item when $\chi(\frac{u_n+2v_n}{3})=0$ let $u_{n+1} =
  \frac{u_n+2v_n}{3}$ and $v_{n+1} = v_n$,
\item when $\chi(\frac{u_n+2v_n}{3})=1$ and
  $\chi(\frac{2u_n+v_n}{3})=1$ let $u_{n+1} = u_n$ and
  $v_{n+1} = \frac{2u_n+v_n}{3}$,
\item when $\chi(\frac{u_n+2v_n}{3})=1$ and
  $\chi(\frac{2u_n+v_n}{3})=0$ let $u_{n+1} = \frac{2u_n+v_n}{3}$ and
  $v_{n+1} = \frac{u_n+2v_n}{2}$.
\end{itemize}

It is easy to see inductively that $(u_n)$ and $(v_n)$ are nonzero
rationals (with denominator dividing $3^n$): indeed, considering the
construction up to $n$, so long as the third case happens we have $u_k
= -3^{-k}$ and $v_k = 3^{-k}$, and as soon as the first (resp. second)
case happens we have $u_n,v_n>0$ (resp. $u_n,v_n<0$) from then on.
This justifies that the construction can be carried out (the function
$\chi$ is evaluated on nonzero rationals).

Obviously we have $\chi(u_n)=0$ and $\chi(v_n)=1$ for all $n$ by
induction.  Furthermore, $(u_n)$ and $(v_n)$ satisfy $-1\leq u_m\leq
u_n\leq v_n\leq v_m\leq 1$ when $m\leq n$, and $|u_n-v_n| \leq
3^{-n}$.  In particular, they are Cauchy with modulus $|u_m-u_n| \leq
3^{-\min(m,n)}$ and $|v_m-v_n| \leq 3^{-\min(m,n)}$, and they have the
same limit.  Call $w$ this common limit: we have $|w-u_n| \leq 3^{-n}$
and $|w-v_n| \leq 3^{-n}$.

Now let $(p_n)$ and $(q_n)$ be binary sequences which jointly have at
most one term equal to $1$ and which are not both identically zero.
We wish to show that $(p_n)$ is the zero sequence or that $(q_n)$ is
the zero sequence.

Define a real sequence $(z_n)$ as follows:
\begin{itemize}\setlength\itemsep{0pt}
\item when $p_k=0$ and $q_k=0$ for all $0\leq k\leq n$, let $z_n = w$,
\item when there exists an $0\leq k\leq n$ (necessarily unique) such
  that $p_k=1$, let $z_n = v_k$,
\item when there exists an $0\leq k\leq n$ (necessarily unique) such
  that $q_k=1$, let $z_n = u_k$.
\end{itemize}
(In other words, $z_n$ is constantly $w$ until such a value as $p_k=1$
or $q_k=1$ if it is found, and is then equal to the corresponding
value of $v_k$ or $u_k$.  This makes sense as we have assumed that
$(p_n)$ and $(q_n)$ jointly have at most one term equal to $1$.)  This
sequence is well-defined.

By an easy case distinction as in the proof of
lemma \ref{dec-r-implies-sequential-wlpo}, we have that $(z_n)$ is
Cauchy with modulus $|z_m-z_n| \leq 3^{-\min(m,n)}$.  Therefore it has
a limit $z$.

If there is $k$ such that $p_k=1$ then $z_n$ is equal to $v_k$ for all
$n\geq k$, and in particular, $z = v_k \apart 0$.  Similarly, if there
is $k$ such that $q_k=1$ then $z_n$ is equal to $u_k$ for all $n\geq
k$, and in particular, $z = u_k \apart 0$.  Contrapositively, if $z =
0$ then $(p_n)$ and $(q_n)$ are both identically zero; but we have
assumed that this be not the case: this shows $\neg(z=0)$.  We are now
allowed to speak of $\chi(z)$.  Note that then $\chi(z)=0$ or
$\chi(z)=1$.

Now if there is $k$ such that $p_k=1$ then $z = v_k$ so $\chi(z) =
\chi(v_k) = 1$; and if there is $k$ such that $q_k=1$ then $z = u_k$
so $\chi(z) = \chi(u_k) = 0$.  So contrapositively, $\chi(z) = 0$
implies that $(p_n)$ is identically zero, and $\chi(z) = 1$ implies
that $(q_n)$ is identically zero.  It follows that $(p_n)$ is the zero
sequence or that $(q_n)$ is the zero sequence.

This gives $\mathbf{WLLPO}_{\mathrm{seq}}$, as claimed.
\end{proof}

\thingy\label{sequential-wllpo-with-some-choice-implies-analytic-wllpo}
Like in ¶\ref{sequential-wlpo-with-some-choice-implies-analytic-wlpo},
a modicum of Choice suffices to give $\mathbf{WLLPO}_{\mathbb{R}}$
from $\mathbf{WLLPO}_{\mathrm{seq}}$.  Indeed, assume again like there
that Choice holds for sequences of inhabited subsets of $\{0,1\}$, and
let us show that $\mathbf{WLLPO}_{\mathrm{seq}}$ implies
$\mathbf{WLLPO}_{\mathbb{R}}$ under this assumption.  Let $c \in
\mathbb{R}\setminus\{0\}$.  For any $n\in\mathbb{N}$ we have either
$c<2^{-n}$ or $c>0$.  By the Choice principle we assumed (just like
in ¶\ref{sequential-wlpo-with-some-choice-implies-analytic-wlpo}), we
can find binary sequence $(p_n)$ such that $c<2^{-n}$ if $p_n=0$ and
$c>0$ if $p_n=1$; similarly, we can find $(q_n)$ such that $c>-2^{-n}$
if $q_n=0$ and $c<0$ if $q_n=1$.  Now if there is $n$ such that
$p_n=1$ then $c>0$, so contrapositively, $c\leq 0$ implies that
$(p_n)$ is identically $0$.  But conversely, if $(p_n)$ is
identically $0$ then $c\leq 2^{-n}$ for all $n$ so that $c\leq 0$.
This shows that $c\leq 0$ if and only if $(p_n)$ is the zero sequence.
Analogously, $c\geq 0$ if and only if $(q_n)$ is the zero sequence.
Our assumption that $\neg(c=0)$ implies that $(p_n)$ and $(q_n)$ are
not both identically zero, so $\mathbf{WLLPO}_{\mathrm{seq}}$ tells us
that one of them is not identically zero, which implies that one of
$c\leq 0$ or $c\geq 0$ must be false, giving $c\gtrdot 0$ or
$c\lessdot 0$.  This gives $\mathbf{WLLPO}_{\mathbb{R}}$, as claimed.

\thingy\emph{Comments and thoughts:}

The main issue in the question of whether
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ implies
$\mathbf{WLLPO}_{\mathbb{R}}$ is the absence of Choice.  As explained
in ¶\ref{sequential-wllpo-with-some-choice-implies-analytic-wllpo}, if
we have a modicum of Choice, then $\mathbf{WLLPO}_{\mathrm{seq}}$
implies $\mathbf{WLLPO}_{\mathbb{R}}$, and therefore
lemma \ref{decprime-r0-implies-sequential-wllpo} shows that
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ implies
$\mathbf{WLLPO}_{\mathbb{R}}$ under this assumption.

The idea to show that $\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$
implies $\mathbf{WLLPO}_{\mathbb{R}}$ without using Choice should be
to replace Choice by a judicious use of the $\chi$ function.  Of
course we can replace $\chi$ by $t \mapsto \chi(\sup(-1,\inf(t,1)))$
so as to get $\chi(t)=0$ if $t\leq -1$ and $\chi(t)=1$ if $t\geq 1$.
We would \emph{like} to do something like this: consider $\chi(2^{n+1}
c - 1)$: if it is $0$ then we know $c \leq 2^{-n}$ and we put $p_n =
0$ while if it is $1$ then we know $c \geq 0$ and we put $p_n = 1$;
and analogously, consider $\chi(2^{n+1} c + 1)$: if it is $1$ then we
know $c \geq -2^{-n}$ and we put $q_n = 0$ while if it is $0$ then we
know $c \leq 0$ and we put $q_n = 1$; if this could do this, the rest
of the proof of
¶\ref{sequential-wllpo-with-some-choice-implies-analytic-wllpo} would
work pretty much the same and we would get $c\leq 0$ or $c\geq 0$.
The problem with this “proof” is that we cannot consider $\chi(2^n c -
1)$ without first knowing that $\neg(c=2^{-n})$; and there does not
seem to be any way to attain such a non-equality without first being
able to separate $c$ from $0$ in some way.  (Of course, one way to get
$\neg(c=2^{-n})$ is to have $\chi(c) \neq \chi(2^{-n})$ but there is
no reason to think the function $\chi$ would oblige us this way.)

Considering just $\chi(2^n c)$ is legitimate, and this gives us a
binary sequence $(r_n)$ which “eventually knows” whether $c\geq 0$ or
$c\leq 0$ in the sense that $r_n$ is eventually $0$ (in the sense:
$\exists n_0.\forall n\geq n_0.(r_n=0)$) if $c<0$, and eventually $1$
if $c>0$.  So we can deduce $\mathbf{WLLPO}_{\mathbb{R}}$ from
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ combined with the following
principle: “If $(r_n)$ is a binary sequence then either $(r_n)$ is not
eventually $0$ or $(r_n)$ is not eventually $1$.”  However, it is not
hard to see that the quoted principle is, in fact, equivalent to
$\mathbf{WLPO}_{\mathrm{seq}}$.  (Sketch of proof.  If it holds, then
we get $\mathbf{WLPO}_{\mathrm{seq}}$ for a binary sequence $(p_n)$ by
defining $r_n$ to be $1$ if there is $0\leq k\leq n$ such that $p_n=1$
and $0$ otherwise.  Conversely, if $\mathbf{WLPO}_{\mathrm{seq}}$
holds and if $(r_n)$ is a binary sequence, we first define $r'_n \in
\{0,1,{?}\}$ to be $0$ if $\forall m\geq n.(r_m=0)$, $1$ if $\forall
m\geq n.(r_m=1)$ and “${?}$” if neither holds:
$\mathbf{WLPO}_{\mathrm{seq}}$ ensures that this disjunction is
exhaustive, so that $r'_n$ makes sense; but further application of
$\mathbf{WLPO}_{\mathrm{seq}}$ allows us to conclude that either
$r'_n$ consists exclusively of ${?}$, or it is false that it does not
take the value $0$, or it is false that it does not take the value
$1$.  In the first two cases, $(r_n)$ is not eventually $1$, and in
the third case, $(r_n)$ is not eventually $0$.~\qedsymbol) So this
shows that $\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ and
$\mathbf{WLPO}_{\mathrm{seq}}$ together imply
$\mathbf{WLLPO}_{\mathbb{R}}$, which is a far cry from answering even
the second part of question \ref{dec-r0-versus-wllpo-question}.

\thingy\emph{More comments and thoughts:}

Related to the question of whether
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ implies
$\mathbf{WLLPO}_{\mathbb{R}}$, we might consider the following
(somewhat loosely defined) \emph{game}, in the context of classical
mathematics:

Alice has hidden a nonzero real number $c$ in a black box, and Bob's
goal is to decide whether $c\leq 0$ or whether $c\geq 0$ (of course,
since we are talking classically here, exactly one of the two holds,
and we can write them as $c<0$ resp. $c>0$).  Alice has also chosen a
function $\chi\colon\mathbb{R}\setminus\{0\}\to\{0,1\}$ such that
$\chi(t)=0$ if $t\leq-1$ and $\chi(t)=1$ if $t\geq 1$ (or maybe she
doesn't need to choose it aforehand, but every time it is evaluated
she must commit to a value and cannot change it afterwards).  Bob can
ask Alice to perform certain computations on numbers hidden in boxes,
such as sums, differences, products, binary $\max$ and $\min$ (or even
computing the inverse of $x$ in a box if Bob can also produce a
positive rational lower bound on $|x|$): Alice will do these
computations for him, and return the result still in a box (and of
course she also will willingly put an explicitly given costant in a
box).  Furthermore, Bob can ask Alice to evaluate $\chi$ on the
content of a box (or on an explicitly given number): in this case, Bob
gets to see the actual result, $0$ or $1$.  But Bob can only ask for
the evaluation of $\chi$ provided he is certain (i.e., can prove) that
the input is $\neq 0$.  Does Bob have a deterministic strategy that
guarantees success in finite time?

(As explained in the previous paragraphs, if we remove the restriction
that $\chi$ can only be evaluated on inputs $\neq 0$, then Bob has a
strategy that consists of computing $\chi(2^{n+1} c - 1)$ and
$\chi(2^{n+1} c + 1)$ until one of the former returns $1$ or one of
the latter returns $0$, which is bound to happen in finite time.  And
with the restriction on $\chi$ but granting Bob a form of omniscience,
he can also do it by evaluating $\chi(2^n c)$ and divining whether it
is eventually $0$ or eventually $1$.)

I \emph{suspect} that Bob does not have a winning strategy for this
game (intuitively, because we can only get the required information
that the input of $\chi$ is nonzero by knowing something which makes
the output of $\chi$ useless; also, because any deterministic strategy
of Bob must apply to the particular case where $\chi$ is $1$ on the
positives and $0$ on the negatives, and then everything is continuous
in $c$), but I have been unable to actually prove it.

In any case, the exact relation between the (classical mathematics)
game I just defined and the question of whether
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ implies
$\mathbf{WLLPO}_{\mathbb{R}}$ constructively is also unclear.  A
winning strategy for the game should probably give a proof of
$\mathbf{WLLPO}_{\mathbb{R}}$ from
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ together with perhaps
Markov's principle (which is stronger than
$\mathbf{WLLPO}_{\mathrm{seq}}$ but hopefully not too distant).  But
conversely, whether a constructive implication from
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ to
$\mathbf{WLLPO}_{\mathbb{R}}$ would necessarily come in the form of a
winning strategy to this game is highly unclear to me: there are,
after all, other ways to define a real number constructively, such as
by the limit of a sequence or by a Dedekind cut (and it could be
important that we are working with Dedekind reals so maybe we
\emph{cannot} do things with sequences, let alone Cauchy sequences
having a modulus of convergence; but how does one usefully produce
Dedekind cuts from the function $\chi$?).

Maybe one should start by combining the proofs of lemmate
\ref{dec-r-implies-sequential-wlpo} and \ref{dec-r-and-sequential-wlpo-imply-analytic-wlpo}
into a single one as a source of inspiration on how to deal with the
analogous problem for $\mathbf{WLLPO}_{\mathbb{R}}$.

Another possible idea might be to try deducing
$\mathbf{WLLPO}_{\mathbb{R}}$ from
$\mathbf{DEC'}(\mathbb{R}\setminus\{0\})$ in a manner similar to
lemma \ref{decprime-r0-implies-sequential-wllpo} but working directly
from signed-bit representations as defined in Lubarsky \& Richman,
“Signed-Bit Representations of Real Numbers”, \textit{J. Log. Anal.}
\textbf{1} (2009), paper 10 (esp. theorems 2.3 \& 2.4), or
alternatively some kind of multivalued\footnote{It seems to be part of
the folklore that some kind of multivalued Cauchy reals are equivalent
to Dedekind reals, but references for this are sketchy at best.}
Cauchy sequence: instead of combining \emph{sequences} $(p_n)$ and
$(q_n)$ with the \emph{sequences} $(u_n)$ and $(v_n)$ (and $w$) to
produce a \emph{sequence} $(z_n)$ which converges to a limit we can
disjunct on, we would rather use some kind of multivalued sequence in
several of these places.  But I have been unable to do this.

\end{document}

See https://mathoverflow.net/questions/479398/does-the-decomposability-of-mathbbr-imply-analytic-llpo/479501#479501 for context.