module module high

`IndisputableMonolith.Foundation.ComplexFromLogic`

Module defines complex numbers over the reals recovered from logic rationals. Researchers tracing the Law-of-Logic number tower cite it to reach the top of the arithmetic hierarchy. It is a definition module that supplies the LogicComplex type and conversion maps without internal proofs.

claimLet $\mathbb{R}_L$ be the reals recovered from LogicRat via Bourbaki completion. Then LogicComplex is the field $\mathbb{R}_L[i]$ of pairs $(x,y)$ with $x,y\in\mathbb{R}_L$ and the usual addition and multiplication rules.

background

The module sits atop RealsFromLogic, whose doc states: "Recovery of the real numbers from the Law-of-Logic rational layer. The construction uses Mathlib's Bourbaki completion of $\mathbb{Q}$ as the completion engine, while the input rationals are the recovered rationals LogicRat from Foundation.RationalsFromLogic." It therefore inherits the recovered reals and extends them by the standard algebraic adjunction of $i$. Sibling declarations supply the concrete type LogicComplex together with the maps toComplex, fromComplex, and the round-trip theorems toComplex_fromComplex and fromComplex_toComplex.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the final layer of the recovered tower LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex. It is imported by LogicComplexCompat, whose doc notes the decision to retain Mathlib $\mathbb{C}$ as the analytic substrate, and by RecoveredTowerAxiomAudit, whose doc states the audit surface for the full tower so that #print axioms can be run on one target.

scope and limits

Does not redefine contour integration or holomorphy on the recovered complex.
Does not prove analytic identities; those remain in Mathlib via the compat layer.
Does not claim that LogicComplex satisfies every axiom of Mathlib's $\mathbb{C}$ without the transport theorems.
Does not close the tower audit; that is performed in the downstream audit module.

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