fromComplex_toComplex
plain-language theorem explainer
The left inverse property for the transport maps between recovered complex numbers and Mathlib ℂ. Researchers building carrier equivalences in the recovered number systems cite this to confirm bijectivity at the set level. The proof proceeds by case analysis on the pair constructor of the recovered complex followed by simplification that reduces to the real-line inverse.
Claim. For every complex number $z$ formed as a pair of recovered reals, the composition of the forward transport into standard complexes followed by the backward transport recovers $z$ exactly.
background
The module constructs complex numbers over recovered reals via the structure consisting of a real part and imaginary part, each drawn from the recovered reals. The forward and backward transport maps are defined by applying the corresponding real-line maps componentwise. This theorem depends on the upstream result that the real round-trip map is the identity, which is invoked during simplification. The module's local setting is to supply carrier equivalence with Mathlib ℂ for later analytic modules without redeveloping complex analysis.
proof idea
The proof performs case analysis on the mk constructor of the recovered complex structure. Simplification then unfolds the transport definitions and reduces both components to the real-line inverse theorem, which is discharged automatically.
why it matters
This supplies the left inverse for the equivalence that equates the recovered complex carrier with Mathlib ℂ. It is invoked directly in the definition of that equivalence and in the theorem asserting exact recovery of the carrier. The result completes the foundation-level bijection between recovered and standard complexes, enabling transport of analytic statements while remaining within the pattern of recovering standard structures from logic primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.