eq_iff_toComplex_eq
plain-language theorem explainer
Equality between two recovered complex numbers holds precisely when their images under the transport to standard complex numbers coincide. Researchers embedding logical constructions into classical analysis cite this when transferring equalities across representations. The proof is a short term-mode argument that splits the biconditional via constructor and reduces both directions with congruence plus the round-trip identity.
Claim. For elements $z, w$ of the structure of complex numbers built over recovered reals, $z = w$ if and only if the image of $z$ under the transport map to the standard complex numbers equals the image of $w$.
background
The module constructs the carrier type as pairs of recovered real numbers and establishes its equivalence with Mathlib's standard complex numbers. The transport maps send a pair to the standard complex number by applying the real transport to each component, and the reverse map reconstructs the pair from a standard complex number. A key upstream result states that applying the reverse map after the forward map recovers the original element exactly.
proof idea
The proof is a term-mode construction of the biconditional. Constructor splits the two directions. The forward direction follows at once from congruence with the forward transport map. The reverse applies congruence with the reverse transport map to the hypothesis, then rewrites both sides using the round-trip identity twice.
why it matters
This supplies the equality transfer required to define algebraic operations on the recovered carrier via transport to the standard complex numbers and back. It directly enables the subsequent instances for addition, multiplication, and other operations in the same module. Within the Recognition framework it ensures the recovered complex numbers match standard ones on equality, supporting the carrier-level equivalence needed for later analytic work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.