nontrivialCharacterValue_pow
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the nondegenerate real character extracted from the doubled trace is a monoid homomorphism on nonzero rationals, so it preserves natural powers: χ(x^k)=χ(x)^k. Used when bounding the character on positive integers or proving it is principal on ℕ. Proof is induction on the exponent, reducing the successor step to multiplicativity and the base to the unit lemma.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses, and suppose the doubled rational trace of $F$ at $2$ is not equal to $2$. Write $\chi_F$ for the nondegenerate real character extracted from that trace. Then for every nonzero rational $x$ and every natural number $k$, $$\chi_F(x^k)=\chi_F(x)^k.$$
background
In the real-character factorization of native cost, one starts from a map $F$ on ratio orbits and forms its doubled trace on rational displays (rationalTrace). The pack SansAnchorHypotheses collects the anchor-free structural axioms: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. These match the PRC structural native-cost hypotheses without an external anchor.
When the trace at $2$ is nondegenerate (rationalTrace F 2 ≠ 2), one extracts a real-valued character $\chi_F$ by linear extraction against the anchor root of $F$. By construction $\chi_F$ is the nondegenerate symbolic value of the trace at two. Multiplicativity $\chi_F(xy)=\chi_F(x)\chi_F(y)$ on nonzero rationals and the unit identity $\chi_F(1)=1$ are already proved under the same hypotheses.
The present statement lifts those two facts to natural powers, which is the standard monoid-homomorphism consequence on $(\mathbb{Q}^\times,\cdot)$.
proof idea
Fix nonzero $x$ and induct on $k:\mathbb{N}$.
Base $k=0$: $x^0=1$, so the claim is $\chi_F(1)=1$, which is exactly nontrivialCharacterValue_one under the same hypotheses.
Successor: rewrite $x^{k+1}=x^k\cdot x$ and apply nontrivialCharacterValue_mul (using $x^k\neq 0$ from pow_ne_zero and $x\neq 0$). The inductive hypothesis replaces $\chi_F(x^k)$ by $\chi_F(x)^k$, and pow_succ on the real side finishes the equality.
why it matters
This is the power-homomorphism step in the real-character package for native cost. Downstream, nontrivialCharacterValue_principal_on_nat uses it to show $\chi_F(n)\ge 1$ for every natural $n\ge 1$, which is the principal-character bound on positive integers.
In the broader Recognition Science cost story, the nondegenerate character is the bridge from the Recognition Composition Law / native-cost uniqueness (PRC) to a concrete real multiplicative functional on ratio orbits. Power preservation is the elementary algebraic fact needed before comparing ladder rungs, integer displays, or positivity along the $\varphi$-ladder. It does not itself force $J$-uniqueness (T5) or $\varphi$, but it is part of the cost-side factorization that those landmarks sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.