quadrantPoint21
plain-language theorem explainer
Concrete witness point (2, 1) in the open positive quadrant, used as the intended configuration for the amplitude-form scale-homogeneity no-go. Anyone citing the S5-style boundary theorem on scaled configuration spaces needs this pair: its ratio pins a/b = 2 while the amplitude stays free under joint rescaling. Construction is a one-line subtype package with positivity discharged by numeric normalization.
Claim. The point $(2,1)$ lies in the positive quadrant $\{(a,b)\in\mathbb{R}\times\mathbb{R}: a>0,\,b>0\}$, regarded as a scaled configuration space whose amplitude is the first coordinate.
background
The module proves the boundary theorem of the forced skeleton: after the uniqueness chain (T-2 through T8) builds the scale-free skeleton, no selection criterion blind to joint rescaling of a posted value and its carrier can fix an absolute value for a scale-invariant target. Any criterion that accepts an intended witness also accepts a doubled decoy whose posted value misses the target, so at least one scale-bearing input is required.
The positive-quadrant carrier is the concrete scaled configuration space whose underlying type is pairs of strictly positive reals, with the $\mathbb{R}_{>0}$-action scaling both coordinates and with amplitude equal to the first coordinate. The witness point is the ordinary pair $(2,1)$ packaged as an element of that subtype.
proof idea
Definitional one-liner: form the subtype element $\langle(2,1),_\rangle$ and discharge the two positivity side-conditions $0<2$ and $0<1$ by norm_num. No lemmas beyond the ambient scaled-configuration-space structure are invoked.
why it matters
This point is the intended witness for the paper's S5 amplitude-form no-go over scaled configuration spaces. Downstream it feeds three facts: the amplitude equals 2 by definitional reduction; the quadrant selector accepts it (because $2=2\cdot 1$); and the composite witness theorem, which asserts existence of a selected point of positive amplitude together with failure of every selected point to have amplitude exactly 2. That composite is the positive-quadrant instantiation of the general statement that an invariant selector's selected amplitude set is contained in ${0}$ or contains every positive real. In the Recognition framework it marks why the forcing chain cannot fix absolute scales without a scale-bearing input, matching the ledger-level joint-scale-homogeneity no-go used later in the library.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.