The name "real numbers" predates the first formal definitions. The philosophical debate that I pointed to predates the general acceptance of the standardizatio

The name "real numbers" predates the first formal definitions. The philosophical debate that I pointed to predates the general acceptance of the standardization of the modern definition of the reals. Now standard definitions literally makes no sense within constructivism. You talk about constructing familiar mathematics, but are using non-constructions that depend on questionable and questioned notions of absolute truth. What I described is as close to standard mathematics as you can come within a constructivist framework. The tradition of calling such constructions "the real numbers" may be new to you, but is actually over a century old.