Foundation Complex From Logic Logic Complex

The recovered complex plane

A complex number is built from two real numbers, one called the real part and one the imaginary part, usually written a + bi where i² = -1. The framework's recognition program, which derives structure from a discrete record of events, recovers the real number line from its own axioms. The declaration LogicComplex constructs complex numbers as ordered pairs of these recovered reals, and then proves that this construction is exactly the standard complex numbers, no more and no less.

The proof is a transport: the framework defines a map from its own complex numbers to the standard ones, and an inverse map back. The two maps are shown to cancel each other perfectly, so every recovered complex number corresponds to exactly one standard complex number and vice versa. The file proves this equivalence at the level of the carrier set, meaning the underlying collection of objects, and also shows that the usual algebraic operations, addition, subtraction, multiplication, division, zero, and one, all agree under this correspondence.

In Recognition Science, this matters because it shows the framework's internal language has not drifted from ordinary mathematics. When later modules want to do complex analysis, they can state that they are working in the standard complex plane via this equivalence, without redeveloping the whole theory. The declaration is a bridge, not a new kind of complex number.

What LogicComplex does not claim is substantial. It does not develop complex analysis, holomorphic functions, or contour integration; those are left to later modules. It does not assert that the recovered reals are the only way to build complex numbers, nor that complex numbers themselves are forced by the recognition axioms. The equivalence is a carrier-level result, so it does not yet transport any analytic structure such as continuity or differentiability. The framework proves the sets and algebra match; the analysis remains future work.

/-- Carrier equivalence between recovered complex numbers and Mathlib `ℂ`. -/
def equivComplex : LogicComplex ≃ ℂ where
  toFun := toComplex
  invFun := fromComplex
  left_inv := fromComplex_toComplex
  right_inv := toComplex_fromComplex

/-- 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⟩

@[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]

/-- Transport a recovered complex number to Mathlib's complex line. -/
def toComplex (z : LogicComplex) : ℂ :=
  ⟨toReal z.re, toReal z.im⟩

/-- Transport a Mathlib complex number to the recovered complex line. -/
def fromComplex (z : ℂ) : LogicComplex where
  re := fromReal z.re
  im := fromReal z.im

What this page does not claim

LogicComplex does not develop complex analysis, holomorphic functions, or contour integration. LogicComplex does not assert that complex numbers are forced by the recognition axioms. LogicComplex does not transport analytic structure such as continuity or differentiability.

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: