LogicComplex
plain-language theorem explainer
LogicComplex supplies the carrier type for complex numbers constructed from the recovered real line. Foundation workers cite it when moving between the logic-derived numbers and Mathlib's ℂ for later analytic statements. The declaration is a plain structure with two fields and no proof obligations.
Claim. A recovered complex number is an ordered pair $(re, im)$ where both components lie in the recovered real line obtained as the Cauchy completion of the recovered rationals.
background
LogicReal is the structure whose single field is a Mathlib Bourbaki real, obtained by completing the recovered rationals via the equivalence LogicRat ≃ ℚ; the wrapper avoids polluting global instances on Completion ℚ. The module ComplexFromLogic constructs the complex carrier as pairs of such recovered reals and supplies transport maps to and from Mathlib ℂ without redeveloping complex analysis. The upstream result LogicReal states that the wrapper reuses Mathlib's completed real line while keeping the recovered construction isolated.
proof idea
The declaration is the structure definition itself; it introduces the carrier with real and imaginary parts of type LogicReal and requires no tactics or lemmas.
why it matters
LogicComplex is the immediate prerequisite for equivComplex (the carrier equivalence LogicComplex ≃ ℂ) and for logicComplex_recovered_from_mathlib (the theorem asserting that transport in both directions recovers the original element). It closes the foundation layer after RealsFromLogic and before any analytic modules that must state when they work in Mathlib ℂ. The construction sits inside the Recognition Science foundation chain that begins with recovered rationals and proceeds through reals to complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.