toReal_neg
Negation is preserved under the canonical transport from the recovered real line to Mathlib reals. Researchers rebuilding analysis from the logic layer cite it when moving sign changes across the equivalence. The argument is a one-line wrapper that invokes the round-trip fact toReal_fromReal.
claimFor every recovered real $x$, the transport satisfies $toReal(-x) = -toReal(x)$.
background
RealsFromLogic recovers the reals by completing the rationals LogicRat (obtained from the Law of Logic) via Mathlib's Bourbaki completion of ℚ. LogicReal wraps CompareReals.Bourbakiℝ to avoid global instance pollution, while toReal applies the canonical equivalence compareEquiv to reach a standard real. Algebra on LogicReal is defined by transport, so every identity reduces to the corresponding theorem on ℝ.
proof idea
One-line wrapper that applies toReal_fromReal.
why it matters in Recognition Science
It is invoked inside coshL_eq_exp to handle the sign flip when transporting the hyperbolic-cosine identity. This belongs to the transport layer that lets the Recognition framework import standard real analysis without rebuilding it from the logic axioms, supporting later steps such as the phi-ladder and the eight-tick octave.
scope and limits
- Does not construct the completion from the logic axioms directly.
- Does not address ordering or the uniform structure on LogicReal.
- Does not treat multiplication or other ring operations.
Lean usage
rw [toReal_neg]formal statement (Lean)
140@[simp] theorem toReal_neg (x : LogicReal) : toReal (-x) = -toReal x :=
proof body
One-line wrapper that applies toReal_fromReal.
141 toReal_fromReal _