module module high

`IndisputableMonolith.Foundation.RealsFromLogic`

This module constructs the recovered real line as the Cauchy completion of recovered rationals, with the Cauchy predicate evaluated after transport to standard rationals. Modules building complex numbers and transported transcendentals cite it to obtain an equivalence with Mathlib reals. The module supplies the relevant sequence type, quotient construction, and round-trip maps.

claimLet LogicRat be the recovered rationals. Define CauchySeqLogicRat as sequences in LogicRat whose image in $ℚ$ is Cauchy under the standard uniform structure. The recovered reals LogicReal are the resulting completion, equipped with maps toReal : LogicReal → $ℝ$ and fromReal : $ℝ$ → LogicReal that satisfy toReal ∘ fromReal = id and fromReal ∘ toReal = id.

background

The module continues the logic-derived number tower after RationalsFromLogic. It introduces recovered-rational Cauchy sequences by transporting the Cauchy predicate to Mathlib's $ℚ$ and its standard uniform structure; this is the precise step at which the rational layer enters the Cauchy completion. The resulting LogicReal carries explicit equivalence maps to the standard reals.

proof idea

This is a definition module. It defines the CauchySeqLogicRat predicate by transport to $ℚ$, constructs LogicReal as the quotient completion, and supplies the maps toReal, fromReal together with the round-trip lemmas toReal_fromReal and fromReal_toReal.

why it matters in Recognition Science

The module supplies LogicReal and its equivalence to $ℝ$ to ComplexFromLogic for the complex carrier, to LogicRealTranscendentals for transport of transcendental functions, and to RecoveredTowerAxiomAudit for the full tower audit. It fills the real-number step in the recovered tower LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex.

scope and limits

Does not develop analytic properties or integration on LogicReal.
Does not construct the reals without using Mathlib's uniform structure on $ℚ$.
Does not address other completions such as p-adics.
Does not interpret the recovered reals in physical units or constants.

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