pos
plain-language theorem explainer
A completely multiplicative integer character with nondecreasing J-cost and positive value at 2 is strictly positive at every n ≥ 2. Cost-algebra morphisms and path-action lemmas cite this to keep values in the positive cone where J is well-posed. Proof is trichotomy on the sign of h(n), using jq monotonicity against the anchor and the nowhere-zero axiom.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, with $h(1)=1$, nowhere zero on positive integers, and with nondecreasing discrete $J$-cost $n\mapsto J(h(n))$. If $h(2)>0$, then $h(n)>0$ for every integer $n\ge 2$.
background
A monotone multiplicative character packages the arithmetic data a cost-compatible map leaves on the positive integers: complete multiplicativity, $h(1)=1$, nowhere-zero values, and monotonicity of the discrete cost jq (the $J$-cost on character values).
The underlying cost is $J(x)=\frac12(x+x^{-1})-1$, equivalently $H(x)=J(x)+1=\frac12(x+x^{-1})$, the unique solution of the Recognition Composition Law. On rationals, jq is nonnegative on the positive ray and falls when the argument is negative; monotonicity of jq\circ h therefore forbids a negative value at any $n\ge 2$ once the dyadic anchor is positive.
This module is the structural ledger for native PRC costs. The present lemma is the first filter keeping monotone characters inside the positive cone.
proof idea
Fix $n\ge 2$ and case-split on the sign of $h(n)$ by trichotomy.
If $h(n)<0$, mono gives jq(h 2) ≤ jq(h n). The sibling jq_lt_zero forces the right side below the unit comparison, while jq_nonneg at the positive anchor keeps the left side nonnegative; linarith yields the contradiction.
If $h(n)=0$, the nowhere-zero field of the monotone-multiplicative structure is absurd (omega discharges the side goal $1\le n$).
The remaining case is exactly $h(n)>0$.
why it matters
Positivity of character values is a standing gate for cost morphisms (CostMorphism requires the underlying map to preserve the positive cone) and for the path-action calculus: AdmissiblePath demands strict positivity so Jcost is defined, the constant-path constructor needs a positive level, and actionJ_nonneg integrates a nonnegative integrand. Convexity of the $J$-action on straight-line interpolants (actionJ_convex_on_interp) sits on the same cone.
In the Recognition framework this is arithmetic bookkeeping rather than a T5–T8 landmark, but it is the discrete gate that lets monotone characters feed the continuous cost algebra without leaving the domain where $J$ and the RCL are well-posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.