ScaleInvariantOn
plain-language theorem explainer
Scale invariance for a comparison operator C on an ordered field K requires C(λx, λy) = C(x, y) for all positive x, y, λ. Researchers building the bootstrap of logic-supported fields cite it when packaging the conditions for the Law of Logic. The predicate is introduced by direct universal quantification over field elements satisfying the positivity hypotheses.
Claim. Let $K$ be a field equipped with zero, order, and multiplication. For a comparison operator $C : K → K → K$, scale invariance holds 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 reals to a uniqueness result: any ordered field supporting a comparison operator that meets the Aristotelian conditions plus scale invariance and distinguishability is canonically isomorphic to ℝ. ComparisonOperatorOn is the type of maps $K → K → K$ that serve as such operators. The module explicitly separates the analytic input (Archimedean and Dedekind completeness) from the logical conditions recovered inside the framework.
proof idea
Direct definition. The body is the universal quantification that encodes the invariance condition; no lemmas or tactics are invoked.
why it matters
ScaleInvariantOn supplies one of the four conditions required by the LogicSupported structure, which packages the ordered-field data needed to state the Law of Logic. That structure feeds the bootstrap theorem asserting that any such field is isomorphic to ℝ, closing the loop between the functional equation and the recovered real line. It sits inside the foundation move that derives the ambient field from the comparison operator without circularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.