quadrant_ratio_scaleInvariant
plain-language theorem explainer
Scaling any positive-quadrant pair by a positive real leaves the coordinate ratio unchanged. The AmplitudeForm half of the scale-homogeneity no-go uses this when the scale-invariant target is the ratio of the two coordinates. Proof is pure cancellation of the common positive factor via the field identity mul_div_mul_left.
Claim. For every $c > 0$ and every point $p = (a,b)$ in the open positive quadrant $\{(x,y)\in\mathbb{R}^2 : x>0,\, y>0\}$, the scaled point $(ca, cb)$ satisfies $\frac{ca}{cb} = \frac{a}{b}$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton. The uniqueness chain (T-2 through T8) derives the theory without a scale; this module shows, abstractly, that 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 such criterion that accepts the intended witness also accepts a doubled decoy.
AmplitudeForm packages the paper's S5 statement: over a scaled configuration space (a $\mathbb{R}_{>0}$-action with a degree-one homogeneous amplitude), an invariant selector's selected amplitude set is contained in ${0}$ or contains every positive real. The positive quadrant is the concrete witness carrier: pairs $(a,b)$ with $a>0$, $b>0$, scaled by multiplying both coordinates by $c>0$, with the first coordinate as amplitude. The scale-invariant observable of interest is the ratio $a/b$.
The quadrant scaled configuration space records that this action is free and associative on the positive orthant, which is exactly the carrier used to pin the ratio while leaving amplitude free.
proof idea
Unfold the quadrant scale action: the image of $p=(a,b)$ under scale by $c$ is $(c\cdot a,, c\cdot b)$. The goal reduces to $(ca)/(cb)=a/b$. Discharge by the standard real-field identity that cancels a common nonzero left factor in a quotient (mul_div_mul_left), using $c\neq 0$ from positivity of $c$. One algebraic step; no cases or induction.
why it matters
Elementary ratio invariance is the step that makes the positive-quadrant target scale-invariant inside AmplitudeForm of ScaleHomogeneityNoGo, the canonical public form of the boundary theorem from the paper "Recognition Composition and the Forced Skeleton". AmplitudeForm states S5: an invariant selector on a scaled configuration space with degree-one homogeneous amplitude either selects only amplitude $0$ or every positive amplitude; the quadrant witness pins the ratio $a/b$ (classically to $2$) while leaving amplitude free.
In the broader framework this sits at the edge of the forcing chain T0–T8: after the skeleton is forced without a scale, at least one scale-bearing input is required. The ledger instantiation lives elsewhere as an instance of the class theorem proved in this module. No downstream dependents are recorded for this particular lemma; it is local support for the AmplitudeForm packaging of the no-go.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.