toComplex_inv
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the transport is a ring homomorphism.
- Does not address continuity or holomorphy of the map.
- Does not apply when the complex number is zero.
formal statement (Lean)
108@[simp] theorem toComplex_inv (z : LogicComplex) :
109 toComplex z⁻¹ = (toComplex z)⁻¹ := by
proof body
One-line wrapper that applies simp.
110 simp [Inv.inv]
111