ScaleInvariantOn
plain-language theorem explainer
Scale invariance requires that a comparison operator C on an ordered field K satisfies C(λx, λy) = C(x, y) whenever x, y, λ are positive. Researchers bootstrapping the Law of Logic to the reals cite this predicate as one of the four core conditions packaged inside LogicSupported. The definition is a direct universal quantification over positive field elements with no additional lemmas.
Claim. A map $C : K → K → K$ on a linearly ordered field $K$ is scale-invariant when $∀ x,y,λ ∈ K$ with $x>0$, $y>0$, $λ>0$, one has $C(λx, λy) = C(x,y)$.
background
DomainBootstrap moves from the Law of Logic stated on an ambient ordered field to a uniqueness result recovering the reals. ComparisonOperatorOn is the bare type of binary maps K → K → K. Scale invariance is listed alongside identity and non-contradiction as one of the Aristotelian-style conditions that any such operator must obey. The module documentation notes that the Law of Logic alone does not force Archimedean completeness; that hypothesis is added explicitly to obtain the isomorphism with ℝ. Upstream, Distinguishability supplies the non-vacuous content that at least one positive pair yields a nonzero comparison.
proof idea
This is a definition. It directly encodes the required invariance as a predicate on C by quantifying over all positive x, y, λ in K and asserting equality of the two comparisons.
why it matters
Scale invariance enters the LogicSupported structure, which collects the minimal data needed to state the Law of Logic on K. The structure feeds the bootstrap theorem that any field carrying such an operator plus Archimedean and Dedekind-completeness hypotheses is order-isomorphic to ℝ, closing the loop between the ambient field and the recovered LogicReal. The module documentation identifies this as the explicit resolution of the chicken-and-egg problem between the Law of Logic and the real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.