toComplex_fromComplex
The round-trip transport from a Mathlib complex through the recovered carrier returns the input unchanged. Analysts working with logic-derived reals cite this to justify identifying the two carriers for later analytic work. The proof is a one-line wrapper that applies complex extensionality and simplifies using the real round-trip theorem.
claimFor any $z : ℂ$, the composition of the transport from the recovered complex carrier back to Mathlib complexes with the forward transport satisfies $toComplex(fromComplex(z)) = z$.
background
The module defines LogicComplex as pairs of recovered reals and constructs transport maps to and from Mathlib's ℂ. The local setting is carrier-level equivalence only; analytic development is deferred to Mathlib via this bridge. Upstream, fromComplex packs a Mathlib complex into the recovered carrier using fromReal on each component, toComplex extracts using toReal, and toReal_fromReal establishes the real-line round-trip.
proof idea
One-line wrapper that applies Complex.ext to reduce to real and imaginary parts, then simp unfolds toComplex, fromComplex, and toReal_fromReal.
why it matters in Recognition Science
This supplies the right-inverse direction for the carrier equivalence. It feeds equivComplex (the explicit bijection) and logicComplex_recovered_from_mathlib (the joint recovery statement). The result closes the foundation step that lets later modules invoke standard complex analysis on the logic-derived reals without redeveloping contours or holomorphy.
scope and limits
- Does not establish holomorphy or contour integration.
- Does not prove algebraic closure or field axioms beyond the carrier map.
- Applies only to the specific transport pair defined here.
- Does not address convergence or limits on the recovered line.
Lean usage
example : toComplex (fromComplex (1 : ℂ)) = 1 := by exact toComplex_fromComplex 1formal statement (Lean)
48@[simp] theorem toComplex_fromComplex (z : ℂ) :
49 toComplex (fromComplex z) = z := by
proof body
One-line wrapper that applies apply.
50 apply Complex.ext <;> simp [toComplex, fromComplex, toReal_fromReal]
51