nontrivialCharacterValue
plain-language theorem explainer
Extracts a real-valued character of a ratio-orbit map F at a rational display x by linear extraction of the doubled trace against the principal root of the trace at two. Gauge-orbit classification cites it as the nondegenerate character that becomes a power map on positive rationals and integers. The body is a one-line composition of linear extraction with the rational trace and the anchor root.
Claim. Given a map $F$ on rational orbits and a rational $x$, the nondegenerate character value of $F$ at $x$ is the linear extraction of the doubled rational trace of $F$, using as anchor the principal real root of that trace evaluated at two.
background
In the real character factorization of the cost module, a ratio orbit is an integer-numerator over nonzero orbit-denominator display of a rational. A map $F$ on such orbits induces a doubled trace, packaged as an honest function on rational displays (the rational trace). The value of that trace at the distinguished positive integer two is the anchor; its principal real root is the anchor root.
Linear extraction from a nondegenerate anchor with chosen root $r$ is the map $T \mapsto x \mapsto (r, T(2x) - T(x))/(r^2 - 1)$. It isolates the multiplicative character component of a d'Alembert-type doubled trace. The present definition is exactly that extraction applied to the rational trace of $F$ with $r$ equal to the anchor root of $F$.
The local setting is the nondegenerate branch of real character factorization: the case where the rational trace at two is not equal to two, so the denominator $r^2 - 1$ is nonzero and the extraction is well-defined as a real function of the rational display.
proof idea
Pure definitional composition, not a proof. The body applies linear extraction to the pair (rational trace of $F$, anchor root of $F$) and evaluates at the rational $x$. No tactics, no lemmas beyond the three constituent definitions.
why it matters
This is the working real character used throughout gauge-orbit classification. Downstream, its restriction to positive integers is shown monotone and completely multiplicative, so Erdős-type input yields a natural exponent; that exponent extends by multiplicativity to every positive rational, and the cost on positive displays becomes $J$ of the $k$-th power. The nondegenerate branch is then identified with a sign-extended power native cost.
Sibling lemmas establish multiplicativity and nonvanishing of the extraction under sans-anchor hypotheses and the nondegeneracy side condition (trace at two unequal to two). In the broader Recognition cost story this is the concrete real character that separates the nondegenerate power branch from the degenerate (trace-two) case, feeding the classification that ties ledger cost to the unique $J$-shape forced by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.