nativeCostDoubledTrace
plain-language theorem explainer
Defines the doubled d'Alembert trace of a native cost map F at a rational orbit q by T_F(q)=2(F(q)+1). For costs generated by a multiplicative character this equals χ(q)+χ(q)^{-1}. Cost and gauge-orbit modules cite it as the bridge from native cost values to trace displays. The body is a one-line wrapper around the scalar map a ↦ 2(a+1).
Claim. Given a map $F$ on rational orbits and an orbit $q$, the doubled d'Alembert trace is $T_F(q) := 2\bigl(F(q)+1\bigr)$. When $F$ is generated by a multiplicative character $\chi$, one has $T_F(q)=\chi(q)+\chi(q)^{-1}$.
background
In the primitive recognition calculus, costs act on RatioOrbit objects: rational displays with a signed-orbit numerator and a nonzero distinction-orbit denominator. A native cost is a map $F$ from orbits to orbits satisfying the Recognition Composition Law (RCL) package and related calibration hypotheses.
The scalar helper doubledTraceValue sends a cost value $a$ to $2(a+1)$. Composing it with $F$ produces the doubled d'Alembert trace $T_F$. The classical d'Alembert (cosine) functional equation is the natural home for traces of the form $\chi+\chi^{-1}$; the factor of two and the shift by one convert the RS native cost normalization (tied to the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ from forcing step T5) into that additive-trace scale.
The surrounding module develops uniqueness of native costs via character factorization and monotone d'Alembert analysis on these rational orbits.
proof idea
Pure definitional wrapper: evaluate $F$ at $q$, then apply doubledTraceValue, which is itself RatioOrbit.mul two (RatioOrbit.add a RatioOrbit.one). No lemmas or tactics.
why it matters
This is the standard conversion from native cost values to the doubled-trace language used throughout the Cost layer. Downstream, cost_display recovers the cost as half the rational trace minus one; doubledTrace_dAlembert_of_native (and the RCL / sans-anchor variants) prove that $T_F$ obeys the d'Alembert cross identity when $F$ satisfies the native-cost hypotheses. Gauge-orbit constructions (signedPowerNativeCost, signGaugeNativeCost) calibrate zero and anchor values through this same display.
In the Recognition framework it sits on the path from RCL and $J$-uniqueness (T5) to character factorization of costs on rational orbits, which feeds gauge-orbit classification and the existence of integer exponents for nontrivial characters. It does not itself force $\phi$ or the eight-tick structure; it only packages the trace that those uniqueness arguments manipulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.