quadrant_ratio_pinned
plain-language theorem explainer
On the positive quadrant with the selector a = 2b, the scale-invariant ratio a/b is constantly 2. Anyone checking the amplitude-form boundary theorem (or the paper's "what this does not add" remark) cites this pinning. The proof is a short field-simplification from the selector equality and positivity of b.
Claim. Let $p = (a,b)$ lie in the open positive quadrant $\{(x,y)\in\mathbb{R}^2 : x>0,\, y>0\}$. If the selector $a = 2b$ holds, then the scale-invariant readout satisfies $a/b = 2$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: the uniqueness chain (T-2 through T8) builds the theory without a scale, and this file shows abstractly why the chain cannot fix an absolute value using only joint-scale-blind selection. Any selector invariant under simultaneous rescaling of a posted value and its carrier that accepts an intended witness also accepts a doubled decoy missing the target, so at least one scale-bearing input is required.
The amplitude form works over a scaled configuration space (a positive-real action with a degree-one homogeneous amplitude). The positive-quadrant witness takes $X = {(a,b)\in\mathbb{R}^2 : a>0,, b>0}$ with diagonal scaling $(a,b)\mapsto(c a, c b)$. The paper's witness selector is the linear relation $a = 2b$. The natural scale-invariant readout on this space is the ratio $B(a,b) = a/b$, constant on orbits.
proof idea
Unpack the selector hypothesis to $a = 2b$. Positivity of the second coordinate gives $b \neq 0$, so division is legal. field_simp clears the denominator; linarith finishes $a/b = 2$. No external lemmas beyond ne_of_gt and elementary field arithmetic.
why it matters
This is the kernel check behind the paper's "what this theorem does not add" remark in the amplitude-form S5 statement: the invariant selector pins the ratio $a/b$ to 2 on every selected configuration while leaving the homogeneous amplitude free. It therefore exhibits exactly the scale-invariant content that joint-scale-blind selection can force, and nothing more. That contrast is the content of the boundary theorem used in "Recognition Composition and the Forced Skeleton": the forcing chain through T8 (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) cannot by itself fix absolute scales. The ledger instantiation lives elsewhere as an instance of the class theorem; this lemma is the elementary pinning step for the positive-quadrant witness. No downstream dependents are recorded in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.