ofLogicReal
plain-language theorem explainer
This definition embeds a recovered real number into the recovered complex numbers by setting the imaginary part to zero. It is cited when lifting real constructions to the complex carrier in the Recognition foundation. The implementation is a direct structure constructor that populates the LogicComplex record with the supplied real part and zero imaginary part.
Claim. The embedding map sends a recovered real number $x$ to the complex number whose real part is $x$ and whose imaginary part is $0$.
background
The module ComplexFromLogic constructs complex numbers over the recovered real line as pairs of LogicReal values. LogicComplex is the structure with fields re and im, each of type LogicReal. LogicReal is the Cauchy completion of the recovered rationals, realized through the canonical completion of ℚ together with the equivalence LogicRat ≃ ℚ; the wrapper avoids global instance pollution on Completion ℚ while reusing Mathlib's completed reals.
proof idea
The definition is a one-line structure constructor that instantiates LogicComplex with re set to the input x and im set to zero. No lemmas or tactics are applied.
why it matters
This embedding is invoked by ofLogicRat to lift recovered rationals into complexes and by toComplex_ofLogicReal to establish the relation to Mathlib's ℂ. It contributes to the carrier-level equivalence between recovered complexes and standard ℂ, allowing later modules to reference Mathlib complex analysis explicitly via the equivalence. It supports the foundation's recovery of the complex line before analytic or physical constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.