toComplex_zero
plain-language theorem explainer
The transport map from recovered complex numbers (pairs of recovered reals) to Mathlib's ℂ sends the zero element to zero. Researchers using the recovered complex line in calculations would cite this simp lemma for simplification. The proof is a one-line wrapper applying the round-trip identity toComplex_fromComplex at zero.
Claim. Let $φ$ be the transport map sending a pair of recovered reals to the corresponding element of $ℂ$. Then $φ(0) = 0$.
background
The module constructs complex numbers over the recovered real line. LogicComplex is the structure whose real and imaginary parts are each a LogicReal. The function toComplex sends such an element to Mathlib's $ℂ$ by applying toReal to each component. The module establishes carrier-level equivalence with $ℂ$ without redeveloping analysis. The key upstream result is the round-trip theorem stating that toComplex (fromComplex z) equals z, proved by Complex.ext and simplification on the real and imaginary parts.
proof idea
One-line wrapper that applies toComplex_fromComplex directly at the zero element of $ℂ$.
why it matters
This simp theorem confirms that the zero element is preserved under transport, supporting algebraic calculations in the recovered complex line. It forms part of the equivalence between LogicComplex and $ℂ$ in the module. The result sits in the foundational layer that recovers reals and complexes from logic before introducing Recognition Science constants such as phi or the forcing chain steps T5-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.