exists_pow_gt_rat
plain-language theorem explainer
For any rational base b > 1 and any rational ceiling c, some natural power b^n exceeds c. The structural ledger cites this Archimedean growth fact when squeezing cut ratios and when proving that a monotone multiplicative character with h(2) > 1 stays at least 1 for all n ≥ 2. The proof is a short Bernoulli comparison after choosing n larger than (c−1)/(b−1).
Claim. Let $b,c\in\mathbb{Q}$ with $b>1$. Then there exists $n\in\mathbb{N}$ such that $c < b^n$.
background
In the Primitive Recognition Calculus native-cost ledger one repeatedly compares geometric sequences of rationals (character values, cut ratios, anchor powers). The classical Archimedean fact that powers of a base strictly larger than one are unbounded above is therefore needed in rational arithmetic, not only over the reals.
The module works with a rational cost character built from the J-cost orbit data (siblings such as jq, nonnegativity and closed-form identities). Growth lemmas of this type let one force contradictions when a monotone multiplicative map is assumed to dip below the unit after an anchor that already exceeds one.
The argument is elementary: Bernoulli’s inequality supplies a linear lower envelope for $(1+x)^n$, which becomes $b^n$ after the substitution $x=b-1>0$.
proof idea
Choose a natural $n$ strictly larger than the rational $(c-1)/(b-1)$ via exists_nat_gt. From $b>1$ one has $b-1>0$, so the division inequality rearranges to $c-1 < n(b-1)$. Bernoulli’s inequality one_add_mul_le_pow gives $1+n(b-1)\le(1+(b-1))^n$. The right-hand side simplifies by ring to $b^n$, and linarith closes $c<b^n$.
why it matters
The lemma is private infrastructure for two ledger results. cut_pins_aux uses it on one side of a cut squeeze: if two geometric families of powers are forced to dominate each other through a pair of rational thresholds $\gamma<\gamma'$, unbounded growth produces a contradiction. The public theorem ge_one then applies the same growth idea to a monotone multiplicative character $h:\mathbb{N}\to\mathbb{Q}$ with $h(2)>1$, showing $h(n)\ge 1$ for all $n\ge 2$ by interpolating an anchor power into any supposed dip below the unit.
Inside Recognition Science this sits in the foundation layer that certifies the native cost is structurally pinned (no cheaper monotone character can undercut the unit once the double-tick anchor exceeds it). It is pure Archimedean arithmetic; it does not itself invoke T5–T8 or the RCL, but it keeps the rational ledger arguments closed without leaving the rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.