scaleInvariantL_to_real
plain-language theorem explainer
If a comparison operator on recovered reals is scale-invariant, its transport to ordinary reals is scale-invariant. Anyone bridging the LogicReal law-of-logic surface to the analytic functional-equation surface cites this. The proof lifts positivity and multiplication through fromReal/toReal, applies the LogicReal hypothesis, and projects equality back with toReal.
Claim. Let $C$ be a comparison operator on recovered reals. If $C(\lambda x,\lambda y)=C(x,y)$ whenever $x,y,\lambda>0$ in the recovered reals, then the transported operator $\widetilde{C}(x,y)=\mathrm{toReal}(C(\mathrm{fromReal}\,x,\mathrm{fromReal}\,y))$ satisfies $\widetilde{C}(\lambda x,\lambda y)=\widetilde{C}(x,y)$ for all $x,y,\lambda>0$ in $\mathbb{R}$.
background
This module is the recovered-real mirror of LogicAsFunctionalEquation. Structural law-of-logic fields (identity, scale invariance, non-triviality) are stated directly on LogicReal; analytic fields are moved through toReal.
A comparison operator on recovered reals is a map $C:\mathrm{LogicReal}\times\mathrm{LogicReal}\to\mathrm{LogicReal}$. Scale invariance on that side means $C(\lambda x,\lambda y)=C(x,y)$ for positive $x,y,\lambda$. Transport is $\widetilde{C}(x,y)=\mathrm{toReal}(C(\mathrm{fromReal},x,\mathrm{fromReal},y))$, landing on the ordinary real comparison surface.
On the real side, scale invariance is the structural bridge from a two-argument comparison to a one-argument cost on positive ratios: the cost depends only on the ratio, so the four laws of logic (which ignore absolute scale) become constraints on $\mathbb{R}_+$. The maps fromReal/toReal and the lemmas eq_iff_toReal_eq, lt_iff_toReal_lt identify order and equality between the two presentations.
proof idea
Tactic proof. Introduce real $x,y,\lambda>0$. Unfold transport. Lift each positivity hypothesis to LogicReal via lt_iff_toReal_lt, toReal_zero, and toReal_fromReal. Establish the two multiplication identities fromReal(λ)·fromReal(x)=fromReal(λx) and likewise for $y$, by rewriting with eq_iff_toReal_eq and simplifying toReal_fromReal. Apply the LogicReal scale-invariance hypothesis at the lifted points, rewrite the products, and finish by congrArg toReal on the resulting LogicReal equality.
why it matters
Scale invariance is the step that turns a two-argument comparison into a ratio cost, which is how the laws of logic become constraints on the multiplicative group and feed the Recognition Composition Law and the J-uniqueness forcing (T5). This lemma closes the LogicReal-to-real transport for that structural field, parallel to the sibling transports for identity, non-contradiction, and non-triviality in the same module.
No downstream consumers are wired yet (used_by is empty). The intended landing is the real ScaleInvariant surface in LogicAsFunctionalEquation, so that operators built on recovered reals can enter the analytic uniqueness pipeline without re-proving scale invariance by hand. It is pure structural transport: no continuity or polynomial-combiner content is moved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.