toComplex_re_eq
plain-language theorem explainer
The real part of a recovered complex number after transport to Mathlib's complex line equals the transport of its real component to Mathlib's reals. Analysts embedding recovered inputs into standard complex analysis for zeta-function work would cite this result. The proof is a one-line reflexivity that follows immediately from the definition of the transport map.
Claim. Let $s$ be a recovered complex number. Then the real part of its image under the transport map to Mathlib's complex numbers equals the image of its real part under the transport map to Mathlib's reals.
background
LogicComplex is the structure with real and imaginary parts each of type LogicReal. The transport map toComplex sends such an $s$ to the Mathlib complex whose components are obtained by applying toReal to $s$.re and $s$.im. LogicReal wraps the Bourbaki completion of the recovered rationals, and its toReal extracts the corresponding Mathlib real via the canonical equivalence compareEquiv.
proof idea
The proof is the term rfl. It succeeds because toComplex is defined by pairing the results of toReal on the real and imaginary parts, so the real-part projection after transport is definitionally identical to the transport of the real part.
why it matters
This theorem supplies the real-part compatibility needed for the module's decision to reuse Mathlib's complex substrate rather than rebuild analytic tools. It directly supports sibling declarations such as logicRiemannZeta_fromComplex that apply standard complex analysis to recovered inputs. The result sits inside the foundation layer that prepares recovered structures for the Euler-product and completed-zeta statements appearing later in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.