module module high

`IndisputableMonolith.Foundation.ComplexFromLogic`

Module constructs complex numbers over reals recovered from the logic rational layer via Bourbaki completion. Researchers tracing the full recovered number tower cite it to reach the complex stage before analytic work. The module supplies definitions and transport maps with no internal proofs.

claimComplex numbers constructed as ordered pairs of recovered reals, with componentwise addition and the multiplication rule $(a,b)(c,d)=(ac-bd,ad+bc)$.

background

The module sits directly above RealsFromLogic, whose doc-comment states: 'Recovery of the real numbers from the Law-of-Logic rational layer. The construction uses Mathlib's Bourbaki completion of ℚ as the completion engine, while the input rationals are the recovered rationals LogicRat.' It therefore inherits the logic-derived reals and extends the tower to complexes. Sibling declarations introduce the type LogicComplex together with the maps toComplex and fromComplex that realize the standard pair construction.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the LogicComplex stage that feeds LogicComplexCompat, whose doc-comment notes the decision to retain Mathlib ℂ as the analytic substrate, and RecoveredTowerAxiomAudit, whose doc-comment describes the audit surface for the tower LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex. It therefore closes the algebraic part of the recovered tower before any analytic or physical application.

scope and limits

Does not redefine holomorphy or contour integration on the recovered complex.
Does not prove any completeness or field properties beyond the pair construction.
Does not claim numerical identity with Mathlib ℂ without the downstream compatibility layer.
Does not introduce physical constants or mass formulas.

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