toComplex_inv
plain-language theorem explainer
The transport map from recovered complex numbers to Mathlib's complex line commutes with multiplicative inversion. Researchers verifying algebraic compatibility between the Recognition Science carrier and standard complex analysis would cite this result when confirming that field operations survive the equivalence. The proof is a one-line simp wrapper that unfolds the inverse definition on the recovered carrier.
Claim. Let $z$ be a recovered complex number with real and imaginary parts in the recovered reals. Let $ι$ be the transport sending $z$ to the corresponding element of the standard complex line $ℂ$. Then $ι(z^{-1}) = ι(z)^{-1}$.
background
The module builds complex numbers over the recovered real line recovered earlier in the foundation. LogicComplex is the carrier structure consisting of ordered pairs of recovered reals, one component for the real part and one for the imaginary part. The transport map sends each such pair to the corresponding element of Mathlib's $ℂ$ by applying the real-line transport to both components.
proof idea
One-line wrapper that applies simp to the definition of the inverse operation.
why it matters
The result closes the algebraic compatibility of the transport with the field inverse, supporting any later analytic work that relies on the equivalence to Mathlib's $ℂ$. It belongs to the foundation layer that recovers standard structures from the logic-derived reals before analytic modules are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.