no_scaleInvariantSelector_forces_value
plain-language theorem explainer
No joint-scale-invariant selector that accepts an intended witness can force the posted value onto a scale-invariant target. Cite this as the abstract class form of the scale-homogeneity boundary in the forced skeleton (paper: Recognition Composition and the Forced Skeleton). The proof is a short doubling decoy: joint invariance yields a scaled witness posting twice the target, while scale invariance of the target keeps its value fixed, a contradiction by positivity.
Claim. Let $S:\mathbb{R}\times X\to\mathrm{Prop}$ be invariant under joint positive rescaling of the posted value and the carrier, and let $f:X\to\mathbb{R}$ be scale-invariant under the same action. If $S(f(x_0),x_0)$ holds at some $x_0$ with $f(x_0)>0$, then $S$ cannot force the posted value: it is false that $S(a,x)$ implies $a=f(x)$ for all $a,x$.
background
The module is the boundary theorem of the forced skeleton, stated type-agnostically. The uniqueness chain (T-2 through T8) builds the skeleton without a preferred scale; this file shows why that chain cannot fix absolute values on its own. The carrier $X$ is any type with a positive-real scaling action ScaleAction.
A selector $S$ is jointly scale-invariant when $S(a,x)$ holds if and only if $S(c\cdot a,,c\cdot x)$ for every $c>0$. A target $f$ is scale-invariant when $f(c\cdot x)=f(x)$ for every $c>0$. The intended witness is the pair $(f(x_0),x_0)$ with $f(x_0)>0$: the selector accepts the posted target value on that carrier point.
The statement is deliberately carrier-neutral. Concrete witnesses later (real pairs with a squared ratio; eight-component complex vectors with a probability weight) only instantiate the hypotheses; the no-go itself is a general fact about scale-blind selection.
proof idea
Assume for contradiction that $S$ forces the target: every accepted pair has posted value equal to $f$. From the intended witness $S(f(x_0),x_0)$, joint scale invariance at $c=2$ produces the decoy $S(2f(x_0),,2\cdot x_0)$. Scale invariance of $f$ gives $f(2\cdot x_0)=f(x_0)$. The forcing hypothesis then equates $2f(x_0)$ with $f(2\cdot x_0)$, hence with $f(x_0)$. Positivity of $f(x_0)$ and linarith close the contradiction. Pure term/tactic proof; no external lemmas beyond the two invariance hypotheses and elementary arithmetic.
why it matters
This is the main class theorem of ScaleHomogeneityNoGo: the doubling decoy that stops the forced skeleton from choosing absolute scales. It is the canonical public form used in the paper Recognition Composition and the Forced Skeleton; the ledger instance lives downstream as an instance of this class result.
Direct consumers: the admission-gate export forcingSelector_not_jointScaleInvariant (any forcing selector fails joint invariance); the non-vacuity check that the positivity selector lies in the class yet cannot force; the certificate bundle scaleHomogeneityNoGoCert; and the two concrete witnesses on real pairs and on eight-component complex vectors (the latter tied to the eight-tick octave). Framework role: after T5--T8 force $J$, $\varphi$, the eight-tick period, and $D=3$, this wall shows at least one scale-bearing input is still required before absolute constants can be fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.