equivComplex
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish holomorphy or any other analytic property on LogicComplex.
- Does not define multiplication, addition, or other operations on LogicComplex beyond the carrier map.
- Does not address convergence, residues, or contour integration.
Lean usage
carrier_equiv := equivComplexformal statement (Lean)
59def equivComplex : LogicComplex ≃ ℂ where
60 toFun := toComplex
proof body
Definition body.
61 invFun := fromComplex
62 left_inv := fromComplex_toComplex
63 right_inv := toComplex_fromComplex
64
65/-- Equality transfer for recovered complex numbers. -/