PositivitySelector
plain-language theorem explainer
The positivity selector is the predicate on a posted real and a carrier that holds exactly when the posted value is strictly positive, ignoring the carrier. It is the canonical joint-scale-invariant criterion used to witness the scale-homogeneity no-go. Anyone citing the boundary result that scale-blind selection cannot fix an absolute value will invoke this as the concrete admission example. The body is a one-line lambda.
Claim. The positivity selector is the relation $S(a,x)$ on a posted real $a\in\mathbb{R}$ and a carrier $x\in X$ defined by $S(a,x)\iff a>0$. It does not depend on $x$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: the uniqueness chain (T-2 through T8) derives structure without a preferred scale, and this file proves abstractly why the chain cannot fix an absolute value on its own. A scale action is a positive-real action on a carrier type $X$. A selector is a predicate on a posted real together with a carrier; it is joint-scale invariant when acceptance is unchanged under simultaneous rescaling of the posted value and the carrier.
A target functional $f:X\to\mathbb{R}$ is scale-invariant when $f(c\cdot x)=f(x)$ for all $c>0$. The no-go states that no joint-scale-invariant selector that accepts an intended witness $(f(x_0),x_0)$ with $f(x_0)>0$ can force the posted value to equal $f$ everywhere: a doubled decoy is also accepted and misses the target.
The positivity selector is the simplest non-vacuous member of that class: it accepts exactly the positive posted values and is blind to the carrier, hence joint-scale invariant for every action.
proof idea
One-line definition: the predicate is the lambda $(a,x)\mapsto (0<a)$, discarding the carrier. No lemmas are applied; the body is pure term construction.
why it matters
This definition supplies the concrete admission witness for the class no-go. Downstream, positivitySelector_jointScaleInvariant proves it is joint-scale invariant for any action; positivitySelector_does_not_force_value shows it cannot force any positive scale-invariant target; and scaleHomogeneityNoGoCert packages both directions of the wall. Instantiations pair_witness (squared ratio on real pairs) and vec_witness (probability weight on eight-component complex vectors) use it to show no scale-blind criterion recovers those absolute posted values.
In the framework this is the public boundary of the forcing chain: after T5–T8 fix $J$, $\varphi$, the eight-tick octave, and $D=3$, absolute scale still requires a scale-bearing input. The paper form is the boundary theorem of "Recognition Composition and the Forced Skeleton"; the ledger instance lives elsewhere as a specialization of this class result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.