Piecewise linear functions in constructive mathematics Is is possible to constructively prove that, for any function $f:\mathbb{R}\to\mathbb{R}$ piecewise linear, the absolute value $|f|:\mathbb{R}\to\mathbb{R}$ is also piecewise linear ?
"Constructively" is for example in the sense of Bishop's constructive mathematics, not in the sense of algorithms (recursive functions).
Piecewise linear can either mean to produce an ordered list of real numbers $a_1<\dots <a_n$ such as $|f|$ is linear on each $[a_i,a_{i+1}]$, or produce an unordered list of corner functions (only 1 angular point) of which $|f|$ is the sum. In both cases, the number of angular points of $f$ and $|f|$ is assumed to be finite.
It seems hard, because that would require to exactly compare the values of $f$ with $0$, to know when to insert angular points $a_i$ for $|f|$. Such a comparison of real numbers is not constructive.
Even on a single interval, $f : [a,b] \to\mathbb{R}$ linear, it seems hard. If there is a point $c\in \, ]a,b[$ such as $f(c)=0$, then $|f|$ is piecewise linear on the subdivision $a<c<b$. Otherwise $|f|$ is piecewise linear on $a<b$. Constructively you would need to know which case it is, but then you would need to exactly compare $f(a)$ and $f(b)$ with $0$.
 A: Say that a function $f \colon \mathbb{R} \to \mathbb{R}$ is somewhere linear if there are rational numbers $p < q$ such that the restriction of $f$ to $[p, q]$ is linear. Note that every piecewise linear function is somewhere linear. I claim that it is not constructively provable that $|f|$ is somewhere linear whenever $f$ is linear.
It is consistent with Bishop style constructive mathematics that continuous choice holds: that if $(\forall \alpha \in \mathbb{N}^\mathbb{N})(\exists n \in \mathbb{N})\phi(\alpha, n)$, then there is a continuous function $F \colon \mathbb{N}^\mathbb{N} \to \mathbb{N}$ such that for all $\alpha \in \mathbb{N}^ \mathbb{N}$, we have $\phi(\alpha, F(\alpha))$. It follows that the same is true if we take the domain to be $2^\mathbb{N} \times 2^\mathbb{N}$, ie given $(\forall \alpha, \beta \in 2^\mathbb{N})(\exists n \in \mathbb{N})\phi(\alpha, \beta, n)$ we have continuous $F \colon 2^\mathbb{N} \times 2^\mathbb{N} \to \mathbb{N}$. I'll show that the above statement is non constructive, by showing it contradicts continuous choice.
Given $\alpha, \beta \in 2^\mathbb{N}$, write $a$ for $\sum_{i = 0}^\infty \alpha(i) 2^{-i}$ and $b$ for $\sum_{i = 0}^\infty \beta(i) 2^{-i}$. Then there exists a natural number encoding rationals $p, q$ such that the function $f(x) := | a x + b |$ is linear on $[p, q]$, by assumption. By continuous choice, in particular continuity at the point $(\lambda n.0, \lambda n.0)$, we have a single choice of rational numbers $p, q$ and a natural number $N$ that whenever $\alpha(n) = 0$ and $\beta(n) = 0$ for $n < N$, $| a x + b |$ is linear on $[p, q]$. However, this gives a contradiction, because for any given $p < q$ we can find $\alpha, \beta$ with $\alpha(n) = \beta(n) = 0$ for $n < N$, such that the corresponding function $a x + b$ crosses the $x$-axis between $p$ and $q$.
