nontrivialCharacterValue_mul
plain-language theorem explainer
Under anchor-free native-cost hypotheses, the nontrivial character extracted from the doubled rational trace is completely multiplicative on nonzero rationals, provided the trace at 2 is nondegenerate. Orbit-classification and Erdős-uniqueness arguments cite this as the bridge from the d'Alembert identity to a genuine character. The proof is a direct term application of the general linear-extraction multiplicativity lemma.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace), and suppose the doubled rational trace of $F$ at $2$ is not $2$. Then for all nonzero rationals $x,y$, the nontrivial character value of $F$ at $xy$ equals the product of its values at $x$ and at $y$.
background
In the real-character factorization of native cost, one starts from a map $F$ on ratio orbits obeying the anchor-free pack SansAnchorHypotheses: base-sans-two structure, sign-reversing and monotone native-cost axioms, and a zero-calibrated doubled trace. The doubled trace is reified as an honest function rationalTrace F on rational displays via the orbit of each rational.
When that trace at $2$ is nondegenerate (not equal to $2$), one extracts a real root anchorRoot F of the associated quadratic and forms the linear extraction nontrivialCharacterValue F x, the nondegenerate symbolic character read off the trace at two. Upstream, the trace is reciprocal and satisfies the d'Alembert identity $T(xy)+T(x/y)=T(x)T(y)$ on nonzero rationals; the anchor root is nonzero, has square not equal to one, and sums with its inverse to the trace at two.
The local setting is the cost module that factors real characters from PRC-native cost uniqueness, preparing the integer restriction for monotone-multiplicative classification.
proof idea
One-line term proof: apply the private lemma linearExtraction_multiplicative to $T:=$ rationalTrace $F$ and $r:=$ anchorRoot $F$. The five side conditions are discharged by rationalTrace_recip, rationalTrace_dAlembert, anchorRoot_ne_zero, anchorRoot_sq_sub_one_ne_zero (using nondegeneracy of the trace at $2$), and anchorRoot_add_inv, together with the nonzero hypotheses on $x$ and $y$. No further rewriting is needed; the character is defined as that linear extraction.
why it matters
Complete multiplicativity is the algebraic engine that turns the extracted real value into a genuine character on $\mathbb{Q}^\times$. Downstream it feeds nontrivialCharacterValue_recip, _pow, _nonzero, and _principal_on_nat inside the same module, and the candidate multiplicativity realCharacterCandidate_mul.
In GaugeOrbitClassification it is the mul field of natChar_monotoneMultiplicative, which packages the integer restriction as a monotone completely multiplicative map so Erdős's theorem applies, and it carries power laws from $\mathbb{N}$ to every positive rational in char_at_pos ("Multiplicativity carries the power law from the integers to every positive rational").
Within Recognition Science this sits in the cost layer that isolates the unique native cost functional (linked to J-uniqueness / T5 and the Recognition Composition Law): once the character is multiplicative and monotone on naturals, the gauge orbit is forced to a pure power, closing the real-factorization route to the cost uniqueness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.