toComplex_one
plain-language theorem explainer
The theorem shows that the transport map from recovered complex numbers to Mathlib's complex line sends the multiplicative unit to the standard unit. Any development relying on the equivalence between logic-derived complexes and standard ℂ cites this when simplifying unit expressions. The proof is a direct one-line application of the round-trip identity for the transport.
Claim. Let $L$ be the structure of complex numbers formed as pairs of recovered reals, and let $t: L → ℂ$ be the map that applies the recovered-real transport to each component. Then $t(1) = 1$.
background
The module recovers complex numbers over the logic-derived real line by defining LogicComplex as pairs of LogicReal values (real and imaginary parts). The transport map toComplex sends such a pair to the corresponding element of Mathlib's ℂ by applying the real transport componentwise. This construction supplies only the carrier and the equivalence with standard ℂ; no analytic machinery is redeveloped here.
proof idea
The proof is a one-line wrapper that applies the round-trip theorem toComplex_fromComplex at the complex number 1.
why it matters
The result supplies the first constant identity needed for arithmetic in the transported complex line, ensuring that the unit behaves correctly under the equivalence. It closes a basic case in the foundation layer that later modules rely on when invoking Mathlib's complex analysis through the stated carrier equivalence. No open questions are touched; the declaration is a direct consequence of the round-trip property already established for the transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.