doubledTraceValue
plain-language theorem explainer
The doubled trace map sends a cost value $a$ on a ratio orbit to the orbit $2(a+1)$. It is the native discrete form of the d'Alembert trace $T_F(q)=2(F(q)+1)$, which for generated costs equals $\chi(q)+\chi(q)^{-1}$. Cost and gauge-orbit modules cite it when relating native costs to character traces. The body is a one-line product of the constant two with the shifted orbit $a+1$.
Claim. For a ratio orbit $a$, define the doubled trace value as the ratio orbit $2(a+1)$, i.e. the product of the constant orbit $2$ with the sum of $a$ and the unit orbit $1$.
background
In the Primitive Recognition Calculus, costs and characters take values in RatioOrbit: an integer numerator over a nonzero orbit denominator (K4.7). Arithmetic on orbits is native; the constant orbit $2$ is the ratio with numerator the orbit of two and denominator one.
Native costs $F$ on ratio orbits induce a doubled d'Alembert trace $T_F(q)=2(F(q)+1)$. The module comment records that for a generated cost this coincides with the character sum $\chi(q)+\chi(q)^{-1}$. That identification is the bridge from discrete cost data to real-character factorization and the Recognition Composition Law (RCL).
Upstream, the constant two and the orbit type are supplied by the PRC J-cost and IntegerRational layers; various engine cost maps (observer J-cost, multiplicative recognizer cost, rung-coarsen weights) are the continuous cousins of the same $F$.
proof idea
Pure definition: multiply the constant orbit two by the sum of the input orbit $a$ and the unit orbit. No lemmas, no tactics; the body is the term RatioOrbit.mul two (RatioOrbit.add a RatioOrbit.one).
why it matters
This is the discrete carrier of the doubled d'Alembert trace used throughout Cost. GaugeOrbitClassification rewrites cost display as half the rational trace minus one by unfolding this map. GaugeOrbitFromRealCharacter uses it to calibrate zero and to check that the sign-gauge native cost has rational trace two at the anchor. RealCharacterFactorization builds the doubled-trace form of the RCL and the monotone rational-trace extraction on top of it.
In the Recognition forcing chain the uniqueness of $J$ (T5) and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ are the continuous targets; the doubled trace is the native object that matches $\chi+\chi^{-1}$ and feeds those uniqueness arguments once the character hypotheses are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.