logicComplex_recovered_from_mathlib
plain-language theorem explainer
The theorem establishes that the custom complex numbers built as pairs of recovered reals are in exact bijection with Mathlib's standard complex numbers through the transport maps toComplex and fromComplex. Researchers formalizing the Recognition Science framework would cite this result when invoking Mathlib's complex analysis tools on the recovered carrier. The proof is a direct term that pairs the two already-proved round-trip identities for the real and imaginary components.
Claim. The transport maps between the recovered complex numbers (pairs of recovered reals) and the standard complex numbers satisfy: for every recovered complex $z$, fromComplex(toComplex $z$) = $z$, and for every standard complex $w$, toComplex(fromComplex $w$) = $w$.
background
LogicComplex is the structure whose elements are pairs of LogicReal values, one for the real part and one for the imaginary part. The map toComplex sends such a pair to a Mathlib complex number by applying toReal to each component, while fromComplex reverses the process by applying fromReal to the real and imaginary parts of a standard complex number. This module constructs the complex carrier over the recovered reals and proves its equivalence to Mathlib's ℂ so that later analytic work can use standard complex tools via the isomorphism. The upstream theorems fromComplex_toComplex and toComplex_fromComplex already supply the separate round-trip identities on the real and imaginary components.
proof idea
The proof is a term-mode construction that returns the ordered pair consisting of the theorem fromComplex_toComplex and the theorem toComplex_fromComplex.
why it matters
This result completes the carrier-level recovery of the complex numbers, allowing downstream modules to treat Mathlib ℂ as interchangeable with the Recognition Science version built from the recovered reals. It supports direct use of standard complex analysis inside the framework that begins from the forcing chain and the real recovery. No open questions remain at this level; the equivalence is fully closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.