toReal_sub
The theorem shows that the canonical transport from recovered reals to standard reals preserves subtraction. Foundation-layer work in Recognition Science cites it when reducing algebraic identities on the completed LogicReal to their Mathlib counterparts. The proof is a one-line wrapper applying the round-trip property of the transport map.
claimLet $phi$ be the canonical transport from the recovered real line to the standard reals. Then $phi(x - y) = phi(x) - phi(y)$ for all recovered reals $x, y$.
background
The module recovers the real numbers from the Law-of-Logic rational layer by completing the recovered rationals LogicRat to LogicReal via Mathlib's Bourbaki completion of Q. LogicReal is a wrapper around CompareReals.BourbakiR to avoid polluting global instances while reusing the completed real line. The map toReal is the canonical comparison equivalence with Mathlib's Cauchy reals, and algebra on LogicReal is defined by pulling back structures along this map.
proof idea
One-line wrapper that applies the round-trip theorem toReal_fromReal after the subtraction on LogicReal is unfolded via the transport definition.
why it matters in Recognition Science
The result belongs to the transport-first API that lets every algebraic identity on LogicReal reduce to an existing real theorem and be read back. It fills the subtraction case in the chain from LogicRat through completion to an equivalence with R, supporting the overall recovery of the reals from the Law of Logic.
scope and limits
- Does not establish the full ring-homomorphism property for the transport map.
- Does not address order or topological preservation.
- Does not treat division or other non-subtraction operations.
formal statement (Lean)
142@[simp] theorem toReal_sub (x y : LogicReal) : toReal (x - y) = toReal x - toReal y :=
proof body
One-line wrapper that applies toReal_fromReal.
143 toReal_fromReal _