realCharacterCandidate_small_traces_rational
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real character candidate on the integer orbits n = 2,3,4,5 has doubled value χ(n)+χ(n)⁻¹ equal to a rational real. Anyone assembling the Sans-anchor real-character factorization target cites this finite check. The proof is a one-line extraction: the doubled-trace display is already rational, and the positive-orbit trace identity identifies it with χ+χ⁻¹.
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). Then for every natural number $n$ with $2 \le n \le 5$, there exists a rational $t$ such that $\chi_F(n) + \chi_F(n)^{-1} = t$ as reals, where $\chi_F$ is the real character candidate extracted from the doubled trace of $F$ and $n$ is viewed as its positive rational orbit.
background
This module builds a real-valued multiplicative character from an anchor-free native cost on ratio orbits. Ratio orbits are equivalence classes of nonzero rationals under the integer-rational identification; natOrbit n is simply the orbit of the positive integer $n$, with toRat recovering $n$ itself.
The pack SansAnchorHypotheses collects four structural axioms on $F$: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. From that pack one extracts a real character candidate $\chi_F$: on the degenerate branch it is the rational sign character; otherwise a generalized linear extraction from the doubled trace is used.
Upstream, realCharacterCandidate_trace_of_pos already identifies $\chi_F(q)+\chi_F(q)^{-1}$ with the doubled-trace display whenever $q$ has positive rational representative. The present lemma only needs that identity on the five small positive integer orbits $n=2,\ldots,5$, together with the fact that the native doubled trace lands in a type that exposes a rational toRat.
proof idea
Term-mode, essentially a one-line wrapper. Introduce $n$ with $2\le n\le 5$. Witness the existential by the rational (nativeCostDoubledTrace F (natOrbit n)).toRat. Discharge the equality by realCharacterCandidate_trace_of_pos under the Sans-anchor pack, using positivity of the orbit: rewrite via natOrbit_toRat and cast $0<n$ (from $n\ge 2$). The upper bound $n\le 5$ is unused in the body; it only scopes the finite check demanded by the factorization target.
why it matters
Feeds directly into SansAnchorRealCharacterFactorizationTarget_proved, whose doc-comment states: "The anchor-free doubled trace always factors through a real-valued principal character." That parent packages four obligations; this lemma discharges the small-traces-rational clause for $n=2,\ldots,5$.
In the Recognition framework the native cost is forced toward the unique $J$-cost of T5 ($J(x)=(x+x^{-1})/2-1$), and character factorization of the doubled trace is the bridge from structural cost axioms to a real multiplicative character on ratio orbits. The finite rational-trace check on small integers is the concrete arithmetic residue of that bridge under the Sans-anchor pack (no fixed two-anchor). Closing this clause lets the parent assert full factorization without residual scaffolding on the small-orbit side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.