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

toComplex

show as:
view Lean formalization →

The map sends each LogicComplex, a pair of recovered reals, to Mathlib's ℂ by embedding its real and imaginary parts separately. Researchers establishing carrier equivalence between logic-derived numbers and classical analysis cite this transport when moving statements between the two settings. The definition is realized as a direct pair constructor that applies the real embedding to each component.

claimFor $z$ a complex number over recovered reals, $toComplex(z) = (toReal(z.re), toReal(z.im))$, where $toReal$ embeds a recovered real into Mathlib's real line.

background

LogicComplex is the structure whose fields are a pair of LogicReal values, one for the real part and one for the imaginary part. The upstream toReal from RealsFromLogic is the noncomputable embedding that sends a recovered real $x$ to the Mathlib real CompareReals.compareEquiv x.val. The module builds the complex carrier over these recovered reals and proves its set-level equivalence to Mathlib's ℂ, without redeveloping analytic machinery.

proof idea

One-line definition that applies toReal to the real and imaginary fields of the input LogicComplex and packages the resulting pair as a Mathlib complex number.

why it matters in Recognition Science

This supplies the forward direction of the equivalence equivComplex : LogicComplex ≃ ℂ and is invoked in the recovery theorem logicComplex_recovered_from_mathlib as well as in the additivity and division compatibility lemmas. It completes the carrier construction begun in RealsFromLogic, allowing later modules to invoke classical complex analysis on the image under this map while remaining inside the Recognition framework.

scope and limits

formal statement (Lean)

  34def toComplex (z : LogicComplex) : ℂ :=

proof body

Definition body.

  35  ⟨toReal z.re, toReal z.im⟩
  36
  37/-- Transport a Mathlib complex number to the recovered complex line. -/

used by (26)

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

depends on (3)

Lean names referenced from this declaration's body.