toComplex_sub
plain-language theorem explainer
The transport map from recovered complex numbers to Mathlib complexes preserves subtraction. Researchers verifying ring homomorphisms between logic-derived carriers and standard analysis cite this when building the equivalence. It follows from a one-line simp wrapper that unfolds the subtraction definitions on both sides.
Claim. Let $z, w$ be recovered complex numbers. Then the transport satisfies $toComplex(z - w) = toComplex(z) - toComplex(w)$.
background
LogicComplex is the structure of pairs of recovered reals, with components re and im. The transport toComplex sends such a pair to the Mathlib complex whose real and imaginary parts are obtained by applying toReal to each component. Subtraction on LogicComplex uses the componentwise operation inherited from the recovered reals, while Mathlib subtraction is the standard one on ℂ.
proof idea
One-line wrapper that applies simp to HSub.hSub and Sub.sub, reducing both sides directly to componentwise subtraction on the real and imaginary parts via the definition of toComplex.
why it matters
This result verifies that the transport respects the additive structure, supporting the carrier-level equivalence with Mathlib ℂ stated in the module. It belongs to the foundation layer that recovers the reals and complexes before analytic or physical applications, consistent with the overall construction of LogicComplex as pairs over recovered reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.