realCharacterCandidate_cost_agrees
plain-language theorem explainer
Under anchor-free native-cost hypotheses, the real value of F at a positive ratio orbit equals the J-cost of the real character extracted from F's doubled trace. Cost and PRC uniqueness arguments cite this when closing real-character factorization. The proof rewrites by the character-trace identity, unfolds the doubled-trace display to rationals, and finishes by ring.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). For every ratio orbit $q$ with $q^{\mathbb{Q}}>0$, the real embedding of $F(q)$ equals $J(\chi_F(q))$, where $\chi_F$ is the real character candidate built from $F$ and $J(x)=(x+x^{-1})/2-1$.
background
This module factors native recognition costs on ratio orbits through real-valued principal characters, without a fixed anchor at two. The cost functional is the classical J-form: costFromRealCharacter sends a real character $\chi$ and orbit $q$ to $(\chi(q)+\chi(q)^{-1})/2-1$, matching the T5 unique cost $J(x)=\cosh(\log x)-1$.
SansAnchorHypotheses F packages the anchor-free structural axioms: base-sans-two, sign-reversing and monotone native cost, and zero-calibrated doubled trace. The doubled trace is displayed in $\mathbb{R}$ by traceDisplay, casting the carrier-valued native doubled trace to a rational then a real. The candidate character realCharacterCandidate F is extracted from that doubled trace (sign character on the degenerate anchor, otherwise the generalized linear extraction).
The immediate upstream identity realCharacterCandidate_trace_of_pos states that for positive $q$, $\chi_F(q)+\chi_F(q)^{-1}$ equals the real doubled-trace display. Integer-rational lemmas (add_toRat, mul_toRat, one_toRat) identify orbit arithmetic with ordinary rational arithmetic after casting.
proof idea
Short term proof. Rewrite the right-hand side by unfolding costFromRealCharacter and applying realCharacterCandidate_trace_of_pos at the positive hypothesis, so the claim becomes equality of $(F q)^{\mathbb{R}}$ with half the doubled-trace display minus one.
Then simp expands traceDisplay, nativeCostDoubledTrace, and doubledTraceValue, pushing through the ratio-orbit arithmetic lemmas (mul_toRat, add_toRat, two_toRat, one_toRat). After push_cast, a single ring closes the rational identity that relates $F(q)$ to the doubled-trace combination $(F(q)+F(q)^{-1})$-style display.
why it matters
This is one of the three legs of SansAnchorRealCharacterFactorizationTarget_proved, which asserts that every anchor-free doubled trace factors through a real-valued principal character: the candidate is a character, its J-cost recovers $F$ on positive orbits (this theorem), and small traces stay rational.
In the Recognition framework it is the concrete cost-agreement step of the real-character factorization of native cost, aligning the orbit-level cost map with the unique J-cost forced at T5 and with the Recognition Composition Law shape $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. It discharges the cost half of the anchor-free factorization target rather than leaving a structural hypothesis open.
Downstream uniqueness and PRC native-cost arguments can therefore quote a proved factorization instead of an interface Prop when working sans anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.