forcingSelector_not_jointScaleInvariant
plain-language theorem explainer
Any selector that forces the posted real to equal a scale-invariant target on an accepted witness cannot be joint-scale invariant. Admission-gate form of the scale-homogeneity no-go: forcing absolute values rules out blindness to joint rescaling. One-line contrappositive of the doubling-decoy class theorem.
Claim. Fix a positive-real scaling action on a carrier $X$. Let $f:X\to\mathbb{R}$ be scale-invariant and $S:\mathbb{R}\times X\to\mathrm{Prop}$ a selector. If there is a witness $x_0$ with $f(x_0)>0$, $S(f(x_0),x_0)$ holds, and $S$ forces every accepted pair to satisfy $a=f(x)$, then $S$ is not invariant under joint positive rescaling of the posted value and the carrier.
background
This module is the boundary theorem of the forced skeleton in neutral vocabulary. The uniqueness chain (T-2 through T8) builds the theory without fixing a scale; the no-go shows why the chain cannot continue on pure selection alone. The carrier $X$ is any type with a positive-real scaling action act.
A target $f:X\to\mathbb{R}$ is scale-invariant when $f(\mathrm{scale},c,x)=f(x)$ for every $c>0$. A selector $S$ is joint-scale invariant when $S(a,x)$ holds if and only if $S(c\cdot a,\mathrm{scale},c,x)$ for every $c>0$. The main class result is the doubling decoy: no joint-scale-invariant selector that accepts the intended witness can force the posted value onto a scale-invariant target, because joint invariance yields $S(2f(x_0),\mathrm{scale},2,x_0)$ while scale invariance of $f$ gives $f(\mathrm{scale},2,x_0)=f(x_0)\neq 2f(x_0)$.
The present declaration is the admission-gate export of that class wall: if a selector does force the posted value, it cannot be joint-scale invariant.
proof idea
One-line wrapper. Assume joint-scale invariance of $S$, then apply no_scaleInvariantSelector_forces_value to the same data (action, selector, scale-invariant target, positive witness, acceptance, and forcing hypothesis). That lemma produces a contradiction, so the assumption is false.
why it matters
Feeds the certificate scaleHomogeneityNoGoCert as its admission_export field: any forcing selector is certified not joint-scale invariant. Together with the class wall (no_scaleInvariantSelector_forces_value), this is the public boundary theorem used in "Recognition Composition and the Forced Skeleton".
In the forcing chain, T5--T8 fix the J-cost, $\varphi$, the eight-tick octave, and $D=3$ without choosing an absolute scale. This no-go is why at least one scale-bearing input is required before absolute values (masses, couplings) can be pinned. The ledger form MassGenesis.T10JointScaleHomogeneityNoGo is an instance of the same class theorem. No open scaffold: the module is sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.