toComplex_fromComplex
plain-language theorem explainer
The round-trip transport from a Mathlib complex through the recovered carrier returns the input unchanged. Analysts working with logic-derived reals cite this to justify identifying the two carriers for later analytic work. The proof is a one-line wrapper that applies complex extensionality and simplifies using the real round-trip theorem.
Claim. For any $z : ℂ$, the composition of the transport from the recovered complex carrier back to Mathlib complexes with the forward transport satisfies $toComplex(fromComplex(z)) = z$.
background
The module defines LogicComplex as pairs of recovered reals and constructs transport maps to and from Mathlib's ℂ. The local setting is carrier-level equivalence only; analytic development is deferred to Mathlib via this bridge. Upstream, fromComplex packs a Mathlib complex into the recovered carrier using fromReal on each component, toComplex extracts using toReal, and toReal_fromReal establishes the real-line round-trip.
proof idea
One-line wrapper that applies Complex.ext to reduce to real and imaginary parts, then simp unfolds toComplex, fromComplex, and toReal_fromReal.
why it matters
This supplies the right-inverse direction for the carrier equivalence. It feeds equivComplex (the explicit bijection) and logicComplex_recovered_from_mathlib (the joint recovery statement). The result closes the foundation step that lets later modules invoke standard complex analysis on the logic-derived reals without redeveloping contours or holomorphy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.