toComplex_zero
plain-language theorem explainer
The transport from recovered complex numbers to Mathlib's complex line sends the zero element to zero. Researchers establishing the carrier equivalence between logic-derived structures and standard analysis cite this when simplifying expressions involving the additive identity. The proof is a direct one-line application of the round-trip identity for the complex transport.
Claim. Let $phi$ be the map sending a pair of recovered reals to the corresponding element of $mathbb{C}$. Then $phi(0) = 0$.
background
The module builds complex numbers over the recovered real line. LogicComplex is the structure whose elements are pairs of LogicReal values, one for the real part and one for the imaginary part. The transport map toComplex applies the real-line transport toReal to each component, yielding an element of Mathlib's $mathbb{C}$./nThe key upstream result is the round-trip theorem stating that toComplex composed with fromComplex recovers the original element of $mathbb{C}$ exactly, proved by applying Complex.ext and simplifying the component maps.
proof idea
One-line wrapper that applies the round-trip theorem toComplex_fromComplex at the zero element of LogicComplex.
why it matters
This supplies the zero case of the carrier equivalence between LogicComplex and $mathbb{C}$. The module states that later analytic work can invoke the equivalence when performing holomorphy or contour integration inside Mathlib $mathbb{C}$. It completes a basic simplification rule needed for any downstream algebraic manipulation that begins from the recovered zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.