transfer_le
plain-language theorem explainer
If a monotone completely multiplicative character h on the positives satisfies h(2)>1, then integer power inequalities 2^m ≤ n^k transfer to the character values: (h 2)^m ≤ (h n)^k for every n≥2. Cited by anyone squeezing two such characters against a common anchor at 2. The proof pushes the base inequality through mono and pow, then reflects the jq-order back to the values via ge_one.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, nowhere zero on $\mathbb{N}_{\ge 1}$, with $h(1)=1$, and with nondecreasing cost $jq\circ h$. Suppose $h(2)>1$. Then for every integer $n\ge 2$ and all $m,k\in\mathbb{N}$, $$2^m\le n^k \implies (h(2))^m\le (h(n))^k.$$
background
The ambient object is a monotone character on the positive integers: a map $h:\mathbb{N}\to\mathbb{Q}$ that is completely multiplicative, satisfies $h(1)=1$ and $h(n)\ne 0$ for $n\ge 1$, and whose cost $jq(h(\cdot))$ is nondecreasing. That package is the structure MonoMult. The cost $jq$ is the rational avatar of the Recognition cost; on the half-line at or above the unit it is strictly monotone, so order on costs reflects order on values (jq_le_reflect).
A basic consequence of monotonicity plus the anchor $h(2)>1$ is that $h$ stays at least $1$ on every integer $n\ge 2$ (ge_one): if some value dipped below the unit, a larger integer would cost less than $2$, contradicting mono. Completely multiplicative characters also obey the power rule $h(a^k)=(h a)^k$ for $a\ge 1$ (MonoMult.pow).
The local module builds the structural ledger for the primitive recognition calculus native cost: arithmetic constraints that any monotone character must satisfy before the gauge uniqueness theorem can fire.
proof idea
Cast the rational power inequality $2^m\le n^k$ to naturals. Apply MonoMult.mono between $2^m$ and $n^k$ (the left base is at least $1$) to obtain $jq(h(2^m))\le jq(h(n^k))$. Rewrite both sides by MonoMult.pow, yielding $jq((h 2)^m)\le jq((h n)^k)$. Both bases sit at least at $1$: $(h 2)^m$ by $h(2)>1$ and one_le_pow₀, and $(h n)^k$ by ge_one plus one_le_pow₀. Order reflection jq_le_reflect then drops the $jq$ and returns $(h 2)^m\le (h n)^k$.
why it matters
This is the cut-transfer step that feeds the gauge theorem monoMult_gauge (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. The gauge theorem's doc-comment states the mechanism explicitly: "the anchor value fixes the whole arithmetic function through the cut squeeze." Transfer supplies one side of that squeeze: whenever a pure power of $2$ sits below a pure power of $n$, the same inequality holds after applying $h$.
In the Recognition Science forcing chain this sits inside the primitive recognition calculus ledger that constrains admissible cost characters before J-uniqueness (T5) and the self-similar fixed point $\varphi$ (T6) are imposed. It is pure arithmetic structure on $\mathbb{N}$, not yet the continuum functional equation, but it is the discrete skeleton that later forces the character to be a pure power of the anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.