module module moderate

`IndisputableMonolith.Foundation.RealsFromLogic`

RealsFromLogic constructs the recovered real line as the Cauchy completion of the logic rationals. The Cauchy predicate is evaluated after transport to the standard uniform structure on rationals. Downstream modules that need a real line equivalent to Mathlib's reals cite this construction. The module supplies the carrier, equivalence maps, and basic transport lemmas.

claimLet $\mathbb{Q}_{\text{logic}}$ be the recovered rationals. The recovered reals are the Cauchy completion of $\mathbb{Q}_{\text{logic}}$ with respect to the uniform structure on $\mathbb{Q}$, yielding a carrier equipped with canonical maps to and from the standard reals $\mathbb{R}$ that are mutual inverses.

background

The module sits immediately after RationalsFromLogic in the foundation tower and imports the standard uniform-space comparison from Mathlib. It introduces the recovered-rational Cauchy sequence, defined so that the Cauchy predicate is measured after transport to Mathlib's $\mathbb{Q}$ with its usual uniform structure. This is the precise location where the recovered rational layer enters the Cauchy completion.

The supplied doc-comment states: "A recovered-rational Cauchy sequence. The Cauchy predicate is measured after transport to Mathlib's ℚ, using the standard uniform structure on ℚ. This is the exact point where the recovered rational layer enters the Cauchy completion." The module also records the round-trip maps and their equality lemmas.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the recovered real line to ComplexFromLogic (which builds complex numbers as pairs of recovered reals), to LogicRealTranscendentals (which defines transcendental functions by transport through the equivalence), and to RecoveredTowerAxiomAudit (which audits the full LogicNat to LogicComplex tower). It completes the rational-to-real step required for any later analytic or physical construction that relies on the recovered number tower.

scope and limits

Does not develop analysis or integration inside the recovered reals.
Does not prove completeness without using Mathlib's uniform-space infrastructure.
Does not connect the recovered reals to the J-cost or forcing-chain constructions.
Does not address non-Archimedean or non-standard extensions.

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