LogicComplex
plain-language theorem explainer
LogicComplex defines the carrier for complex numbers as ordered pairs of recovered real numbers. Foundation researchers cite it when establishing the equivalence between logic-derived complexes and Mathlib's ℂ. The structure declaration directly pairs two LogicReal fields with no additional axioms or proofs required.
Claim. The structure consists of pairs $(re, im)$ where both $re$ and $im$ belong to the recovered real line obtained as the Cauchy completion of the logic rationals.
background
LogicReal is the Cauchy completion of the recovered rationals, realized through the canonical completion of ℚ and the equivalence with the logic rationals. The wrapper prevents global instance pollution on the completion while reusing Mathlib's completed real line. This module constructs complex numbers over the recovered real line as pairs, without redeveloping complex analysis. The carrier is shown equivalent to Mathlib's ℂ via transport maps.
proof idea
The declaration is a bare structure definition with no proof body or obligations. It directly introduces the two fields re and im of type LogicReal.
why it matters
LogicComplex serves as the foundational carrier for complex numbers, enabling equivalence theorems such as equivComplex and logicComplex_recovered_from_mathlib. It extends the real line construction to complexes and supports transport to Mathlib's ℂ. This fills the complex carrier step after the real recovery, allowing downstream modules to invoke standard complex operations via the equivalence without local analytic development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.