monotone_multiplicative_pins
plain-language theorem explainer
A completely multiplicative, nowhere-zero map h from naturals to rationals with nondecreasing J-cost and h(2)=2 equals the identity on every positive integer. The structural ledger calibration cites this as the monotone rigidity pin that forces the native cost character on integer orbits. Proof is a one-line specialization of the gauge comparison against the identity character.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, nowhere zero for $n\ge 1$, with $h(1)=1$, and with nondecreasing cost $J_q(h(\cdot))$ on positive integers. If $h(2)=2$, then $h(n)=n$ for every integer $n\ge 1$.
background
In the Primitive Recognition Calculus structural ledger, a character on positive integers is recorded by the MonoMult package: complete multiplicativity, unit normalization $h(1)=1$, nowhere-zero values, and monotonicity of the rational J-cost $J_q$ along the natural order. Here $J_q$ is the discrete display of the Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently the shifted form $H=J+1$).
The module builds the round-5 structural ledger: reciprocity, normalization invariance, the nonzero composition law, unit-zero, the orbit-2 anchor, sign reversal, monotonicity, and the zero-orbit convention. Compared with earlier slim ledgers, prime-pair product families and signed-unit calibrations that named the canonical cost are removed.
Upstream, the gauge comparison for two MonoMult characters reduces equality of characters to matching cost and a single pin. The identity map $n\mapsto n$ is itself MonoMult, so it is the natural comparison target once $h(2)=2$ is fixed.
proof idea
Term-mode one-liner: apply the MonoMult gauge theorem comparing $h$ to the natural-cast character $n\mapsto(n:\mathbb{Q})$. Both sides are MonoMult; the two gauge side-conditions collapse by rewriting the given pin $h(2)=2$ and a numeric check, so the gauge forces $h=n$ on every positive integer.
why it matters
This is the monotone rigidity step of the round-5 engine. Downstream, structural_character_calibrated_on_positive_integers uses it to conclude that any character attached to a structural native cost agrees in $J_q$-display with the identity on every positive-integer orbit (up to reciprocal orientation invisible to the cost). That calibration is how the structural ledger forces the canonical cost without naming it in the hypotheses.
In the broader Recognition chain, locking multiplicative characters on $\mathbb{N}$ to the identity supports the arithmetic side of cost uniqueness tied to T5 J-uniqueness and the Recognition Composition Law, before ladder and dimension forcing (T6–T8) are invoked. It closes the integer-orbit half of the structural-character story rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.