Jakob1d ago
Is it true constructively that every element x of R^2 with the Euclidean norm (or more general normed vector spaces) has the form r*u with r in [0, oo) and ||u|| = 1? I assume the fact that there exists no continuous section of the map (r, u) |-> r * u means that this is not a constructive fact, but I'm not sure if this logical reasoning is sound?
Show threadjcreed

@jdw I think not, although I'm not 100% confident that it might not depend in some fiddly way on how you constructively define the reals.

My intuition is this: if your proposition were true, you could define a total function R -> R which is -1 below 0, and +1 above zero. This should be discontinuous regardless of the value at zero, and constructively we shouldn't be able to make a total discontinuous function R -> R.

Mar 28 at 7:15pmWeb
Show threadjcreed1d ago
@jdw The R -> R function I have in mind is, simply: given any x : R, consider the vector (x, 0). Use your proposition to extract its normalization u = (ux, uy). Return ux.
Show threadJakob1d ago
@jcreed If we interpret the existential statement in my proposition in a proof-irrelevant way, then you are using the axiom of choice here, right?
Show threadjcreed1d ago

@jdw Let's say your proposition is

A = "for any v : R^2, there exist suitable r, u such that v = r * u"

and a variation of that is

A' = "for any v : R^2, there *merely* exist suitable r, u such that v = r * u"

My current belief is that:

A doesn't imply falsehood
A implies something decisively anticonstructive, i.e. the existence of a total discontinuous function R -> R

it does not yet seem obvious to me that A' necessarily implies anything decisively anticonstructive the way A does

Show threadjcreed1d ago
@jdw I'm using "merely* in the HoTT sense of truncatons ~= proof irrelevance... my natural tendency at this point in my evolution as a mathematician is to treat "forall" and "exist" as always meaning pi and sigma, and "merely exist" is a sigma wrapped with a propositional truncation