natCast_monoMult
plain-language theorem explainer
The natural inclusion of positive integers into the rationals is a monotone multiplicative character: completely multiplicative, nowhere zero on n ≥ 1, and nondecreasing under the native cost jq. Anyone proving monotone rigidity or gauge uniqueness for characters on ℕ cites this as the reference model. The proof fills the four structure fields by casting lemmas, ring arithmetic, and the already-proved monotonicity of jq on [1, ∞).
Claim. The casting map $n \mapsto (n:\mathbb{Q})$ is a monotone multiplicative character on the positive integers: it is nowhere zero for $n \ge 1$, sends $1$ to $1$, is completely multiplicative, and is nondecreasing for the native cost $\mathrm{jq}$ (i.e., $1 \le m \le n$ implies $\mathrm{jq}(m) \le \mathrm{jq}(n)$).
background
In the Primitive Recognition Calculus native-cost ledger, a monotone multiplicative character is a map $h:\mathbb{N}\to\mathbb{Q}$ that is completely multiplicative on positive integers, never zero there, normalized by $h(1)=1$, and nondecreasing when costs are measured by $\mathrm{jq}$. The structure packages exactly those four arithmetic constraints.
The cost $\mathrm{jq}$ is the rational native cost on positive rationals; its key comparison lemma states that if $1\le s\le t$ then $\mathrm{jq}(s)\le\mathrm{jq}(t)$, proved by rewriting $t+t^{-1}-(s+s^{-1})$ as a manifestly nonnegative rational expression. That monotonicity is the only nontrivial input needed to place the identity casting map inside the structure.
Locally this sits in the structural ledger that records which arithmetic maps preserve the PRC cost ordering, preparatory to rigidity statements that pin characters to the identity.
proof idea
Instance construction for the four fields of the monotone-multiplicative structure on $n\mapsto(n:\mathbb{Q})$.
- Nonvanishing: cast
Nat.one_le_iff_ne_zerofrom $\mathbb{N}$ to $\mathbb{Q}$. - Unit:
norm_numgives $1=1$. - Multiplicativity:
push_castthenringon the cast product identity. - Cost monotonicity: apply the upstream comparison
jq_monoafter casting the hypotheses $1\le m$ and $m\le n$ into $\mathbb{Q}$.
No further lemmas; the work is bookkeeping plus the already-proved $\mathrm{jq}$ comparison on $[1,\infty)$.
why it matters
This is the reference character against which other monotone multiplicative maps are gauged. The sole downstream consumer is monotone rigidity: any monotone multiplicative $h$ with $h(2)=2$ equals the casting map on every positive integer. That theorem is the round-5 engine and the special case of the gauge theorem in which the second character is the identity; it is proved by feeding this instance and the hypothesis $h(2)=2$ into the general mono-multiplicative gauge comparison.
In the broader Recognition stack, pinning characters on $\mathbb{N}$ to the identity is the arithmetic half of forcing unique cost-compatible observables. It sits upstream of uniqueness arguments that eventually feed the forcing chain (J-uniqueness and the self-similar fixed point), by ensuring there is only one monotone multiplicative cost character once the value at $2$ is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.