eq_one_of_two_eq_one
plain-language theorem explainer
If a completely multiplicative nondecreasing map f from naturals to reals satisfies f(2)=1, then f(n)=1 for every positive integer n. Classification arguments for cost characters and power-like ledger maps cite this as the degenerate branch. The proof squeezes each n under a power of two, rewrites the image by multiplicativity, and matches the lower bound f≥1.
Claim. Let $f:\mathbb{N}\to\mathbb{R}$ be completely multiplicative and nondecreasing on positive integers, with $f(1)=1$. If $f(2)=1$, then $f(n)=1$ for every integer $n\ge 1$.
background
A MonotoneMultiplicative map is a real-valued function on the naturals that sends 1 to 1, is completely multiplicative for arguments at least 1, and is nondecreasing on that same range. The value at 0 is left free: the cost ledger never reads it.
In the Recognition Science cost layer such maps are candidate characters that turn integer tick counts into real costs while respecting composition of intervals. The non-degenerate theory identifies them with pure powers $n\mapsto n^c$ for a fixed $c\ge 0$. The present result isolates the zero-exponent (constant-1) case.
The module develops the elementary arithmetic of these maps (powers, log-ratios, existence of a common exponent) before the rigidity argument that forces a single global exponent from the value at 2.
proof idea
Fix $n\ge 1$. The bound $n<2^n$ together with monotonicity yields $f(n)\le f(2^n)$. The sibling power identity rewrites the right-hand side as $f(2)^n$. The hypothesis $f(2)=1$ collapses that to $1$. The reverse inequality $f(n)\ge 1$ is the standing lower bound for every such map on positive integers. Antisymmetry of $\le$ finishes the equality.
why it matters
This is the degenerate branch of the classification of monotone multiplicative cost maps. Once $f(2)=1$ is separated, the remaining work (Howe's argument, recorded in the sibling that equates log-ratios across bases) shows that $\log f(n)/\log n$ is independent of base, so $f$ is a pure power. That power form is the arithmetic skeleton behind the J-cost ladder and the phi-scaling of Recognition costs: only after the constant-1 case is closed can one extract a nontrivial exponent and match it to the self-similar fixed point forced at T6.
No downstream edges are recorded in the graph, yet the lemma is the necessary case-split before the heart of Howe's argument in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.