monoMult_gauge
plain-language theorem explainer
Two completely multiplicative, cost-monotone maps ℕ→ℚ that agree at 2 agree at every positive integer. This is the Erdős 1946 gauge theorem in the completely multiplicative case, cited by anyone pinning a monotone character by a single anchor. The proof splits on whether the common anchor equals 1 (both maps collapse to 1) or exceeds 1 (cut-lemma squeeze via transferred power comparisons).
Claim. Let $h_1,h_2:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, nowhere zero on positive integers, with $h_i(1)=1$ and nondecreasing cost $J\circ h_i$. If $h_1(2)=h_2(2)$ and $1\le h_1(2)$, then $h_1(n)=h_2(n)$ for every integer $n\ge 1$.
background
A monotone character (structure MonoMult) is an arithmetic function $h:\mathbb{N}\to\mathbb{Q}$ that is completely multiplicative, never zero on positive integers, normalized by $h(1)=1$, and whose cost $J\circ h$ is nondecreasing. Here $J$ is the native recognition cost (the T5 unique $J$-cost). The module builds a structural ledger for such characters without analysis: only rational arithmetic and integer comparisons.
The cut lemma says two rationals at or above the unit that transport the same integer-exponent comparisons against a common reference cut are equal: "the whole of the Erdős squeeze, and there is no analysis in it." Transfer lemmas push power inequalities $2^m\le n^k$ (or the reverse) through monotonicity of cost into the corresponding inequalities for $h(2)$ and $h(n)$. When the anchor is exactly 1, the character is identically 1 (the degenerate $c=0$ member).
The local setting is the PRC native-cost structural ledger: pin monotone characters by a single rational anchor before lifting to ratio-orbit costs.
proof idea
Case split on the anchor $h_1(2)$ relative to 1.
If $h_1(2)=1$, then $h_2(2)=1$ by the shared anchor, and both maps are identically 1 on $n\ge 1$ by the degenerate-gauge lemma trivial_of_two_eq_one.
If $1<h_1(2)$, fix $n\ge 1$. For $n=1$ both sides are 1 by the structure axiom. For $n\ge 2$, ge_one gives $h_i(n)\ge 1$. Apply the cut lemma with reference cut $\alpha=h_1(2)$ and the two values $\gamma=h_1(n)$, $\gamma'=h_2(n)$: the four transport hypotheses are exactly transfer_le/transfer_ge for $h_1$, and the same transfers for $h_2$ after rewriting the shared anchor. The cut lemma forces $h_1(n)=h_2(n)$.
why it matters
This is the arithmetic core of gauge rigidity for monotone characters. Downstream, monotone_multiplicative_pins is the special case with second character the identity: a monotone character sending 2 to 2 is the identity on positive integers ("the round-5 engine"). Further downstream, structural_gauge_rigidity lifts the same pin to ratio-orbit costs: two monotone costs that factor through characters and agree at the single orbit 2 agree on every positive integer orbit. Combined with the cube witness, "the anchor is a real choice, and it is the only one" (free-side stratification: form forced, unit free).
In the Recognition forcing chain this sits under native-cost uniqueness (T5 $J$-uniqueness and the composition law): once cost is $J$, monotone completely multiplicative data cannot float; a single rational anchor freezes the whole function. No logarithms or limits appear; the squeeze is purely rational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.