equivComplex
plain-language theorem explainer
EquivComplex supplies the canonical bijection between LogicComplex, the complex numbers built as pairs of recovered reals, and Mathlib's standard ℂ. Analysts in the Recognition framework cite it when transporting holomorphic objects or zeta functions between the recovered carrier and the classical one. The definition is a one-line wrapper that installs toComplex as the forward map, fromComplex as the inverse, and the two round-trip lemmas to establish the equivalence.
Claim. The structure of pairs of recovered reals is canonically equivalent to the complex numbers ℂ via the map sending each pair (re, im) to the complex number whose real part is the image of re under the recovered-to-standard real map and whose imaginary part is the image of im under the same map.
background
LogicComplex is the structure whose fields are two elements of LogicReal, the reals recovered from the logic layer. The transport maps toComplex and fromComplex send such a pair to the Mathlib complex number with components toReal(re) and toReal(im), and conversely embed a standard complex number by applying fromReal to each component. The module constructs only the carrier and its equivalence with ℂ; it deliberately avoids redeveloping complex analysis so that later modules can invoke holomorphy or contour integration directly in the standard ℂ via this equivalence.
proof idea
This is a one-line wrapper definition that sets the toFun field to toComplex, the invFun field to fromComplex, and supplies the left inverse fromComplex_toComplex together with the right inverse toComplex_fromComplex.
why it matters
The equivalence is required by logicComplexAnalyticSubstrateCert to certify the analytic substrate for Phase 2. It lets subsequent modules state that analytic operations occur in Mathlib ℂ without rebuilding the theory over LogicComplex, thereby closing the carrier construction in the foundation layer before any holomorphic work begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.