IsScaleInvariant
plain-language theorem explainer
A real-valued functional on a scaled carrier is scale-invariant when positive rescaling of the carrier leaves its value unchanged. Anyone citing the scale-homogeneity no-go (the doubling decoy) needs this predicate as the target-side hypothesis. The body is a one-line universal quantification over positive scales, not a derived proof.
Claim. Fix a type $X$ with a positive-real scaling action. A map $f : X \to \mathbb{R}$ is scale-invariant when, for every $c > 0$ and every $x \in X$, one has $f(c \cdot x) = f(x)$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton, stated in neutral vocabulary. The uniqueness chain (T-2 through T8) builds the skeleton without a preferred scale; this module shows abstractly why the chain cannot fix absolute values on its own.
A scale action equips a carrier type $X$ with a map that multiplies configurations by positive reals. The companion notion of joint scale invariance applies to selectors $S : \mathbb{R} \to X \to \mathrm{Prop}$ that treat a posted value and its carrier together. Scale invariance of a target functional $f$ is the complementary property: $f$ itself is blind to rescaling of the carrier.
Two concrete carriers instantiate the setup later in the file: real pairs with a squared-ratio functional, and eight-component complex vectors with a probability weight. Both functionals satisfy this predicate, so the no-go is a general fact about scale-invariant selection rather than a quirk of one carrier.
proof idea
Pure definition: the predicate is the proposition that for every positive real $c$ and every point $x$, evaluating $f$ after scaling the carrier by $c$ returns the same real as evaluating $f$ at $x$. No lemmas are applied; downstream theorems unfold or apply this Prop directly.
why it matters
This is the target-side hypothesis of the class wall. The main theorem no_scaleInvariantSelector_forces_value (the doubling decoy) assumes a joint-scale-invariant selector that accepts the intended witness $(f(x_0), x_0)$ and concludes it cannot force the posted value to equal the scale-invariant target: joint invariance produces the decoy $(2 f(x_0), \mathrm{scale}, 2, x_0)$, while scale invariance of $f$ keeps the target at $f(x_0) \neq 2 f(x_0)$.
Admission and non-vacuity exports reuse it: any selector that does force the value cannot be joint-scale invariant, and the positivity selector (which is joint-scale invariant) therefore cannot force the target. Concrete witnesses pairRatio and probWeight are proved scale-invariant under their respective actions. The certificate structure bundles the class wall over all such $f$.
In the Recognition framework this is the public form of the boundary used in "Recognition Composition and the Forced Skeleton": after T5–T8 force $J$, $\varphi$, the eight-tick octave, and $D=3$, at least one scale-bearing input is still required before absolute values (masses, couplings) can be fixed. The ledger instance lives downstream as an instance of this class theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.