cut_pins
plain-language theorem explainer
Two rationals at or above 1 that transport the same integer-power comparisons against a common reference cut α>1 must be equal. Anyone proving uniqueness of monotone multiplicative characters from a single anchor (the Erdős gauge) cites this. The argument is trichotomy plus a one-sided squeeze that rules out either strict inequality; no analysis enters.
Claim. Let $u,v,\alpha,\gamma,\gamma'\in\mathbb{Q}$ with $\alpha>1$ and $\gamma,\gamma'\ge 1$. Suppose both $\gamma$ and $\gamma'$ preserve the same integer-exponent comparisons against the cut $\alpha$ relative to $(u,v)$: $u^m\le v^n$ implies $\alpha^m\le\gamma^n$ and $\alpha^m\le\gamma'^n$, while $v^n\le u^m$ implies $\gamma^n\le\alpha^m$ and $\gamma'^n\le\alpha^m$. Then $\gamma=\gamma'$.
background
In the primitive recognition calculus, monotone characters on the positive integers are completely multiplicative maps that never vanish and have nondecreasing cost. Uniqueness of such characters is classical Erdős territory: if two of them agree at a single anchor, they agree everywhere. The arithmetic engine that makes the uniqueness go through is a pure comparison squeeze on rational powers, with no logarithms or limits.
The cut lemma isolates that squeeze. Fix a reference pair $(u,v)$ and a cut $\alpha>1$. A rational $\gamma\ge 1$ "transports" the integer-exponent order of $(u,v)$ against $\alpha$ when every comparison $u^m\le v^n$ (resp. the reverse) lifts to $\alpha^m\le\gamma^n$ (resp. the reverse). The claim is that any two such transporters coincide.
The one-sided engine is the private auxiliary: if $\gamma<\gamma'$ and $\gamma$ transports forward while $\gamma'$ transports backward, a contradiction follows by classical arithmetic on rational powers. That auxiliary is the only nontrivial input.
proof idea
Apply trichotomy to $\gamma$ and $\gamma'$. The equality branch is immediate. If $\gamma<\gamma'$, feed the forward transport hypotheses for $\gamma$ and the backward transport hypotheses for $\gamma'$ into the one-sided auxiliary; it returns False. If $\gamma'>\gamma$, swap the roles (forward for $\gamma'$, backward for $\gamma$) and again obtain False from the auxiliary. No further arithmetic is done at this layer; the squeeze lives entirely in the auxiliary.
why it matters
This is the comparison core of the Erdős squeeze inside the PRC native-cost structural ledger. Downstream it is consumed by the gauge theorem: two monotone characters that agree at the single index 2 agree at every positive index, with no logarithm, no limit, and no real analysis, the anchor fixing the whole arithmetic function through the cut squeeze. That gauge is the uniqueness step for monotone multiplicative cost data on the positive integers, which is how recognition cost is pinned once a single calibration value is fixed. In the broader Recognition forcing chain this sits under the native-cost minimality and structural-ledger layer that certifies the J-cost arithmetic before continuum structure is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.