toComplex_ofLogicReal
plain-language theorem explainer
The theorem shows that embedding a recovered real into the recovered complex plane as a purely real element and then transporting the result to standard complexes yields exactly the standard complex whose real part is the transported real. Researchers verifying consistency between logic-derived number systems and classical analysis cite this when composing real and complex embeddings. The proof is a one-line wrapper applying complex extensionality followed by simplification on the embedding definitions.
Claim. For any recovered real number $x$, the transport to standard complexes of the embedding of $x$ as a purely real recovered complex equals the standard complex number whose real part is the transport of $x$ to standard reals.
background
The module builds complex numbers over the recovered real line by taking LogicComplex as ordered pairs of recovered reals. LogicReal is the Cauchy completion of recovered rationals, obtained via the canonical completion of the rationals together with the equivalence between recovered rationals and standard rationals. The embedding ofLogicReal sends a recovered real $x$ to the recovered complex with real part $x$ and imaginary part zero. The transport toComplex sends a recovered complex to the standard complex whose real and imaginary parts are the images of the components under the real transport map. This construction rests on the recovered reals from the RealsFromLogic module, where the real transport converts a recovered real to a standard real via the Bourbaki completion equivalence.
proof idea
The proof is a one-line wrapper that applies the complex extensionality lemma and then simplifies using the definitions of the real embedding and the complex transport map.
why it matters
This result is used by the parent theorem that extends the embedding to recovered rationals. It forms part of the carrier-level equivalence between recovered complexes and standard complexes, as described in the module documentation. Within the Recognition Science framework the step ensures that complex numbers constructed from logic align with classical analysis, allowing later analytic modules to invoke standard complex analysis via the transport without redevelopment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.