pow
plain-language theorem explainer
A monotone completely multiplicative character on the positive integers is a pure power map: h(a^k) equals h(a)^k whenever a ≥ 1. Anyone working with discrete cost characters, gauge classification, or the structural ledger of native PRC costs will cite this. The proof is a short induction on the exponent, using the unit and multiplicativity axioms of MonoMult.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, nowhere zero on $n\ge 1$, with $h(1)=1$, and with nondecreasing cost under the native $J$-cost character. Then for every $a,k\in\mathbb{N}$ with $a\ge 1$, one has $h(a^k)=h(a)^k$.
background
In the primitive recognition calculus, discrete cost data on the positive integers is packaged as a MonoMult character: a map $h:\mathbb{N}\to\mathbb{Q}$ that is nowhere zero for $n\ge 1$, sends $1$ to $1$, is completely multiplicative on arguments at least one, and is monotone after composition with the native cost character $jq$ (the discrete avatar of the $J$-cost $J(x)=(x+x^{-1})/2-1$).
The module builds a structural ledger of what such characters can and cannot do before any continuum analysis. Multiplicativity alone already forces $h$ on products; the present statement extends that to pure powers. Upstream, the same ledger uses the shifted cost $H(x)=J(x)+1$, under which the Recognition Composition Law becomes d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$, linking discrete characters to the continuous uniqueness theory for $J$.
proof idea
Induction on the exponent $k$. The zero case is $a^0=1$, so $h(a^0)=h(1)=1=h(a)^0$ by the unit axiom of MonoMult (via simpa). For the successor step, write $a^{k+1}=a^k\cdot a$. The lower bound $1\le a^k$ follows from $a\ge 1$ and the standard natural-number power inequality. Multiplicativity then gives $h(a^{k+1})=h(a^k)\cdot h(a)$; the inductive hypothesis replaces $h(a^k)$ by $h(a)^k$, and the rational power successor identity finishes the rewrite.
why it matters
This is a basic structural fact in the PRC native-cost ledger: once a character is MonoMult, its values on pure powers are completely determined by the value at the base. Downstream it feeds ge_one in the same module (monotonicity rules out negative values above the unit) and is reused across the cost stack: Aczél uniqueness and classification bridges (ode_neg_zero_uniqueness, aczel_classification_conditional), rational-trace exponent control (int_of_rat_exponent_of_trace_rat, no_rational_sqrt_five), and energy identities in the action layer.
In the forcing chain this sits under the discrete side of T5 $J$-uniqueness and the RCL: power-multiplicativity is the integer skeleton that continuous d'Alembert solutions must match when restricted to rational characters. Without it, gauge and exponent classification steps that compare $h(a^k)$ to $h(a)^k$ would have no algebraic footing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.