toComplex
plain-language theorem explainer
The map sends each LogicComplex, a pair of recovered reals, to Mathlib's ℂ by embedding its real and imaginary parts separately. Researchers establishing carrier equivalence between logic-derived numbers and classical analysis cite this transport when moving statements between the two settings. The definition is realized as a direct pair constructor that applies the real embedding to each component.
Claim. For $z$ a complex number over recovered reals, $toComplex(z) = (toReal(z.re), toReal(z.im))$, where $toReal$ embeds a recovered real into Mathlib's real line.
background
LogicComplex is the structure whose fields are a pair of LogicReal values, one for the real part and one for the imaginary part. The upstream toReal from RealsFromLogic is the noncomputable embedding that sends a recovered real $x$ to the Mathlib real CompareReals.compareEquiv x.val. The module builds the complex carrier over these recovered reals and proves its set-level equivalence to Mathlib's ℂ, without redeveloping analytic machinery.
proof idea
One-line definition that applies toReal to the real and imaginary fields of the input LogicComplex and packages the resulting pair as a Mathlib complex number.
why it matters
This supplies the forward direction of the equivalence equivComplex : LogicComplex ≃ ℂ and is invoked in the recovery theorem logicComplex_recovered_from_mathlib as well as in the additivity and division compatibility lemmas. It completes the carrier construction begun in RealsFromLogic, allowing later modules to invoke classical complex analysis on the image under this map while remaining inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.