nonContradictionL_to_real
plain-language theorem explainer
If a comparison operator on recovered reals is symmetric under argument swap on the positive cone, its transport to ordinary reals inherits the same reciprocal symmetry. Anyone wiring LogicReal comparison laws into the real-side functional-equation surface cites this bridge. The proof lifts positivity via the toReal/fromReal order isomorphism and applies congrArg toReal to the LogicReal identity.
Claim. Let $C$ be a binary comparison operator on recovered reals. If $C(x,y)=C(y,x)$ whenever $x>0$ and $y>0$ in the recovered-real order, then the transported real operator $(x,y)\mapsto \mathrm{toReal}(C(\mathrm{fromReal}\,x,\mathrm{fromReal}\,y))$ satisfies $C_{\mathbb{R}}(x,y)=C_{\mathbb{R}}(y,x)$ for all ordinary reals $x,y>0$.
background
This module is the recovered-real mirror of LogicAsFunctionalEquation. Comparison operators are stated directly on LogicReal (the reals reconstructed from the logic/forcing spine); analytic regularity is pushed through toReal, while structural laws such as identity, reciprocal symmetry, scale invariance, and non-triviality live natively on LogicReal.
A comparison operator over recovered reals is simply a map $C:\mathrm{LogicReal}\times\mathrm{LogicReal}\to\mathrm{LogicReal}$. Non-contradiction (reciprocal symmetry) asserts $C(x,y)=C(y,x)$ on the positive cone. On the ordinary-real side the same law is the Aristotelian counterpart: if comparison failed to be single-valued under reordering, the same comparison would simultaneously hold and not hold.
Transport is the bridge transportComparison: evaluate $C$ after embedding ordinary positives via fromReal, then project back with toReal (the evaluation $\mathbb{Z}[\varphi]\to\mathbb{R}$, $\langle a,b\rangle\mapsto a+b\varphi$, extended to the recovered reals). The companion facts toReal_zero and the order isomorphism lt_iff_toReal_lt make positivity transfer mechanical.
proof idea
Tactic proof, four steps. Introduce ordinary positives $x,y>0$. Unfold the transport definition so the goal is an equality of toReal images. Rebuild positivity on the LogicReal side: rewrite lt_iff_toReal_lt, cancel toReal_zero and toReal_fromReal, and reuse the real inequalities. Apply the LogicReal non-contradiction hypothesis at fromReal x and fromReal y, then push the resulting equality through congrArg toReal.
why it matters
Part of the structural-law transport suite (identityL_to_real, scaleInvariantL_to_real, nonTrivialL_to_real, …) that lets every law-of-logic field proved on recovered reals descend to the existing real comparison-operator surface used by the Recognition Composition Law and the J-cost uniqueness chain (T5). Reciprocal symmetry is the mathematical stand-in for Aristotelian non-contradiction; without this bridge, a LogicReal proof of symmetry would not automatically feed the real-side forcing arguments that pin $J(x)=(x+x^{-1})/2-1$.
No downstream consumers are wired yet (used_by is empty), so the lemma presently closes the mirror interface rather than a named parent theorem. It is the non-contradiction half of showing that a LogicReal operator satisfying the full law package transports to an ordinary operator that can enter the functional-equation uniqueness pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.