cut_pins_aux
plain-language theorem explainer
If two rational thresholds γ < γ' both sit at least at 1, and a common reference α > 1 transports the same integer-power comparisons of a pair (u,v) forward into γ and backward into γ', a contradiction follows. Anyone citing the cut lemma (Erdős-style squeeze for rational cost thresholds) needs this one-sided impossibility. The proof is pure Archimedean growth plus a minimal-exponent case split; no analysis.
Claim. Let $u,v,\alpha,\gamma,\gamma'\in\mathbb{Q}$ with $\alpha>1$, $\gamma\ge 1$, and $\gamma<\gamma'$. Suppose that for all $m,n\in\mathbb{N}$, $u^m\le v^n$ implies $\alpha^m\le\gamma^n$, and $v^n\le u^m$ implies $\gamma'^n\le\alpha^m$. Then a contradiction.
background
In the Primitive Recognition Calculus native-cost ledger, cost thresholds are rational and comparisons are transported only through integer exponents. The cut lemma asserts that two such thresholds which induce identical forward and backward comparisons against a fixed reference cut $\alpha$ must coincide. This auxiliary lemma is the strict-inequality half of that squeeze.
The only growth engine is exists_pow_gt_rat: for $b>1$ and any rational $c$ there is $n$ with $c<b^n$, proved from Bernoulli's inequality. Positivity of powers of $\gamma$ and $\alpha$ follows from $\gamma\ge 1$ and $\alpha>1$. The case split on $u^m$ versus $v^n$ uses totality of $\le$ on the rationals (via the integer-order totality pattern already present in the PRC stack).
The module sits under the native-cost minimality certificate import chain; the goal is an analysis-free identification of cost cuts by pure comparison transport.
proof idea
Classical mode. From $\gamma\ge 1$ and $\alpha>1$ get positivity, hence $1<\gamma'/\gamma$. Apply exists_pow_gt_rat to obtain $n$ with $\alpha<(\gamma'/\gamma)^n$, rewritten as $\alpha\cdot\gamma^n<\gamma'^n$.
Again by Archimedean growth, take the least $m$ with $\gamma^n<\alpha^m$. Minimality forces $m\ne 0$, write $m=j+1$, and obtain $\alpha^j\le\gamma^n$, so $\alpha^m\le\alpha\cdot\gamma^n<\gamma'^n$.
By totality, either $u^m\le v^n$ or $v^n\le u^m$. The first with the forward hypothesis yields $\alpha^m\le\gamma^n$, contradicting $\gamma^n<\alpha^m$. The second with the backward hypothesis yields $\gamma'^n\le\alpha^m$, contradicting $\alpha^m<\gamma'^n$.
why it matters
Feeds directly into cut_pins, the cut lemma: two rationals at or above the unit that transport the same integer-exponent comparisons against a common reference cut are equal. The parent doc-comment calls that "the whole of the Erdős squeeze, and there is no analysis in it."
This auxiliary supplies the one-sided impossibility $\gamma<\gamma'\Rightarrow\bot$ under mixed forward/backward transport; the parent theorem runs the symmetric argument (or both directions) to force equality. Inside Recognition Science the cut lemma pins native cost thresholds on the rational ledger without real-analytic limits, keeping the structural cost certificate fully discrete and aligned with the forcing-chain style of T5–T8 (uniqueness by algebraic comparison, not continuum analysis).
No open scaffold remains: the lemma is fully proved and private to the ledger module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.