exponentOfCharacter
plain-language theorem explainer
Extracts the real multiplicative exponent of a character χ on ratio orbits by reading χ at the orbit of 2 and taking log base 2. Cost and gauge-orbit arguments cite it to turn a real-valued character into a single real power. The body is a direct one-line formula, not a proof.
Claim. For a real-valued map $\chi$ on ratio orbits, define its exponent as $\mathrm{exponent}(\chi) := \log(\chi([2])) / \log 2$, where $[2]$ is the ratio orbit of the natural number $2$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a rational (K4.7). The helper natOrbit n embeds a natural number as that orbit via the rational $n$.
This module studies real-valued characters on those orbits in the anchor-free cost ledger: maps $\chi$ whose values at small bases are rational so an exponent step is well-defined. The surrounding doc frames the corrected factorization target: every inhabitant of that ledger factors through such a character.
The construction sits in the Cost domain, linking functional-equation uniqueness of the native cost to gauge-orbit reductions that need a single real power attached to $\chi$.
proof idea
Pure definition, not a theorem. The body evaluates $\chi$ at the orbit of $2$ and returns $\log(\chi([2]))/\log 2$. No lemmas are applied; noncomputability comes from real logarithm.
why it matters
Gives the scalar power that turns a real character into the exponent step of the corrected factorization target for the anchor-free ledger. Downstream, signGaugeNativeCost_characterExponent_zero rewrites with this definition to prove that the character extracted from the sign-gauge native cost has exponent zero, closing the gauge-orbit reduction for that cost.
In the broader Recognition chain this is bookkeeping for cost uniqueness (T5 J-cost / RCL lineage and PRC native-cost uniqueness imports), not a new physical constant. It lets later arguments treat characters as pure powers without reintroducing anchor data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.