traceRootCandidate
plain-language theorem explainer
Given a doubled-trace map T on rational orbits, the linear root candidate recovers the putative character by χ(q)=(2·T(2q)−T(q))/3 for q≠0, and returns zero at the origin. Anyone extracting a multiplicative character from a split trace on the axis 2 cites this formula. It is a pure arithmetic construction on ratio orbits, with fixed denominator orbit 3.
Claim. For a map $T$ on rational orbits and an orbit $q$, set the linear root candidate to $0$ when the rational display of $q$ is zero; otherwise set it equal to $(2\cdot T(2q)-T(q))/3$, where $2$ is the distinguished ratio orbit and the denominator $3$ is the orbit $2+1$.
background
In the Primitive Recognition Calculus, costs and characters live on RatioOrbit: integer numerator over a nonzero distinction-nat denominator, with a verifier display toRat into $\mathbb{Q}$. The reciprocal is total, sending zero to zero as in the rationals. The constant orbit two is the ratio $2/1$; traceRootDenominator is the orbit $3=2+1$.
The ambient problem is native-cost uniqueness: a doubled-trace map $T$ is meant to equal $\chi+\chi^{-1}$ for a multiplicative character $\chi$ normalized so that $\chi(2)=2$. Under that ansatz the linear algebra of the split at the axis $2$ forces the closed extraction $\chi(q)=(2T(2q)-T(q))/3$. The zero case is handled by the repaired zero-calibration field rather than by division.
This definition sits in the PRC native-cost uniqueness module, which builds the doubled-trace hypotheses, d'Alembert structure, and character-matching targets used to force the unique native cost (the RS $J$-cost lineage).
proof idea
Pure definition by cases. If the rational display of $q$ is zero, return the zero orbit. Otherwise form the numerator orbit $2\cdot T(2q)-T(q)$ by orbit multiplication and subtraction, then multiply on the right by the total reciprocal of the fixed denominator orbit $3$. No lemmas are invoked; the arithmetic is the formula stated in the doc-comment.
why it matters
This extractor is the concrete witness fed to the linear-root and coherent-root targets. Downstream, PRCDoubledTraceLinearRootCandidateWorks packages that the candidate is a ratio character whose doubled trace recovers $T$; PRCDoubledTraceZeroCalibratedCoherentRootTarget_of_linear_root lifts a linear-root solution to a coherent root by returning exactly this candidate. Multiplicativity, normalization, and non-vanishing lemmas (traceRootCandidate_multiplicative_of_trace_respect, _one_of_trace_respect, _normalized_of_trace_respect, _nonzero_of_quadratic) all quantify over it.
In the broader RS chain this is local infrastructure for uniqueness of the native cost functional, the PRC avatar of T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$). Structural-ledger results such as cubeGeneratedNativeCost_two_not_canonical sit in the same uniqueness campaign: only the genuine character-derived cost survives the axis-$2$ constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.