toReal_neg
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.