pos
plain-language theorem explainer
Any completely multiplicative nondecreasing map f from naturals to reals with f(1)=1 is strictly positive on every n ≥ 1. Cost-algebra morphisms, admissible-path actions, and J-integrand nonnegativity cite this to keep denominators and integrals well-defined. The argument is a one-line comparison chaining the sibling lower bound f(n) ≥ 1 against 0 < 1.
Claim. Let $f:\mathbb{N}\to\mathbb{R}$ be completely multiplicative and nondecreasing on the positive integers, with $f(1)=1$. Then for every natural number $n\ge 1$ one has $f(n)>0$.
background
The ambient structure is a completely multiplicative, nondecreasing real-valued map on the positive integers: $f(1)=1$, $f(mn)=f(m)f(n)$ whenever $m,n\ge 1$, and $m\le n$ (with $m\ge 1$) implies $f(m)\le f(n)$. The value at zero is deliberately unconstrained; the cost ledger that produces such characters has no content there.
The immediate prior fact is the sibling lower bound: under the same hypotheses, $f(n)\ge 1$ for every $n\ge 1$, obtained by monotonicity from $1$ to $n$ and the unit axiom. A related structural ledger result in the primitive recognition calculus likewise uses monotonicity alone to rule out negative values above the unit, once positivity at $2$ is known.
Locally this module packages the power-multiplicativity facts that the cost squeeze and the Recognition Composition Law need when the argument is a natural exponent.
proof idea
One-line term proof. Apply the sibling lower bound to obtain $1\le f(n)$, then chain with the elementary comparison $0<1$ via lt_of_lt_of_le. No case split on $n$, no appeal to multiplicativity beyond what the lower bound already used.
why it matters
Strict positivity of monotone-multiplicative cost characters is the gate that keeps path actions and cost morphisms inside the positive reals. Downstream, the admissible-path structure requires strictly positive continuous paths; the constant-path and straight-line interpolation constructors inherit positivity from this fact. Nonnegativity of the J-action on any admissible path, and convexity of that action under path interpolation, both rest on a positive integrand built from J-cost.
In the cost-algebra layer, morphisms are required to preserve positivity on $\mathbb{R}_+$; this lemma supplies the discrete skeleton of that condition when the character is evaluated on natural counts. Within Recognition Science the same positivity underwrites the J-cost landscape (T5 uniqueness of $J(x)=\cosh(\log x)-1$) and the nonnegativity of recognition action along admissible trajectories, so the ledger never assigns a negative cost to a positive integer tick count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.