Foundation Complex From Logic From Complex

Recovered complex numbers

Complex numbers are usually introduced as pairs of real numbers (a, b) with a rule for multiplication. The declaration fromComplex in the Recognition Science framework is a translation map: it takes an ordinary complex number and writes it as a pair of recovered reals. The framework first constructs its own real numbers, called recovered reals, from its basic logic. Then it builds complex numbers as pairs of those recovered reals, and fromComplex is the function that carries a standard complex number into that recovered form.

The framework proves that this translation is exact. Two theorems, toComplex_fromComplex and fromComplex_toComplex, show that going from the standard complex numbers to the recovered ones and back again returns the original number. A further theorem, logicComplex_recovered_from_mathlib, states both directions in one statement. The framework also proves that the recovered complex numbers preserve the usual arithmetic: addition, multiplication, and division all match the standard operations. This means that any calculation done in the recovered complex numbers gives the same result as the same calculation in the ordinary complex numbers.

In Recognition Science, this is a carrier-level equivalence. It shows that the framework's complex numbers are not a new kind of number; they are the same complex numbers, just built from the framework's own real line. The framework does not redevelop complex analysis in this file. It does not prove the fundamental theorem of algebra, Cauchy's theorem, or any other theorem about holomorphic functions. Later files can use the equivalence to state when they are working with the standard complex numbers, but this file only establishes the translation.

The practical consequence is that the framework can use all of the usual complex-number machinery without inventing a parallel universe of mathematics. When a later framework result needs complex analysis, it can point to this equivalence and say: the complex numbers here are the familiar ones. The framework's complex numbers are not a rival structure; they are the standard structure, reached through a different path.

@[simp] theorem toComplex_fromComplex (z : ℂ) :
    toComplex (fromComplex z) = z := by
  apply Complex.ext <;> simp [toComplex, fromComplex, toReal_fromReal]

@[simp] theorem fromComplex_toComplex (z : LogicComplex) :
    fromComplex (toComplex z) = z := by
  cases z with
  | mk re im =>
    simp [toComplex, fromComplex, fromReal_toReal]

@[simp] theorem toComplex_add (z w : LogicComplex) :
    toComplex (z + w) = toComplex z + toComplex w := by
  simp [HAdd.hAdd, Add.add]

@[simp] theorem toComplex_mul (z w : LogicComplex) :
    toComplex (z * w) = toComplex z * toComplex w := by
  simp [HMul.hMul, Mul.mul]

@[simp] theorem toComplex_div (z w : LogicComplex) :
    toComplex (z / w) = toComplex z / toComplex w := by
  simp [HDiv.hDiv, Div.div]

/-- The recovered complex carrier is exactly Mathlib `ℂ`, by transport. -/
theorem logicComplex_recovered_from_mathlib :
    (∀ z : LogicComplex, fromComplex (toComplex z) = z) ∧
    (∀ z : ℂ, toComplex (fromComplex z) = z) :=
  ⟨fromComplex_toComplex, toComplex_fromComplex⟩

What this page does not claim

This file does not prove any theorem of complex analysis, such as Cauchy's integral formula or the fundamental theorem of algebra. The equivalence does not show that the framework's complex numbers are different from the standard ones; it shows they are the same.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/ComplexFromLogic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: