nontrivialCharacterValue_pos_on_nat
plain-language theorem explainer
Under the anchor-free native-cost pack, a nondegenerate map yields a strictly positive real character value at every positive integer. Cost and character-factorization arguments cite this before upgrading to the principal bound. The proof is a short contradiction: nonvanishing plus the trace identity force value plus reciprocal to equal a doubled trace at least two, impossible if the value is nonpositive.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base without two, sign-reversing, monotone, and zero-calibrated doubled trace). If the rational doubled trace of $F$ at $2$ is not equal to $2$, then for every natural number $n\ge 1$ the nontrivial real character value extracted from $F$ at $n$ is strictly positive.
background
This module builds a real character factorization of native recognition costs on ratio orbits. The rational doubled trace sends a rational display to the real trace of the orbit of that display. The nontrivial character value is the nondegenerate linear extraction of that trace against the anchor root at two: a real number attached to each nonzero rational whose multiplicative behaviour encodes the cost.
The ambient hypothesis pack is anchor-free: base structure without fixing two, sign-reversing and monotone native cost, and a zero-calibrated doubled trace. Nondegeneracy is the single numerical condition that the rational trace at two is not two itself.
Upstream, the character value is already known to be nonzero on nonzero rationals, and to satisfy the d'Alembert-type identity that the value plus its reciprocal recovers the rational trace. Separately, the rational trace on every positive integer is at least two.
proof idea
Cast $n\ge 1$ to a nonzero rational. Apply nonvanishing of the character value and the identity that value plus reciprocal equals the rational trace. Invoke the lower bound that the rational trace at $n$ is at least two. Argue by contradiction: if the character value is not positive then it is $\le 0$, hence (by nonvanishing) strictly negative, so its reciprocal is also strictly negative. The sum of two negatives cannot meet a lower bound of two; linarith closes.
why it matters
The immediate parent is the principal bound on natural numbers: once positivity is known, the same trace identity upgrades the character value from $>0$ to $\ge 1$ on every $n\ge 1$. That principal comparison is the arithmetic half of showing the extracted real character is the standard positive branch rather than a sign-flipped or exotic solution of the functional equation.
In the broader cost story this sits inside the real-character factorization of native PRC costs, which isolates the unique positive multiplicative character compatible with the Recognition Composition Law and the J-cost uniqueness (T5). It does not itself force $\phi$ or the eight-tick structure, but it clears the sign obstruction before those global uniqueness theorems consume the character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.