toComplex_ofLogicRat
plain-language theorem explainer
Embedding a recovered rational into the logic complex via the real line and transporting the result recovers the standard embedding of its rational value into the complex numbers. Researchers verifying carrier-level equivalence between recovered structures and classical mathematics would cite this for consistency in the foundational recovery. The proof reduces via definition unfolding and a prior real-embedding theorem, then simplifies the resulting numerical equality.
Claim. Let $q$ be a recovered rational. The complex transport of the logic embedding of $q$ equals the standard complex number obtained by casting the rational value of $q$ into $ℂ$.
background
The module defines LogicComplex as pairs of recovered reals and supplies a transport map toComplex that extracts the real and imaginary parts via toReal to obtain a Mathlib ℂ. The embedding ofLogicRat first maps the recovered rational into a recovered real, then treats it as a purely real complex number. The module documentation states the local goal: construct the carrier LogicComplex as pairs of recovered reals and prove the carrier-level equivalence with Mathlib's ℂ for later analytic use.
proof idea
The tactic proof rewrites with the definition of ofLogicRat, applies the theorem toComplex_ofLogicReal to replace the complex transport by the real transport, invokes toReal_ofLogicRat to obtain the rational value, and finishes with norm_num to discharge the numerical equality.
why it matters
The result closes the rational case in the embedding chain that recovers standard complex numbers from the logic foundation. It directly supports the module's stated purpose of enabling later analytic modules to work in Mathlib ℂ via the established equivalence. No downstream uses are recorded, but the declaration completes one link in the carrier transport for rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.