transfer_ge
plain-language theorem explainer
If a monotone completely multiplicative character h satisfies h(2)>1 and the integer inequality n^k ≤ 2^m holds for n≥2, then the same power inequality transfers to the character: (h n)^k ≤ (h 2)^m. Cited by the gauge uniqueness theorem for MonoMult characters. Proof casts the base inequality, applies cost monotonicity on powers, rewrites by complete multiplicativity, and reflects through the J-cost comparison.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative with $h(1)=1$, nowhere zero on positive integers, and with nondecreasing cost $J\circ h$. If $h(2)>1$, $n\ge 2$, and $n^k\le 2^m$ in $\mathbb{Q}$, then $(h(n))^k\le (h(2))^m$.
background
The module builds a structural ledger for native recognition cost on positive integers. A MonoMult character is arithmetic data left by a monotone multiplicative recognizer: completely multiplicative, $h(1)=1$, nowhere zero for $n\ge 1$, and nondecreasing in the cost functional $jq\circ h$. Here $jq$ is the rational avatar of the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $H(x)-1$ with $H(x)=\tfrac12(x+x^{-1})$), the unique cost forced by the Recognition Composition Law.
The hypothesis $h(2)>1$ anchors the character away from the degenerate sign/unit gauge. Complete multiplicativity supplies $h(n^k)=(h n)^k$ and $h(2^m)=(h 2)^m$, so integer power comparisons can be pushed through $h$ once cost monotonicity is available. Upstream cost infrastructure ($H$, derived recognizer costs, observer J-cost) supplies the same comparison geometry used here on $\mathbb{Q}$.
proof idea
Cast $n^k\le 2^m$ from $\mathbb{Q}$ to $\mathbb{N}$. Apply MonoMult.mono to the pair $(n^k,2^m)$ (using $1\le n^k$) to obtain $jq(h(n^k))\le jq(h(2^m))$. Rewrite both sides by the structure's power law H.pow, yielding $jq((h n)^k)\le jq((h 2)^m)$. Finish with jq_le_reflect, feeding nonnegativity/lower bounds from ge_one (so $(h n)^k\ge 1$ and $(h 2)^m\ge 1$) to recover the raw rational inequality $(h n)^k\le (h 2)^m$.
why it matters
This is the cut-transfer step inside the structural ledger for primitive recognition cost. Downstream it is consumed by monoMult_gauge, the gauge theorem (Erdős 1946, completely multiplicative case): two monotone characters that agree at the single index 2 agree at every positive index, with no logarithms or limits, only the anchor and the cut squeeze.
In Recognition Science terms, the result rigidifies the discrete arithmetic shadow of the unique J-cost (T5) before continuum limits appear. It keeps the native cost ledger on $\mathbb{N}$ aligned with the forced cost functional, so later uniqueness and minimality certificates for PRC native cost can treat the value at 2 as a complete gauge fix for the whole character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.