transportComparison
plain-language theorem explainer
Maps a comparison operator on recovered reals to one on Mathlib reals by conjugating with the LogicReal ↔ ℝ equivalence. Anyone proving that recovered-real logic laws imply the classical real laws cites this bridge. The body is a one-line conjugation: apply fromReal on inputs, run C, then toReal on the output.
Claim. Given a comparison operator $C$ on recovered reals ($\mathrm{LogicReal}\to\mathrm{LogicReal}\to\mathrm{LogicReal}$), define a comparison operator on $\mathbb{R}$ by $(x,y)\mapsto \mathrm{toReal}\bigl(C(\mathrm{fromReal}\,x,\,\mathrm{fromReal}\,y)\bigr)$, where $\mathrm{fromReal}$ and $\mathrm{toReal}$ are the mutually inverse transports between Mathlib reals and recovered reals.
background
This module is the recovered-real mirror of Foundation.LogicAsFunctionalEquation. Comparison operators encode the structural content of well-posed comparison: identity (cost of $x$ with itself is zero), reciprocal symmetry, scale invariance, and non-triviality. On ordinary reals these are the four Aristotelian constraints that force the Recognition Composition Law.
Here the domain is LogicReal, the real line recovered from the logic/forcing construction, with transports toReal : LogicReal → ℝ and fromReal : ℝ → LogicReal (via CompareReals.compareEquiv). A recovered-real comparison operator is simply a binary map LogicReal → LogicReal → LogicReal. The classical surface expects ℝ → ℝ → ℝ.
This definition is the conjugation that moves operators across that equivalence so that already-proved real theorems (identity, non-contradiction, scale invariance, non-triviality, and uniqueness of the RCL form) become available on the recovered-real side without re-deriving analytic regularity.
proof idea
Pure definitional conjugation, not a proof. On inputs $x,y:\mathbb{R}$, push into recovered reals by fromReal, apply the given operator $C$, and pull the cost back by toReal. No lemmas are invoked; the term is exactly fun x y => toReal (C (fromReal x) (fromReal y)). Downstream theorems unfold this definition and use toReal_fromReal, lt_iff_toReal_lt, and related transport lemmas to move inequalities and equalities across the bridge.
why it matters
Every recovered-real Law-of-Logic transport theorem factors through this map: identityL_to_real, nonContradictionL_to_real, scaleInvariantL_to_real, nonTrivialL_to_real, and the bundled lawsL_to_real. Those feed RCL_is_unique_functional_form_of_logicL, which states that any recovered-real operator satisfying the laws forces the Recognition Composition Law on the derived cost (the unique multiplicative form $P(u,v)=2u+2v+c,uv$).
In the forcing chain this is infrastructure for treating logic itself as a functional equation on the recovered continuum, so T5 J-uniqueness and the RCL land on LogicReal without a second analytic development. The structure SatisfiesLawsOfLogicL records structural fields natively on LogicReal and routes the analytic/polynomial surface through this transport to the already-verified real theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.