fromComplex
plain-language theorem explainer
The declaration supplies the embedding from Mathlib's complex numbers into the recovered LogicComplex carrier by transporting each component through the real-line recovery map. Analysts working with the completed Riemann zeta function or other meromorphic objects in the Recognition Science setting cite this map when they need to move data between the two complex structures. The definition proceeds by direct record construction, applying the fromReal transport separately to the real and imaginary parts of the input.
Claim. The map $f : {ℂ} → LogicComplex$ sends a complex number $z$ to the pair $(fromReal(z.re), fromReal(z.im))$, where LogicComplex is the structure whose fields are recovered reals and fromReal embeds a standard real into the recovered real line.
background
The ComplexFromLogic module constructs complex numbers as pairs of recovered reals rather than redeveloping full complex analysis. LogicComplex is the structure with fields re and im of type LogicReal, the recovered real line obtained via the comparison equivalence from RealsFromLogic. The upstream fromReal function transports a Mathlib real $x$ by fromReal $x := ⟨CompareReals.compareEquiv.symm x⟩. This carrier setup lets later modules state explicitly when holomorphy or contour integration occurs in standard Mathlib $ℂ$ via the equivalence.
proof idea
The definition is a direct record constructor that applies the fromReal embedding to the real and imaginary parts of the input complex number $z$. No tactics or lemmas are invoked beyond the structure definition of LogicComplex and the fromReal transport.
why it matters
This embedding completes the carrier-level equivalence between LogicComplex and Mathlib $ℂ$, which is used to define equivComplex and to prove the round-trip identities fromComplex_toComplex and toComplex_fromComplex. It supports downstream results such as logicCompletedRiemannZeta_fromComplex in LogicComplexCompat, allowing the completed Riemann zeta function to be evaluated on recovered complexes while agreeing with the standard definition. In the Recognition framework this supplies the complex numbers needed for analytic continuations without rebuilding the entire theory from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.