char_at_pos
plain-language theorem explainer
Multiplicativity extends a power-law character from the positive integers to every positive rational. Orbit classifiers for the recognition cost cite this when lifting an integer exponent to ℚ₊ under the sans-anchor hypotheses. The proof writes a positive rational as num/den and applies character multiplicativity plus reciprocity, then rearranges.
Claim. Let $F$ be a ratio-orbit map satisfying the sans-anchor hypotheses, with nontrivial rational trace at $2$. Suppose there exists $k\in\mathbb{N}$ such that the nontrivial character value of $F$ on every integer $n\ge 1$ equals $n^k$ in $\mathbb{R}$. Then for every positive rational $x$, that character value equals $x^k$.
background
In the gauge-orbit classification of recognition cost, one studies maps $F$ on ratio orbits and extracts a real-valued character from the rational trace of $F$. The nontrivial character value is the nondegenerate symbolic extraction of that trace at two (via linear extraction against an anchor root). Sans-anchor hypotheses package the structural assumptions needed for that extraction to be multiplicative on nonzero rationals and to invert under reciprocals.
The local setting is Cost.GaugeOrbitClassification: once the character is known on the positive integers as a pure power $n\mapsto n^k$, one must push that law onto all of $\mathbb{Q}_{>0}$ before comparing displays to the $J$-cost. Upstream, multiplicativity (nontrivialCharacterValue_mul) and reciprocity (nontrivialCharacterValue_recip) supply the algebraic skeleton; positivity of the monotone-multiplicative power on naturals is available but used only indirectly through the integer hypothesis.
proof idea
Fix positive $x\in\mathbb{Q}$. Write $x=\mathrm{num}/\mathrm{den}$ with positive integer numerator (via toNat) and positive denominator. Multiplicativity on the product of the numerator with the reciprocal of the denominator, together with reciprocity on the denominator, reduces the character at $x$ to the ratio of the two integer values. The integer power-law hypothesis then replaces each factor by the corresponding $k$-th power. A short rational identity $x^k=(\mathrm{num})^k/(\mathrm{den})^k$ and a cast/ring cleanup finish the equality in $\mathbb{R}$.
why it matters
This lemma is the bridge from integer exponents to rational displays inside the gauge-orbit classification. Its sole direct consumer is cost_at_pos, whose doc-comment states: on a positive display the cost is $J$ of the $k$-th power. That parent theorem converts the character identity into an equality of orbit representatives with $J(q^k)$, which is the form needed to match the recognition cost functional.
In the broader RS forcing picture, characters of this shape are the discrete avatars of the unique $J$-cost (T5) on multiplicative ratios; extending the power law to $\mathbb{Q}_{>0}$ keeps the classification free of ad-hoc anchors and feeds the later dichotomy between degenerate (sign-gauge) and nontrivial (signed-power) orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.