quadrantPoint21_selected
plain-language theorem explainer
The positive-quadrant point (2,1) satisfies the witness selector a = 2b. Anyone assembling the amplitude-form scale-homogeneity no-go cites this as the concrete selected configuration. The proof is a one-line arithmetic check that 2 equals 2·1.
Claim. The point $(2,1)$ in the positive quadrant lies in the selector set defined by $a = 2b$: writing $p=(a,b)$, one has $a=2b$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: after the uniqueness chain (T-2 through T8) builds a scale-free theory, no selection rule blind to joint rescaling of a posted value and its carrier can pin an absolute scale. The amplitude form restates the paper's S5: over a scaled configuration space with a degree-one homogeneous amplitude, an invariant selector either forces amplitude zero or accepts every positive amplitude.
Here the carrier is the positive quadrant of $\mathbb{R}^2$, with points $p=(a,b)$ for $a,b>0$. The witness selector is the ray $a=2b$. The witness point is the concrete pair $(2,1)$ on that ray. The amplitude on this space is the scale-sensitive quantity that the no-go leaves free once the ratio is fixed.
proof idea
Unfold the selector at the witness point: the claim is exactly $(2:\mathbb{R})=2\cdot 1$. Discharge by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This is the first conjunct of quadrant_witness, which packages existence of a selected positive-amplitude point together with the failure of every selected point to share a fixed amplitude. That witness pins the scale-invariant ratio $a/b$ to 2 while leaving amplitude free, exactly the positive-quadrant instance of the amplitude-form no-go (paper S5). Downstream it supports the claim that the forced skeleton cannot fix absolute scales without at least one scale-bearing input, the public boundary theorem of "Recognition Composition and the Forced Skeleton".
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.