Can a space filling curve exist in iset.mm?

[jkingdon]

This is probably a bit of a stretch given the current state of iset.mm (for example, we have some theorems about continuity but nothing yet about dependent choice), but it is easily stated and perhaps fun.

The problem: is there a surjective curve from [0,1] to [0,1]²? The answer is that this should be provable with iset.mm plus dependent choice, but cannot be proved in iset.mm alone. See more explanation and some nice visuals at https://math.andrej.com/2024/01/30/space-filling-curves-constructively/

For the first part, the proof in the blog post should be formalizable, although we'd need to state dependent choice (analogous to CCHOICE) and prove some helper theorems which make it easy to use.

For the second part, the blog post describes a topos which does not allow this sort of curve. Although perhaps we could go down that road somehow, showing impossibility would presumably be easier if there is a way to derive a taboo from the existence of the curve.

[jkingdon]

On mastodon Andrej Bauer writes:

If you're going to formalize the theorem which says that, assuming Dependent choice, there are space-filling curves, then I would suggest a different proof:

1) An inhabited complete separable totally bounded metric X space is the image of the Cantor set by a uniformly continuous map.

2) Any uniformly continuous map from the Canto set (seen as a subspace of [0,1]) to a [0,1] can be extended to [0,1].

[digama0]

I think we can show a taboo from the existence of the alpha = 1/2 Hilbert curve: Consider the point (x, 1/4) for 0 < x < 1, that is, points on a line which crosses from region 1 to region 4 of the first stage of the construction. Suppose that the Hilbert curve γ : [0, 1] -> [0, 1]^2 is surjective, and let t be such that γ(t) = (x, 1/4). If 1/4 < t < 3/4 then we get a contradiction because the point would be in regions 2 or 3, hence weak trichotomy t < 3/4 \/ 1/4 < t can be strengthened to t <= 1/4 \/ 3/4 <= t. But t <= 1/4 implies x <= 1/2 and 3/4 <= t implies 1/2 <= x. Since x was arbitrary we have proved strong trichotomy, x <= 1/2 \/ 1/2 <= x.

[digama0]

Regarding the usage of DC for the $\alpha > 1/2$ Hilbert curve, I think it's not essential, and one can reduce it at least to countable choice: Let $T^\alpha_0,\dots, T^\alpha_3$ be the four transformations defined in Bauer's post and let $R^\alpha_i$ be the range of $T^\alpha_i$ (four squares that cover $[0,1]^2$ with overlap) but without their outer edges (i.e. $R^\alpha0=(-\infty,\alpha]\times (-\infty,\alpha]$, etc.) so that they are all quarter-planes. Let $T^\alpha{as} = T^\alpha_{a1} \circ \dots T^\alpha{a_n}$ represent some sequence of those transformations. Let $1/2<\beta<\alpha$ so that $(R^\beta_i)^c$ and $R^\alphai$ cover $\mathbb{R}^2$ with overlap. Now for each $as\in\{0,...,3\}^*,i\in\{0,...,3\}$ we have $T^\alpha{as}[R^\alphai]\cup(T^\alpha{as}[R^\beta_i])^c$ covering $\mathbb{R}^2$ with overlap, so for $x\in[0,1]^2$ we have that it is in one of the two sets.

Now, fix $x\in[0,1]^2$. There are countably many choices of $as,i$ above, so using countable choice we obtain a function $f$ which returns $\mathsf{T}$ if $x$ is in $T^\alpha_{as}[R^\alphai]$ and $\mathsf{F}$ if it is in $(T^\alpha{as}[R^\beta_i])^c$. Let $g(as)$ be the following algorithm:

• For $i$ in 0..3:
  • If $f(as,i)=\mathsf{T}$ (that is, $x\in T^\alpha_{as}[R^\alpha_i]$), then return $i$
• else return $\bot$.

Now suppose $x\in T^\alpha{as}[[0,1]^2]$. If $g(as)=\bot$ then $f(as,i)=\mathsf{F}$ for all $i$, and we obtain a contradiction because the sets $(T^\alpha{as}[R^\betai])^c$ have empty intersection. Therefore $g(as)\in\{0,...,3\}$ and $f(as,g(as))=\mathsf{T}$, and hence $x\in T^\alpha{as,g(as)}[[0,1]^2]$.

We define $i_n\in\{0,...,3\}$ by the recurrence $i_n=g(i0,...,i{n-1})$, and get an infinite sequence with the property that $x\in T^\alpha_{i0,\dots,i{n-1}}[[0,1]^2]$ for all $n$; thus $t=0.i_0i_1\dots$ (written in quaternary) is the desired point.

[frogeyedpeas]

@digama0 how did you get the LaTeX to render so nicely in github? I would've liked to use that feature a lot in an old job I used to work at.

[digama0]

There is nothing you really need to do, it is supported out of the box: https://github.blog/2022-05-19-math-support-in-markdown/

Docs: https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/writing-mathematical-expressions