module module high

`IndisputableMonolith.Foundation.RealsFromLogic`

The RealsFromLogic module constructs the recovered real line LogicReal as the Cauchy completion of the recovered rationals. It supplies the carrier, field operations, and the equivalence equivReal to Mathlib's ℝ. Modules building complex numbers and transporting transcendentals cite this layer to move analytic statements across the tower. The construction defines Cauchy sequences over the transported uniform structure on ℚ and quotients by the standard equivalence.

claimLet $L$ be the recovered rationals. The recovered reals are the quotient of Cauchy sequences in $L$ (Cauchy condition evaluated after transport to the standard uniform structure on $ℚ$) by the usual equivalence. The maps toReal and fromReal establish the equivalence $L_ℝ ≃ ℝ$.

background

This module follows RationalsFromLogic in the foundation layer and supplies the next step in the recovered number tower. It introduces CauchySeqLogicRat as a recovered-rational Cauchy sequence whose predicate is measured after transport to Mathlib's ℚ, marking the entry of the rational layer into the Cauchy completion. The module defines the carrier LogicReal, the embedding ofLogicRat, the round-trip maps toReal_fromReal and fromReal_toReal, and the equivalence equivReal.

proof idea

This is a definition module, no proofs. It defines the Cauchy sequence type, the quotient carrier LogicReal, the field operations, and the equivalence maps toReal and fromReal by direct transport of the standard real construction through the logic-to-rational map.

why it matters in Recognition Science

The module completes the rational-to-real step in the tower LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex. It is imported by ComplexFromLogic to form pairs of recovered reals and by LogicRealTranscendentals to transport transcendental functions through equivReal. RecoveredTowerAxiomAudit pulls it in to audit the full tower for axiom dependencies, supplying the real layer needed for later analytic work in the Recognition framework.

scope and limits

Does not construct reals independently of Mathlib's ℝ.
Does not develop differentiation, integration, or measure theory on LogicReal.
Does not address non-standard models or hyperreals.
Does not link directly to the J-function, phi-ladder, or forcing chain.

used by (3)

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

IndisputableMonolith.Foundation.ComplexFromLogic module_import
IndisputableMonolith.Foundation.LogicRealTranscendentals module_import
IndisputableMonolith.Foundation.RecoveredTowerAxiomAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.RationalsFromLogic module_import

declarations in this module (35)

structure CauchySeqLogicRat L46
structure LogicReal L66
def toReal L72
def fromReal L76
theorem toReal_fromReal L79
theorem fromReal_toReal L82
def equivReal L87
theorem eq_iff_toReal_eq L95
def ofRatCore L106
def ofLogicRat L110
theorem toReal_ofRatCore L113
theorem toReal_ofLogicRat L120
theorem toReal_zero L136
theorem toReal_one L137
theorem toReal_add L138
theorem toReal_neg L140
theorem toReal_sub L142
theorem toReal_mul L144
theorem toReal_inv L146
theorem toReal_div L148
theorem le_iff_toReal_le L151
theorem lt_iff_toReal_lt L152
theorem add_assoc' L154
theorem add_comm' L159
theorem zero_add' L164
theorem add_zero' L168
theorem add_left_neg' L172
theorem mul_assoc' L176
theorem mul_comm' L181
theorem one_mul' L186
theorem mul_one' L190
theorem mul_add' L194
theorem add_mul' L199
theorem bourbaki_complete L208
theorem logicReal_recovered_from_completion L213