pith. machine review for the scientific record. sign in
structure definition def or abbrev high

LogicComplex

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  27structure LogicComplex where
  28  re : LogicReal
  29  im : LogicReal
  30
  31namespace LogicComplex
  32
  33/-- Transport a recovered complex number to Mathlib's complex line. -/

used by (27)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.