trivial_of_two_eq_one
plain-language theorem explainer
If a completely multiplicative, nowhere-zero arithmetic character on the positives has nondecreasing J-cost and equals 1 at 2, then it is identically 1 on every positive integer. This is the degenerate (c = 0) member of the power family of monotone characters. The gauge theorem cites it to discharge the unit-anchor case. The proof squeezes the cost between the value at 2 and at 2^n via complete multiplicativity and monotonicity.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, nowhere zero on positives, with $h(1)=1$, and with nondecreasing cost $J\circ h$. If $h(2)=1$, then $h(n)=1$ for every integer $n\ge 1$.
background
The ambient structure is a monotone character: an arithmetic map $h:\mathbb{N}\to\mathbb{Q}$ that is completely multiplicative, satisfies $h(1)=1$, never vanishes on positives, and has nondecreasing cost under the native cost functional $J$ (equivalently under the shifted cost $H=J+1$). The cost comparison is written through the rational display jq of $J$ on the values of $h$.
This sits in the Primitive Recognition Calculus structural ledger for native cost. The ledger isolates the arithmetic data a monotone character leaves on the positives before any real-analytic or logarithmic machinery is introduced. The shifted cost $H(x)=\tfrac12(x+x^{-1})$ converts the Recognition Composition Law into d'Alembert form, but the present argument never leaves the rationals.
The result is the unit-anchor degeneration: fixing $h(2)=1$ forces the whole character to the constant $1$, the sign character / $c=0$ power.
proof idea
First prove $n\le 2^n$ by induction on $n$ (base $0$; successor uses $1\le 2^k$ and omega). Fix $n\ge 1$. If $n<2$ then $n=1$, so $h(n)=h(1)=1$ by the unit axiom of MonoMult.
If $n\ge 2$, monotonicity gives $J(h(2))\le J(h(n))\le J(h(2^n))$. The left side is $J(1)$ by the hypothesis $h(2)=1$. The right side uses complete multiplicativity: $h(2^n)=h(2)^n=1^n=1$, so again $J(1)$. Antisymmetry of the cost order forces $J(h(n))=J(1)=0$; the companion lemma that $J$ vanishes only at $\pm 1$, together with $h(n)\ne 0$, yields $h(n)=1$.
why it matters
This is the degenerate branch of the gauge theorem (Erdős 1946, completely multiplicative case) formalized immediately downstream as monoMult_gauge: two monotone characters that agree at the single index $2$ agree everywhere. The parent splits on whether the common anchor is $1$ or strictly larger; the unit case is discharged by a one-line appeal to this lemma, after which the non-unit case runs the cut squeeze between powers of $2$.
In Recognition Science the monotone characters are the discrete skeletons of $J$-automorphisms. Collapsing the unit-anchor member shows that the only cost-flat completely multiplicative character is the trivial one, so nontrivial native cost on the positives is forced as soon as $h(2)\ne 1$. That feeds the structural ledger certifying that the native cost is the unique monotone multiplicative cost compatible with the Recognition Composition Law, upstream of the forcing chain steps that pin $J$ (T5) and $\varphi$ (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.