pairRatio
plain-language theorem explainer
Squared first-component share of a real pair: r(x,y)=x²/(x²+y²). Canonical scale-invariant target for the joint-selector no-go: any criterion blind to joint rescaling that accepts a witness also accepts a scaled decoy whose posted value misses an absolute target. Pure definition used as the real-pair witness in the boundary theorem.
Claim. For a real pair $(x,y)$, define the squared first-component share $r(x,y) := \frac{x^2}{x^2+y^2}$.
background
ScaleHomogeneityNoGo 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 shows abstractly why the chain cannot fix an absolute value on its own: no selection criterion blind to joint rescaling of a posted value and its carrier can pin a scale-invariant target.
The carrier is any type with a positive-real scaling action. Two ordinary witnesses instantiate the hypotheses: real pairs with a squared ratio, and eight-component complex vectors with a probability weight. The squared ratio is the posted observable on $\mathbb{R}\times\mathbb{R}$: the share of squared mass in the first component.
Joint scaling multiplies both components by the same $\lambda>0$. Under that action the ratio is unchanged (proved in the sibling scale-invariance lemma), so it is a legitimate scale-invariant target for the no-go.
proof idea
One-line definitional abbreviation. Numerator is the square of the first component; denominator is the sum of squares of both components. No lemmas, no tactics.
why it matters
Supplies the concrete scale-invariant observable for the real-pair witness of the joint-selector no-go. Downstream, pairRatio_scaleInvariant records invariance under the pair scale action, and the ratio appears inside RecognitionBridge constructions in OntologyPredicates (the bridge from configurations to positive real intensities).
In the paper framing ("Recognition Composition and the Forced Skeleton"), this is the ordinary-math witness that any joint-scale-invariant selector accepting the intended pair also accepts a doubled decoy, so at least one scale-bearing input is required beyond T0–T8. The ledger form lives elsewhere as an instance; here the definition keeps the public boundary theorem type-agnostic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.