ScaleInvariantL
plain-language theorem explainer
Scale invariance for a two-argument comparison operator on recovered reals: positive rescaling of both arguments leaves the value unchanged. Anyone assembling the Law-of-Logic package on LogicReal cites this field. It is a pure Prop definition, not a proved statement.
Claim. A comparison operator $C$ on recovered reals is scale-invariant when, for all recovered reals $x,y,\lambda>0$, one has $C(\lambda x,\lambda y)=C(x,y)$.
background
The module is the recovered-real mirror of LogicAsFunctionalEquation. Structural Law-of-Logic fields (identity, non-contradiction, scale invariance, non-triviality) are stated natively on LogicReal; analytic regularity is transported via LogicReal.toReal.
LogicReal is the Cauchy completion of the recovered rationals, wrapped so Mathlib's completed reals can be reused without polluting global instances. A comparison operator here is simply a map $C:\mathrm{LogicReal}\to\mathrm{LogicReal}\to\mathrm{LogicReal}$.
Scale invariance is the homogeneity condition that only relative scale matters: multiplying both inputs by the same positive factor does not change $C$.
proof idea
Definition only. The body is the universal quantification over positive recovered reals $x,y,\lambda$ asserting $C(\lambda x,\lambda y)=C(x,y)$. No tactics or lemmas.
why it matters
This is one of the four native structural fields of SatisfiesLawsOfLogicL, the recovered-real Law of Logic package. Downstream, scaleInvariantL_to_real pushes the property across transportComparison to the already-verified real-line scale-invariance predicate, so the structural half of the Law of Logic can be checked on LogicReal while analytic content rides on the real theorem.
In the broader Recognition forcing chain, scale-free comparison is the structural counterpart of the J-cost's multiplicative homogeneity (T5 J-uniqueness and the Recognition Composition Law live on ratios). Without this field the recovered-real Law of Logic would not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.