quadrantSelector
plain-language theorem explainer
Witness selector on the positive quadrant: pairs (a,b) with a = 2b. Cited by anyone using the amplitude-form scale-homogeneity no-go, where an invariant criterion must pin the ratio while leaving amplitude free. One-line predicate on the scaled configuration space of positive real pairs.
Claim. On the positive quadrant $X = \{(a,b)\in\mathbb{R}_{>0}\times\mathbb{R}_{>0}\}$ equipped with the diagonal $\mathbb{R}_{>0}$-scaling action, define the selector $S:X\to\mathrm{Prop}$ by $S(a,b)\iff a=2b$.
background
The module proves the boundary of the forced skeleton (T-2 through T8): no selection criterion blind to joint rescaling of a posted value and its carrier can fix an absolute scale-invariant target. Any criterion that accepts the intended witness also accepts a doubled decoy whose posted value misses the target, so at least one scale-bearing input is required.
The amplitude form (paper S5) works over a scaled configuration space: a type $X$ with a positive-real action and a degree-one homogeneous amplitude $A$. An invariant selector's selected amplitude set is contained in ${0}$ or contains every positive real.
The carrier used here is the positive quadrant: $X={(a,b):a>0,b>0}$ with $c\cdot(a,b)=(ca,cb)$ and amplitude equal to the first coordinate. The selector below is the paper's concrete witness on that space.
proof idea
Pure definition: the predicate is the lambda $p \mapsto p.1.1 = 2\cdot p.1.2$ on the subtype of positive pairs. No proof obligations; the body is the equality $a=2b$ on the underlying pair.
why it matters
This is the paper's witness selector for the amplitude-form no-go. Downstream it is shown to be an invariant selector, to accept the point $(2,1)$ with positive amplitude, to pin the scale-invariant readout $a/b$ to $2$ on every selected configuration, and to serve as the existential half of the quadrant witness (selected points exist with $A>0$, yet $A$ is not forced to any fixed positive value).
That witness instantiates the general statement that an invariant selector cannot force a positive amplitude: the ratio is pinned, the absolute scale is free. In the Recognition framework this marks why the uniqueness chain stops without a scale-bearing input, the boundary theorem of "Recognition Composition and the Forced Skeleton".
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.