IsJointScaleInvariantSelector
plain-language theorem explainer
A selector on posted real values and carriers is jointly scale-invariant when it accepts (a, x) exactly when it accepts (c·a, c·x) for every positive scale c. Anyone stating the Scale Homogeneity No-Go cites this predicate to mark criteria blind to absolute scale. It is a pure Prop definition: the biconditional under the carrier's positive scaling action.
Claim. Fix a type $X$ with a positive-real scaling action $c \cdot x$. A selector $S : \mathbb{R} \to X \to \mathrm{Prop}$ is jointly scale-invariant if, for every $c > 0$, every posted value $a \in \mathbb{R}$, and every carrier $x \in X$, one has $S(a,x)$ if and only if $S(c \cdot a,\, c \cdot x)$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: the uniqueness chain (T-2 through T8) builds the theory without a preferred scale, and this file proves abstractly why the chain cannot fix an absolute value on its own. The carrier $X$ is any type with a positive-real scaling action; the posted value is an ordinary real paired with that carrier.
A selector is a predicate $S(a,x)$ deciding whether the posted value $a$ is admissible for carrier $x$. Joint scale invariance means the decision is unchanged when $a$ and $x$ are rescaled by the same positive factor. The companion notion of scale invariance for a target functional $f : X \to \mathbb{R}$ says $f(c \cdot x) = f(x)$, so the target itself carries no absolute scale.
The module states the no-go in neutral vocabulary and supplies ordinary mathematical witnesses (real pairs with a squared ratio; eight-component complex vectors with a probability weight), so the obstruction is a general fact about scale-invariant selection rather than a quirk of one carrier.
proof idea
Pure definition: the predicate holds exactly when, for every $c > 0$, the biconditional $S(a,x) \leftrightarrow S(c\cdot a,, \mathrm{scale}(c,x))$ is true for all posted values $a$ and carriers $x$. No lemmas are applied; the body is the Prop that downstream theorems quantify over.
why it matters
This is the hypothesis class for the class wall of the Scale Homogeneity No-Go. The main theorem no_scaleInvariantSelector_forces_value shows that any jointly scale-invariant selector accepting the intended witness $(f(x_0), x_0)$ also accepts the doubled decoy $(2f(x_0), 2\cdot x_0)$, so it cannot force the posted value onto a scale-invariant target $f$. The admission export forcingSelector_not_jointScaleInvariant is the contrapositive: any selector that does force the value fails joint scale invariance.
The positivity selector is proved jointly scale-invariant and shown not to force a value, giving non-vacuity. The certificate structure bundles the class wall, the admission export, and that witness. In the framework this is why T0–T8 stop short of absolute units: at least one scale-bearing input is required. The ledger form lives downstream as an instance; the paper form is the S5 amplitude statement in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.