positivitySelector_does_not_force_value
plain-language theorem explainer
The positivity selector (accept any positive posted value, ignore the carrier) cannot force a scale-invariant target to one absolute value. Citers of the scale-homogeneity boundary theorem use this as the non-vacuity witness: the selector class is inhabited and the doubling-decoy argument applies. The proof is a one-line specialization of the joint-selector class theorem, feeding joint scale-invariance of positivity and the positivity witness twice.
Claim. Let $f : X \to \mathbb{R}$ be scale-invariant under a positive-real scaling action on $X$, and suppose $f(x_0) > 0$. Then the positivity selector (which accepts $(a,x)$ exactly when $a > 0$) does not force the posted value: it is not the case that every accepted pair satisfies $a = f(x)$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton in neutral vocabulary. The uniqueness chain (T-2 through T8) builds the skeleton without a scale; this module shows abstractly why the chain cannot fix absolute values on its own. Any selection criterion blind to joint rescaling of a posted value and its carrier that accepts the intended witness also accepts a doubled decoy whose posted value misses the target. Hence at least one scale-bearing input is required.
A target $f$ is scale-invariant when $f(\mathrm{scale}, c, x) = f(x)$ for every $c > 0$. A joint-scale-invariant selector $S$ is stable under simultaneous rescaling of the posted real and the carrier. The positivity selector accepts exactly the pairs with positive posted value and ignores the carrier, so it is joint-scale-invariant for any action.
The upstream class theorem states the doubling decoy: no joint-scale-invariant selector that accepts the intended witness can force the posted value onto a scale-invariant target, because acceptance of $(f(x_0), x_0)$ yields acceptance of $(2 f(x_0), \mathrm{scale}, 2, x_0)$ while $f(\mathrm{scale}, 2, x_0) = f(x_0) \neq 2 f(x_0)$.
proof idea
One-line term wrapper. Apply the class theorem no_scaleInvariantSelector_forces_value to the positivity selector, supplying joint scale-invariance of positivity (proved by a short constructor on mul_pos / pos_of_mul_pos_right), the given scale-invariance of $f$, the base point $x_0$, and the positivity hypothesis twice: once as $0 < f(x_0)$ and once as the acceptance witness $S(f(x_0), x_0)$.
why it matters
This is the non-vacuity export for the scale-homogeneity no-go: the positivity selector lies in the joint-invariant class, accepts the intended witness whenever the target is positive there, and therefore cannot force the target value. Together with the class wall and the admission export it feeds the module certificate that packages the boundary theorem used in the paper "Recognition Composition and the Forced Skeleton".
In the Recognition framework the uniqueness chain (T5 J-uniqueness through T8, $D=3$) derives the skeleton without fixing an absolute scale. This lemma makes precise that a purely positivity-based, scale-blind criterion is insufficient; a scale-bearing input is mandatory. The ledger instantiation lives downstream as an instance of the class theorem proved here. No direct used_by edges are recorded on this specialization itself; its role is the concrete inhabited witness inside the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.