module module high

`IndisputableMonolith.Foundation.ComplexFromLogic`

The module constructs complex numbers over the reals recovered from Law-of-Logic rationals via Bourbaki completion. Researchers completing the number tower or bridging to Mathlib analytics cite it for the algebraic extension and transport maps. The structure follows the standard pair definition of complexes with componentwise addition and the usual multiplication rule.

claimComplex numbers are constructed as ordered pairs of recovered reals, equipped with componentwise addition and the multiplication rule $(a,b)(c,d)=(ac-bd,ad+bc)$, together with the canonical isomorphism to the standard complex field.

background

Upstream RealsFromLogic recovers the real numbers from the rational layer by applying Mathlib's Bourbaki completion to the recovered rationals. This module extends that recovery to the complex domain by the standard algebraic construction over those reals. The local setting is the Law-of-Logic number tower, which proceeds from naturals through integers and rationals to reals and now complexes.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the recovered complexes that feed LogicComplexCompat, which makes explicit the decision to retain Mathlib's analytic substrate rather than rebuild holomorphy. It also completes the audited tower LogicNat to LogicComplex in RecoveredTowerAxiomAudit, pinning the final recovery step for axiom inspection.

scope and limits

Does not redefine contour integration or holomorphy on the recovered complexes.
Does not alter the Bourbaki completion used for the underlying reals.
Does not include completeness or metric properties beyond the algebraic field structure.
Does not supply explicit embeddings of the recovered complexes into later physical models.

used by (2)

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

IndisputableMonolith.Foundation.LogicComplexCompat module_import
IndisputableMonolith.Foundation.RecoveredTowerAxiomAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.RealsFromLogic module_import

declarations in this module (22)

structure LogicComplex L27
def toComplex L34
def fromComplex L38
theorem toComplex_re L42
theorem toComplex_im L45
theorem toComplex_fromComplex L48
theorem fromComplex_toComplex L52
def equivComplex L59
theorem eq_iff_toComplex_eq L66
theorem toComplex_zero L86
theorem toComplex_one L89
theorem toComplex_add L92
theorem toComplex_neg L96
theorem toComplex_sub L100
theorem toComplex_mul L104
theorem toComplex_inv L108
theorem toComplex_div L112
def ofLogicReal L117
theorem toComplex_ofLogicReal L121
def ofLogicRat L127
theorem toComplex_ofLogicRat L130
theorem logicComplex_recovered_from_mathlib L136