positivitySelector_jointScaleInvariant
plain-language theorem explainer
The positivity selector (accept pairs $(a,x)$ exactly when $a>0$) is invariant under joint positive rescaling of the posted value and the carrier, for any scale action. Anyone citing the scale-homogeneity no-go needs this as the canonical non-vacuous member of the joint-invariant class. The proof is a two-direction positivity check: $a>0$ iff $c\cdot a>0$ when $c>0$.
Claim. For any type $X$ equipped with a positive-real scale action, the selector $S(a,x)\iff(a>0)$ satisfies: 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) derives the theory without a scale, and this file shows abstractly why the chain cannot fix absolute values on its own. A selector $S:\mathbb{R}\to X\to\mathrm{Prop}$ is joint-scale invariant when $S(a,x)\leftrightarrow S(c\cdot a,,c\cdot x)$ for all $c>0$. A target $f:X\to\mathbb{R}$ is scale-invariant when $f(c\cdot x)=f(x)$.
The positivity selector ignores the carrier entirely and keeps only the sign condition $a>0$. Because joint rescaling multiplies the posted value by a positive constant, positivity is automatically preserved. The module is deliberately type-agnostic: any carrier with a $\mathbb{R}_{>0}$-action works; concrete witnesses later use real pairs and eight-component complex vectors.
proof idea
Unfold joint-scale invariance and introduce $c>0$, $a$, and $x$. The two directions of the biconditional are pure real arithmetic on the posted value (the carrier is ignored by the selector).
Left-to-right: if $a>0$ and $c>0$ then $c\cdot a>0$ by the standard product-of-positives fact. Right-to-left: if $c\cdot a>0$ and $c>0$ then $a>0$ by positivity of the right factor under a positive left factor. No property of the scale action beyond the type signature is used.
why it matters
This lemma supplies the non-vacuous inhabitant of the joint-invariant class that the no-go needs. Downstream, positivitySelector_does_not_force_value feeds it into the abstract wall: any joint-invariant selector that accepts a positive intended witness also accepts a doubled decoy, so it cannot force the target value. The same fact is wired into scaleHomogeneityNoGoCert (the certificate packaging both the class wall and the admission export) and into the concrete instantiations pair_witness (squared ratio on real pairs) and vec_witness (probability weight on eight-component complex vectors).
In the paper framing this is the canonical public form of the boundary theorem of "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. The ledger-level MassGenesis instance is a specialization of the class theorem proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.