realCharacterCandidate_trace_of_pos
plain-language theorem explainer
On positive ratio orbits, the real character candidate extracted from a native cost map F satisfies χ(q) + χ(q)⁻¹ equal to the doubled-trace display of F at q. Cost-factorization arguments cite this to rebuild the native cost from the character. The proof case-splits on whether the doubled trace is degenerate at 2, then applies the trivial-constant or nontrivial-extraction identity.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base without the two-anchor, sign-reversing, monotone, zero-calibrated doubled trace). For every ratio orbit $q$ with positive rational display, if $\chi_F(q)$ denotes the real character candidate of $F$ at $q$, then $\chi_F(q) + \chi_F(q)^{-1}$ equals the doubled-trace display of $F$ at $q$.
background
The module builds a real multiplicative character from the doubled trace of a native recognition cost on ratio orbits. The doubled trace is the real-valued display of $F(q)\cdot F(q)^{-1}$-type data; rationalTrace evaluates that display on rational inputs via the orbit-of-rational embedding, and under the anchor-free pack it agrees with traceDisplay on every orbit.
SansAnchorHypotheses packages the structural native-cost axioms without fixing the two-anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. From those axioms one extracts realCharacterCandidate: if the doubled trace at 2 equals 2 (degenerate anchor), the candidate is the rational sign character; otherwise it is the generalized linear root of the nontrivial character value (with a zero clause at the zero rational).
Upstream, positivity forces the sign character to 1, and if the doubled trace is constantly 2 at the anchor then it is constantly 2 on all positive rationals. In the nontrivial branch, nontrivialCharacterValue_trace already states that the extracted value plus its inverse recovers the doubled trace.
proof idea
From $0 < q.\mathrm{toRat}$ deduce $q.\mathrm{toRat}\neq 0$. Record rationalTrace_eq_traceDisplay so the rational doubled trace matches the orbit display.
Case on whether rationalTrace F 2 = 2.
Degenerate branch: rationalTrace_pos_eq_two_of_two_eq_two forces the rational trace (hence the display) to equal 2. Unfold the candidate via the positive branch of the if, replace by rationalSignCharacter_of_pos (value 1), and finish by $1+1^{-1}=2$.
Nondegenerate branch: unfold the candidate on the nontrivial, nonzero arm and rewrite by nontrivialCharacterValue_trace, then match the display via the recorded equality.
why it matters
This is the bridge from doubled-trace data to a genuine real character on positive orbits. Immediately downstream, realCharacterCandidate_cost_agrees rewrites the native cost of $F$ as costFromRealCharacter of the candidate, using this identity as the first step. The companion realCharacterCandidate_small_traces_rational uses it to pin small integer-orbit traces to rational values.
In the Recognition framework this sits inside the cost-uniqueness lane feeding T5 (J-uniqueness of $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law: recovering cost from a character whose sum-with-inverse is the doubled trace is exactly the d'Alembert/cosh shape of $J$. Closing the candidate-to-cost agreement is what lets native PRC costs be identified with the unique RS cost functional without an external two-anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.