MonoMult
plain-language theorem explainer
A monotone character on the positive integers is a completely multiplicative map h:ℕ→ℚ that never vanishes for n≥1, fixes 1, and has nondecreasing rational J-cost. Rigidity and uniqueness arguments for native costs on ratio orbits cite this interface as the discrete arithmetic shadow of a PRC character. It is a pure Prop structure: four axioms, no proof body.
Claim. A map $h:\mathbb{N}\to\mathbb{Q}$ is a monotone multiplicative character when (i) $h(n)\neq 0$ for every $n\ge 1$, (ii) $h(1)=1$, (iii) $h(mn)=h(m)h(n)$ for all $m,n\ge 1$, and (iv) the rational $J$-cost is nondecreasing: $J_q(h(m))\le J_q(h(n))$ whenever $1\le m\le n$.
background
In the Primitive Recognition Calculus structural ledger, native costs on ratio orbits factor through characters. The Recognition cost is the T5 functional $J(x)=(x+x^{-1})/2-1$; its shift $H=J+1$ turns the Recognition Composition Law into d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$. On rational values the same geometry is tracked by the rational cost $J_q$ (written jq in the module).
Completely multiplicative arithmetic functions that are monotone in this cost are the discrete shadows of continuous ratio-orbit characters. The module sits on the native-cost minimality certificate import and packages ledger facts that pin which such characters can arise from cube-generated or factorized native costs. The structure records exactly the arithmetic data the doc-comment names: completely multiplicative, nowhere zero, with nondecreasing cost.
proof idea
Definitional Prop structure with empty proof body. Four fields package the axioms directly: nonvanishing on $n\ge 1$; unit $h(1)=1$; complete multiplicativity $h(mn)=h(m)h(n)$; and cost monotonicity stated in the $J_q$ order rather than the raw rational order, matching Recognition cost geometry. Downstream lemmas inhabit or consume the structure; nothing is proved at the declaration itself.
why it matters
Hypothesis type for the gauge theorem: two monotone characters that agree at the single index 2 agree at every positive index (Erdős 1946, completely multiplicative case; cut-squeeze, no logarithm or real limits). Specializes to monotone rigidity: the character with $h(2)=2$ is the identity on $\mathbb{N}$. Also feeds the one-sided bound that an anchor $>1$ forces values $\ge 1$ above the unit, the extraction theorem that a monotone factorized PRC cost leaves exactly this arithmetic data on $\mathbb{N}$, and the canonical inhabitant $n\mapsto n$. Non-canonicity results such as the cube-generated cost at two failing cross-equality with the ratio-orbit cost rely on the same ledger. In the forcing chain this sits under T5 $J$-uniqueness and the RCL, restricting which discrete characters can realize native costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.