quadrantSelector_invariant
plain-language theorem explainer
The positive-quadrant selector enforcing the ratio a=2b is invariant under joint positive rescaling of both coordinates. Anyone citing the amplitude-form scale-homogeneity no-go needs this: the paper's witness selector is blind to absolute scale. The proof is a short cancellation using that the scale factor is nonzero, via the zero-divisor law.
Claim. On the positive quadrant $X=\{(a,b)\in\mathbb{R}^2:a>0,\,b>0\}$ with scaling $c\cdot(a,b)=(ca,cb)$ for $c>0$, the predicate $P(a,b)\equiv(a=2b)$ satisfies $P(c\cdot x)\leftrightarrow P(x)$ for every positive scale $c$ and every $x\in X$.
background
This module is the boundary theorem of the forced skeleton: the uniqueness chain (T-2 through T8) builds the theory without a scale, and the no-go shows why the chain cannot fix an absolute value by itself. Any selector blind to joint rescaling of a posted value and its carrier that accepts an intended witness also accepts a doubled decoy. At least one scale-bearing input is required.
A scaled configuration space carries a type $X$ with a positive-real action. An invariant selector is a predicate $P:X\to\mathrm{Prop}$ such that $P(c\cdot x)\leftrightarrow P(x)$ for every $c>0$. The positive quadrant is the concrete space with $X={(a,b):a>0,b>0}$, scaling both coordinates by $c$, and amplitude equal to the first coordinate. The witness selector is the ratio condition $a=2b$.
The argument uses that the ambient ring has no zero divisors (from the integers-from-logic development): $ab=0$ forces $a=0$ or $b=0$.
proof idea
Unfold invariance at scale $c>0$ and point $p=(a,b)$ in the positive quadrant. The goal is the biconditional $(ca=2(cb))\leftrightarrow(a=2b)$.
Forward: from $ca=2cb$, rewrite as $c(a-2b)=0$. Since $c>0$, one has $c\neq 0$. Apply the zero-divisor law; the $c=0$ branch is absurd, so $a-2b=0$, hence $a=2b$ by linear arithmetic.
Backward: substitute $a=2b$ into the scaled equality and clear by ring.
why it matters
This pins the paper's positive-quadrant witness as a genuine invariant selector, so it is admissible input to the amplitude-form no-go. Downstream, quadrant_witness uses it to exhibit a selected point with positive amplitude while showing the selector does not force that amplitude to equal 2: existence of a selected positive-amplitude configuration together with failure of universal amplitude forcing.
In the framework this is the concrete S5 witness for the boundary of the forced skeleton (T-2 through T8). The chain derives structure without a scale; the no-go shows a scale-invariant ratio target cannot be pinned to an absolute amplitude by any jointly scale-blind criterion. The ledger instantiation in MassGenesis is an instance of the same class theorem. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.