CauchySeqLogicRat
plain-language theorem explainer
CauchySeqLogicRat packages a sequence of recovered rationals whose images under the transport toRat form a Cauchy sequence in the standard uniform structure on ℚ. Researchers recovering the real line from the Law-of-Logic rational layer cite it as the direct input to the Bourbaki completion. The definition is a two-field structure that pulls the Cauchy predicate across the equivalence LogicRat ≃ ℚ.
Claim. A recovered-rational Cauchy sequence consists of a map $s : ℕ → LogicRat$ together with a proof that the transported sequence $n ↦ toRat(s(n))$ is Cauchy in the uniform space $ℚ$.
background
The module recovers the reals from the Law of Logic by constructing LogicNat, LogicInt and LogicRat with LogicRat ≃ ℚ, then applying Mathlib's Bourbaki completion of ℚ to obtain LogicReal ≃ ℝ. Arithmetic and order on LogicReal are defined by transport along the equivalence toReal, so every theorem reduces to the corresponding statement on the completed rationals.
proof idea
The structure is introduced directly by its two fields: seq of type ℕ → LogicRat and cauchy_toRat asserting that the image sequence under toRat is Cauchy. The helper definition toRatSeq projects the sequence component, and the theorem toRatSeq_cauchy returns the supplied field verbatim.
why it matters
This structure supplies the precise interface at which the recovered rationals enter the Cauchy completion, enabling the wrapper LogicReal that reuses Mathlib's real line without global instance pollution. It completes the chain Law of Logic ⊢ LogicRat ≃ ℚ ⊢ Completion ℚ ≃ ℝ required for the Recognition framework's real-valued quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.