pairRatio_scaleInvariant
plain-language theorem explainer
The squared first-component share of a real pair is invariant under joint positive rescaling of both components. Anyone citing the scale-homogeneity no-go on real pairs needs this fact as the scale-invariance hypothesis for the target. The proof is short algebraic cancellation: the common factor c^{2} divides out of the ratio once c>0.
Claim. For every $c>0$ and every pair $p=(x,y)\in\mathbb{R}\times\mathbb{R}$, $$\frac{(cx)^2}{(cx)^2+(cy)^2}=\frac{x^2}{x^2+y^2}.$$ Equivalently, the squared first-component share is invariant under the diagonal scaling action $(x,y)\mapsto(cx,cy)$.
background
The module is the boundary theorem of the forced skeleton, in neutral vocabulary. The uniqueness chain (T-2 through T8) derives the skeleton without a scale; this module proves abstractly why the chain cannot go further alone: no selection criterion blind to joint rescaling of a posted value and its carrier can fix an absolute value for a scale-invariant target.
A target functional is scale-invariant when rescaling the carrier leaves its value unchanged: for all $c>0$ and carriers $x$, $f(\mathrm{scale},c,x)=f(x)$. The real-pair witness takes as target the squared first-component share $p_1^2/(p_1^2+p_2^2)$, with the diagonal action that multiplies both components by the same positive constant.
Two ordinary mathematical witnesses (real pairs with this ratio, and eight-component complex vectors with a probability weight) instantiate the hypotheses, so the no-go is a general fact about scale-invariant selection rather than a property of one carrier.
proof idea
Direct term-mode expansion. Introduce $c>0$ and the pair $p$. Rewrite the scaled numerator and the scaled sum of squares by factoring $c^2$ out of each squared term (via ring). Then mul_div_mul_left cancels the common factor $c^2$, which is nonzero because $c>0$ (via pow_ne_zero and ne_of_gt). The unscaled ratio is recovered.
why it matters
Feeds pair_witness, the real-pair instantiation of the no-go: no scale-blind criterion can recover the squared ratio as an absolute posted value. That theorem applies the class doubling-decoy argument with this lemma as the scale-invariance hypothesis on the target, together with joint scale invariance of the positivity selector.
In the Recognition framework this is part of the canonical public form of the boundary theorem from "Recognition Composition and the Forced Skeleton". The uniqueness chain forces the skeleton without a scale; the present fact closes the real-pair instance, showing that at least one scale-bearing input is required before an absolute posted value can be fixed. The ledger instantiation elsewhere is an instance of the same class theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.