fromComplex_toComplex
The theorem shows that transporting a recovered complex number to Mathlib's complex line and back recovers the original exactly. Researchers establishing carrier equivalences between logic-derived structures and standard mathematics would cite it when building the complex equivalence. The proof is a direct case split on the pair constructor followed by simplification using the real round-trip lemma.
claimFor any $z$ in the recovered complex carrier, fromComplex(toComplex($z$)) = $z$, where toComplex applies the real transport to each component and fromComplex applies the inverse real transport.
background
LogicComplex is the structure pairing two recovered real numbers (LogicReal) to form a complex carrier. The function toComplex maps such a pair to a Mathlib ℂ by applying toReal to the real and imaginary parts. The function fromComplex maps a Mathlib ℂ back by applying fromReal to its real and imaginary parts. The module sets up these carriers to obtain equivalence with Mathlib ℂ without redeveloping complex analysis.
proof idea
The term proof cases on the LogicComplex constructor mk re im, then invokes simp with the definitions of toComplex and fromComplex together with the upstream real round-trip theorem fromReal_toReal.
why it matters in Recognition Science
This result supplies the left inverse for the equivalence equivComplex : LogicComplex ≃ ℂ and is invoked in logicComplex_recovered_from_mathlib to confirm exact recovery of the carrier. It completes the foundational transport for complex numbers over the recovered reals, allowing later modules to invoke Mathlib analytic tools via the equivalence.
scope and limits
- Does not prove any analytic properties such as holomorphy or differentiability.
- Does not address contour integration or residue theorems.
- Applies only at the carrier level; does not define or verify arithmetic operations beyond the transport maps.
Lean usage
example (z : LogicComplex) : fromComplex (toComplex z) = z := fromComplex_toComplex zformal statement (Lean)
52@[simp] theorem fromComplex_toComplex (z : LogicComplex) :
53 fromComplex (toComplex z) = z := by
proof body
Term-mode proof.
54 cases z with
55 | mk re im =>
56 simp [toComplex, fromComplex, fromReal_toReal]
57
58/-- Carrier equivalence between recovered complex numbers and Mathlib `ℂ`. -/