toComplex_inv
plain-language theorem explainer
The transport from LogicComplex to Mathlib ℂ commutes with multiplicative inversion. Researchers verifying algebraic compatibility of the recovered-complex carrier with standard ℂ would cite this result. The proof is a one-line simp wrapper on the definition of inversion.
Claim. Let $z$ be a complex number formed as a pair of recovered reals. The transport of its multiplicative inverse equals the multiplicative inverse of its transport: toComplex$(z^{-1}) = ($toComplex $z)^{-1}$.
background
LogicComplex is the carrier structure whose elements are pairs (re, im) of LogicReal. The map toComplex sends such a pair to the Mathlib complex whose real and imaginary parts are the images under toReal. The module establishes only the carrier-level equivalence with ℂ and defers all analytic development. Upstream, the inverse operation on LogicComplex is supplied by the field structure on recovered reals; the referenced inv lemmas from Ribbons and RecogSpec.Core supply the corresponding preservation statements used by the simplifier.
proof idea
One-line wrapper that applies simp on Inv.inv.
why it matters
The result closes the inverse case for the transport map, completing the algebraic compatibility needed before the equivalence theorems (equivComplex and fromComplex_toComplex) can be stated. It sits inside the foundation layer that recovers ℂ from the logic primitives, prior to any use of complex numbers in the phi-ladder or the eight-tick octave. No open questions are attached to this specific lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.