realCharacterCandidate_principal_on_pos_int
plain-language theorem explainer
Under the anchor-free native-cost pack on a ratio-orbit map F, the extracted real character is at least 1 on every positive integer orbit. Anyone assembling the PRC real-ratio character from the doubled trace cites this positivity/principal bound. The proof case-splits on the degenerate anchor (trace at 2 equals 2) versus the nontrivial branch and reduces each side to a prior lemma.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). Then for every natural number $n\ge 1$, the real character candidate of $F$ evaluated on the ratio orbit of $n$ satisfies $\mathrm{real\,character}(F,n)\ge 1$.
background
This module extracts a real multiplicative character on ratio orbits from the doubled trace of a native cost map $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. The doubled trace, written as rationalTrace on rational displays, is the real-valued readout of $F$ after embedding $\mathbb{Q}$ into ratio orbits. The candidate character is defined by cases: if the doubled trace at $2$ equals $2$ (degenerate anchor), it is the rational sign character; otherwise it is a generalized linear extraction, with value $0$ at the zero orbit.
SansAnchorHypotheses packages the structural native-cost assumptions without a fixed anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Positive integers embed as natOrbit n, the ratio orbit of $n$ as a rational, with toRat recovering $n$.
Upstream, rationalSignCharacter_of_pos gives value $1$ on positive rationals, and nontrivialCharacterValue_principal_on_nat already proves the same lower bound $1$ on naturals $n\ge 1$ in the nontrivial-trace branch.
proof idea
Introduce $n\ge 1$ and record $n>0$ and $n\neq 0$ as rationals. Case on whether rationalTrace F 2 = 2.
Degenerate branch: unfold the candidate, take the if_pos arm, rewrite the orbit to $n$ via natOrbit_toRat, and apply rationalSignCharacter_of_pos to get value $1$, hence $\ge 1$.
Nontrivial branch: unfold the candidate, take if_neg on the trace test and on $n\neq 0$, then invoke nontrivialCharacterValue_principal_on_nat under the same SansAnchorHypotheses and the nontriviality hypothesis. No further arithmetic is needed.
why it matters
The bound feeds directly into realCharacterCandidate_is_character, which assembles the full PRCRealRatioCharacter instance (unit, multiplicativity, reciprocity) for the extracted candidate. Without principal values $\ge 1$ on positive integer orbits, the character package cannot certify the unit and positivity conventions expected by the PRC native-cost uniqueness path.
In the Recognition cost layer this sits under the real-character factorization of the doubled trace: the same uniqueness story that forces the $J$-cost shape (T5) and the native cost functional. The result is a local positivity lemma, not a global uniqueness theorem, but it closes the integer-orbit side of the character axioms used when cost is reconstructed from a real ratio character (costFromRealCharacter and siblings).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.