monoMult_of_character
plain-language theorem explainer
A monotone native cost that factors through a ratio character leaves completely multiplicative, nowhere-zero arithmetic data on the positive integers, with nondecreasing J-cost. Gauge-rigidity arguments for factorized PRC costs cite this extraction. The proof assembles the four MonoMult axioms from character multiplicativity, unit preservation, and monotonicity of F on natural orbits.
Claim. Let $F$ and $\chi$ map ratio orbits to ratio orbits. Suppose $F$ is monotone on positive-integer orbits, $\chi$ is a ratio character, and $F(q)$ is cross-equal to the cost induced by $\chi$ at every orbit $q$. Then $n \mapsto (\chi(\mathrm{natOrbit}\, n))^{\mathrm{disp}}$ is completely multiplicative on $\mathbb{N}_{\ge 1}$, sends $1$ to $1$, is nowhere zero, and has nondecreasing $J$-cost $jq$.
background
In the primitive recognition calculus, costs act on ratio orbits. A native cost $F$ is monotone when, on positive-integer orbits, larger rational imbalance never lowers the displayed cost of $F$. A ratio character $\chi$ is a multiplicative, unit-preserving, nonzero-preserving map on orbits; its induced cost is the orbit whose display is $jq$ of the character value (the standard $J$-cost on rationals: $J(x)=(x+x^{-1})/2-1$).
MonoMult packages the arithmetic shadow of such a character on $\mathbb{N}$: $h(1)=1$, $h(mn)=h(m)h(n)$ for $m,n\ge 1$, $h(n)\ne 0$, and $jq(h(m))\le jq(h(n))$ whenever $1\le m\le n$. Natural numbers embed as orbits via natOrbit, with display equal to the integer itself.
The module builds structural ledger facts for native costs that factor through characters. Upstream, character display and cross-equality identify $F$ with $jq\circ\chi$ on displays; multiplicativity of characters and of orbit multiplication supply the algebraic skeleton.
proof idea
First rewrite: cross-equality plus costFromCharacter_jq gives $(F q)^{\mathrm{disp}}=jq((\chi q)^{\mathrm{disp}})$ for every orbit $q$.
Build MonoMult by fields. Nonzero: character nonzero-preservation on natOrbit n, using natOrbit_toRat and $n\ge 1$. Unit: natOrbit 1 displays as the unit orbit, so character display plus the character unit axiom yield display $1$. Multiplicativity: natOrbit(mn) displays as the product of the two natural orbits; character display and character multiplicativity push the product through to rational multiplication. Monotonicity: apply $F$-monotonicity on natOrbit m and natOrbit n (both positive-integer orbits when $1\le m\le n$), then rewrite both sides via the display identity to $jq$ of the character values.
why it matters
This is the bridge from geometric cost data (monotone $F$ factoring through $\chi$) to pure arithmetic on $\mathbb{N}$. Downstream, structural_gauge_rigidity uses it: two monotone factorized costs that agree at the single orbit $2$ agree on every positive-integer orbit. The doc there states the free-side stratification: form forced, unit free; the anchor is a real choice and the only one.
In the Recognition forcing picture this supports uniqueness of the cost shape once factorization and monotonicity are in hand (the $J$-uniqueness landmark T5, and the RCL that $J$ satisfies). Reciprocal and orientation lemmas sitting just below show the character can be flipped without changing cost, so only the gauge at $2$ remains free. Without extracting MonoMult, the integer-orbit comparison in gauge rigidity has no multiplicative handle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.