lawsL_to_real
plain-language theorem explainer
Any comparison operator on recovered reals that satisfies the recovered-real laws of logic transports, via the real embedding, to a comparison operator that satisfies the ordinary real laws of logic. Downstream uniqueness of the Recognition Composition Law on recovered reals cites this bridge. The proof is a one-line field projection from the recovered-real law structure.
Claim. If $C$ is a comparison operator on recovered reals and $C$ satisfies the recovered-real laws of logic (identity, non-contradiction, scale invariance, non-triviality, together with the transported analytic regularity package), then the transported real operator $(x,y)\mapsto \mathrm{toReal}(C(\mathrm{fromReal}\,x,\mathrm{fromReal}\,y))$ satisfies the ordinary real laws of logic.
background
This module is the recovered-real mirror of Foundation.LogicAsFunctionalEquation. Comparison operators are maps $C:\mathrm{LogicReal}\times\mathrm{LogicReal}\to\mathrm{LogicReal}$. The structure of recovered-real laws packages four native structural axioms (identity, non-contradiction, scale invariance, non-triviality) plus an explicit transport field asserting that the real image already satisfies the verified real law package.
Transport is the pointwise embedding transportComparison: send a recovered-real operator to the real operator $(x,y)\mapsto\mathrm{toReal}(C(\mathrm{fromReal},x,\mathrm{fromReal},y))$. On the real side, SatisfiesLawsOfLogic requires the Aristotelian constraints together with scale invariance and route-independence (the bridge from two-argument form to a one-argument cost).
The present theorem simply exposes that transport field as a standalone implication, so downstream results can invoke the real theorem surface without unpacking the recovered-real structure by hand.
proof idea
One-line term proof: project the field transported_real_laws from the hypothesis SatisfiesLawsOfLogicL C. That field is definitionally the desired real-side satisfaction statement for transportComparison C. No further rewriting or analytic work is required.
why it matters
This is the bridge lemma that lets recovered-real logic inherit the real uniqueness theorem for the Recognition Composition Law. Its sole downstream consumer is RCL_is_unique_functional_form_of_logicL, whose doc-comment states: "RCL is forced for recovered-real logic, by transport through the existing real theorem." That parent result concludes multiplicative consistency of the derived cost with the bilinear combiner $P(u,v)=2u+2v+c,uv$, i.e. the RCL functional form.
In the forcing chain this sits under T5 (J-uniqueness): once laws of logic hold, the cost is forced to $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, and RCL is the two-argument identity that characterizes it. Without this transport, the recovered-real development would have to re-prove the entire real analytic package rather than reuse it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.