toReal_div
plain-language theorem explainer
The theorem establishes that the canonical transport from the recovered real line to the standard reals preserves division. Researchers recovering algebraic identities in the Recognition Science foundation layer cite it when moving rational operations across the completion. The proof is a one-line wrapper that invokes the round-trip lemma for the transport map.
Claim. Let $x, y$ be elements of the recovered real line obtained as the Cauchy completion of the logic-derived rationals. The canonical embedding $i$ into the standard reals satisfies $i(x / y) = i(x) / i(y)$.
background
The module recovers the real numbers from the law-of-logic rationals by completing the rationals via Mathlib's Bourbaki completion. LogicReal is a wrapper around the completed rationals that prevents global instance pollution while allowing reuse of the standard real line. The map toReal is the comparison equivalence that transports a recovered real to the standard reals.
proof idea
The proof is a one-line wrapper that applies the round-trip lemma toReal_fromReal.
why it matters
This result is invoked directly in the proof of the transported hyperbolic cosine identity. It supplies the missing algebraic transport step for division, allowing identities on the standard reals to be read back on the recovered line. Within the Recognition framework it supports the reals-from-logic recovery chain that precedes the eight-tick octave and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.