toComplex_neg
plain-language theorem explainer
The theorem shows that negation on LogicComplex commutes with the transport map to Mathlib's complex plane. Researchers verifying that recovered arithmetic matches standard operations under the embedding would cite it when checking group laws. The proof is a one-line simp wrapper that unfolds the negation definition.
Claim. Let $z$ be a complex number with real and imaginary parts from the recovered reals. Then the transport of its negation equals the negation of its transport: $toComplex(-z) = -toComplex(z)$.
background
The module builds complex numbers over recovered reals. LogicComplex is the structure with fields re and im of type LogicReal. The map toComplex sends such a pair to Mathlib's ℂ by applying toReal to each component. Module documentation states the goal: construct the carrier as pairs of recovered reals and prove carrier-level equivalence with Mathlib's ℂ. Upstream negation definitions appear on LogicInt, LogicRat, and intervals, which lift to this level.
proof idea
The proof is a one-line wrapper that applies simp [Neg.neg]. This unfolds the negation instance on LogicComplex and matches it directly to negation on ℂ.
why it matters
The result confirms that the embedding preserves the additive inverse, supporting the full equivalence equivComplex and related lemmas such as toComplex_add in the same module. It closes a basic compatibility check in the recovery of standard complex numbers from the logic primitives, consistent with the forcing chain steps that recover arithmetic before analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.