exists_pow_trace_decrease
plain-language theorem explainer
For 0 < u < 1 and r > 1 there is a power k with T(r u^k) < T(u^k), where T(x) = x + x^{-1} is the doubled multiplicative trace. Cost and character-factorization arguments cite it to force high powers of a sub-unit base below the unit level of the trace. The proof picks k so that (u^2)^k < r^{-1}, then reads the sign of T(rv) - T(v) from a short algebraic identity.
Claim. Let $u,r \in \mathbb{R}$ satisfy $0 < u < 1$ and $r > 1$. Then there exists $k \in \mathbb{N}$ such that $$r\,u^k + (r\,u^k)^{-1} < u^k + (u^k)^{-1}.$$
background
The ambient module develops real character factorizations of Recognition cost. The doubled trace $T(x) := x + x^{-1}$ (for $x > 0$) is the raw form behind the J-cost $J(x) = (x + x^{-1})/2 - 1$ forced at T5; siblings such as doubledTrace_dAlembert_of_rcl record that $T$ obeys the d'Alembert / RCL functional equation coming from the Recognition Composition Law.
Here one compares $T$ at a scaled point $r v$ against $T$ at $v$, with $v = u^k$ a high power of a base strictly inside the unit interval. Because $T(x) = T(x^{-1})$ and $T$ has a global minimum at $x = 1$ with $T(1) = 2$, any factor $r > 1$ pushes the argument away from 1 only when the base power has not yet been driven small enough; the lemma guarantees a power at which the opposite happens.
The local setting is the real-ratio character calculus used to classify cost functionals without an a-priori anchor (SansAnchorHypotheses), feeding uniqueness results imported from PRCNativeCostUniqueness.
proof idea
From $0 < u < 1$ one has $0 < u^2 < 1$, and $r > 1$ gives $r > 0$ and $r^{-1} > 0$. Apply exists_pow_lt_of_lt_one to obtain $k$ with $(u^2)^k < r^{-1}$. Set $v := u^k > 0$, so $v^2 < r^{-1}$ and therefore $r v^2 < 1$.
Clear denominators to get the identity
$(r v)\bigl(T(r v) - T(v)\bigr) = (r-1)(r v^2 - 1)$.
The right-hand side is negative ($r-1 > 0$ and $r v^2 - 1 < 0$). The prefactor $r v$ is positive, so $T(r v) - T(v) < 0$, which is the claim. The algebra is discharged by field_simp/ring; the final sign chase uses nlinarith.
why it matters
The sole recorded consumer is nontrivialCharacterValue_principal_on_nat: under SansAnchorHypotheses, if the rational trace at 2 is nontrivial ($\neq 2$), then the nontrivial character value on every natural $n \ge 1$ is at least 1. That lower bound needs a power at which scaling by $r > 1$ strictly decreases the doubled trace; this lemma supplies exactly that decrease.
In the broader Recognition chain the result is a real-analytic support lemma for J-uniqueness (T5) and the RCL-driven classification of cost: once high powers of a sub-unit base can be forced into the decreasing regime of $T$, character values cannot drift below the principal level, which pins native cost uniqueness on the positive reals. It does not itself force $\varphi$ or the eight-tick structure; those enter through the surrounding factorization and forcing-chain modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.