natChar_monotoneMultiplicative
plain-language theorem explainer
The extracted real character of a nondegenerate cost ledger, restricted to positive integers, is completely multiplicative and nondecreasing. Anyone invoking Erdős's classification of monotone multiplicative maps on ℕ cites this packaging step. The proof fills the three structure fields from the character factorization lemmas, routing ledger monotonicity through the trace-comparison inequality on principal values.
Claim. Under the sans-anchor hypotheses on the orbit map $F$, and assuming the rational trace of $F$ at $2$ is not equal to $2$, the map $n\mapsto\chi_F(n)$ on natural numbers (where $\chi_F$ is the nontrivial real character extracted from the trace of $F$) is completely multiplicative and nondecreasing: $\chi_F(1)=1$, $\chi_F(mn)=\chi_F(m)\chi_F(n)$ whenever $m,n\ge 1$, and $m\le n$ implies $\chi_F(m)\le\chi_F(n)$.
background
In the cost/gauge-orbit setting, a ledger map $F$ on ratio orbits has a rational trace. When that trace is nondegenerate at $2$ (trace $\neq 2$), a real character $\chi_F$ is extracted by linear extraction against an anchor root: the nontrivial character value at a rational $x$. The structure MonotoneMultiplicative packages a map $f:\mathbb{N}\to\mathbb{R}$ with $f(1)=1$, complete multiplicativity on arguments $\ge 1$, and monotonicity on the positive integers; values at $0$ are unconstrained.
The comparison lemma le_of_trace_le states that $v\mapsto v+v^{-1}$ is strictly increasing on $[1,\infty)$, so an inequality between traces of principal values is an inequality between the values themselves. That is the bridge from ledger monotonicity (stated on costs/traces) to monotonicity of the character. Multiplicativity and the unit value are already proved for $\chi_F$ on nonzero rationals in the real-character factorization module.
proof idea
The proof constructs the three fields of MonotoneMultiplicative for $n\mapsto\chi_F(n)$.
unit: one-line reduction to the already-proved fact that the nontrivial character value at $1$ is $1$.mul: for $m,n\ge 1$, cast to nonzero rationals and apply complete multiplicativity of the nontrivial character value on $\mathbb{Q}^{\times}$.mono: for $1\le m\le n$, obtain principal-on-nat bounds for both arguments, invoke the nat-trace monotonicity lemma (which gives an inequality of traces $\chi+\chi^{-1}$), and feed that intole_of_trace_leto conclude $\chi_F(m)\le\chi_F(n)$.
why it matters
This is the exact interface Erdős's theorem needs: a completely multiplicative nondecreasing function on positive integers. Downstream, exists_nat_exponent applies that classification (Howe supplies a real exponent; the anchor root forces positivity; the six-exponentials input forces integrality) to conclude there is a positive integer $k$ with $\chi_F(n)=n^k$ for all $n\ge 1$. The doc-comment on that parent theorem notes this is the only place the six-exponentials import is used.
In the Recognition cost story, gauge-orbit classification of nondegenerate ledgers reduces to signed power laws once the extracted character is known to be a pure power on $\mathbb{N}$. That feeds the broader claim that cost displays are signed powers on ratio orbits, tying the ledger's J-cost geometry to discrete multiplicative structure rather than an arbitrary real character.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.