equivComplex
plain-language theorem explainer
The carrier equivalence identifies pairs of recovered reals with Mathlib complex numbers via componentwise transport. Analysts extending results to the recovered substrate cite it to move statements between carriers. It is assembled directly from the toComplex and fromComplex maps together with their roundtrip theorems as inverses.
Claim. The map sending a pair $(x,y)$ of recovered reals to the Mathlib complex number with real part toReal$(x)$ and imaginary part toReal$(y)$, together with its inverse sending $z$ to the pair of recovered reals obtained by fromReal, forms a bijection between the two carriers.
background
LogicComplex is the structure whose fields are a pair of LogicReal values; LogicReal is the recovered real line imported from RealsFromLogic. The forward transport toComplex applies toReal to each component, while fromComplex applies fromReal to the real and imaginary parts of a Mathlib complex. The module constructs only this carrier-level equivalence and leaves analytic operations in Mathlib ℂ.
proof idea
One-line wrapper that assembles the equivalence structure by setting toFun to toComplex, invFun to fromComplex, left_inv to fromComplex_toComplex, and right_inv to toComplex_fromComplex.
why it matters
This equivalence supplies the carrier_equiv field required by logicComplexAnalyticSubstrateCert, the analytic substrate certificate for Phase 2. It lets later modules transfer statements about the Riemann zeta function and related objects between the recovered substrate and standard complex analysis. The construction follows the Recognition pattern of recovering standard carriers before layering analytic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.