toComplex_zero
The transport from recovered complex numbers to Mathlib's ℂ sends the zero element of the recovered carrier to the zero of ℂ. Researchers recovering the complex line from the logic foundation cite this when simplifying identities that involve the additive identity. The proof is a one-line wrapper applying the round-trip theorem at zero.
claimLet $toComplex : LogicComplex → ℂ$ send a pair of recovered reals to the corresponding element of Mathlib's complex numbers. Then $toComplex(0) = 0$.
background
LogicComplex is the structure of pairs of LogicReal elements that serves as the carrier for complex numbers recovered from the logic foundation. The function toComplex transports such a pair to Mathlib's ℂ by applying the real transport toReal to the real and imaginary parts separately. The module establishes the carrier-level equivalence with standard complex numbers without redeveloping analytic theory.
proof idea
The proof is a one-line wrapper that applies the round-trip theorem toComplex_fromComplex instantiated at the zero complex number.
why it matters in Recognition Science
This simp lemma records the compatibility of the zero element under the equivalence between the recovered and standard complex lines. It supplies a basic case needed for any later module that routes analytic statements through the Mathlib ℂ equivalence. The result closes the zero instance in the transport construction that begins from the recovered reals.
scope and limits
- Does not establish preservation of multiplication or addition beyond the zero case.
- Does not address holomorphy or contour integration on the recovered carrier.
- Does not supply any metric or topological properties of the transport map.
formal statement (Lean)
86@[simp] theorem toComplex_zero : toComplex (0 : LogicComplex) = 0 := by
proof body
One-line wrapper that applies exact.
87 exact toComplex_fromComplex 0
88