Fusible numbers

[Ryota KUROKI]

Dear All,

I recently heard about the fusible numbers.

https://arxiv.org/abs/2003.14342v9

The proof that the set of fusible numbers is well-founded is highly non-constructive (see Lemma 2.3). I wonder if we can translate this proof into a constructive one.

Well-foundedness can be defined via accessibility (e.g., Definition 10.3.3 of the HoTT Book https://homotopytypetheory.org/book ).

Fusibility is defined by a generalized inductive definition.

Sincerely,

Ryota Kuroki

Graduate School of Mathematical Sciences, The University of Tokyo, Japan