ge_one
plain-language theorem explainer
A completely multiplicative monotone character on the positive integers that exceeds 1 at the anchor 2 must satisfy h(n) ≥ 1 for every n ≥ 2. Cited by anyone running the cut-squeeze uniqueness argument for monotone characters (the Erdős gauge). Proof is contradiction via a minimal power of the anchor that lifts a putative dip above the unit, then strict cost monotonicity.
Claim. Let $h:\mathbb{N}\to\mathbb{Q}$ be completely multiplicative, nowhere zero on $n\ge 1$, with $h(1)=1$, and with nondecreasing cost $J\circ h$ (a monotone character). If $h(2)>1$, then $h(n)\ge 1$ for every integer $n\ge 2$.
background
In the Primitive Recognition Calculus ledger, a monotone character is packaged as the structure MonoMult: a map $h:\mathbb{N}\to\mathbb{Q}$ that is completely multiplicative on positive integers, satisfies $h(1)=1$ and $h(n)\ne 0$ for $n\ge 1$, and is nondecreasing in the native cost $jq$ (the rational form of the J-cost $J(x)=(x+x^{-1})/2-1$). The shifted cost $H=J+1$ turns the Recognition Composition Law into d'Alembert's equation, but the present argument works entirely with $jq$ and rational arithmetic.
The local setting is the structural ledger that prepares the gauge theorem: two monotone characters agreeing at the single index 2 agree everywhere. Before uniqueness can run, one needs elementary comparison lemmas that push inequalities between powers of integers into inequalities between powers of character values. The present result is the base positivity/lower-bound fact those transfers rely on: once the anchor strictly exceeds the unit, no later value may fall below it.
proof idea
Contradiction. Fix $n\ge 2$ with $h(n)<1$. Positivity of $h$ (from MonoMult and $h(2)>0$) gives $h(n)>0$, so some power of the anchor clears the reciprocal: $\exists k$ with $(h 2)^k,h(n)\ge 1$. Take the least such $k$; it cannot be zero (else $h(n)\ge 1$). Write $k=j+1$. Minimality forces $(h 2)^j h(n)<1$, hence $(h 2)^k h(n)<h(2)$. Complete multiplicativity rewrites the left side as $h(2^k n)$. Cost monotonicity of MonoMult then yields $jq(h 2)\le jq(h(2^k n))$. But $jq$ is strictly monotone on the ray above 1 in the sense of the sibling lemma jq_strictMono, and the two bounds $1\le (h 2)^k h(n)<h(2)$ produce a strict inequality that contradicts the previous comparison. Finish by linarith.
why it matters
This is the lower-bound half of the arithmetic control needed for the gauge theorem (Erdős 1946, completely multiplicative case) stated as monoMult_gauge in the same module: agreement at the single anchor 2 forces agreement at every positive index, with no logarithms or real limits. The two transfer lemmas transfer_le and transfer_ge invoke it to justify that power inequalities among integers pass to the character values once $h(2)>1$.
In the Recognition Science forcing chain the result sits inside the native-cost ledger that certifies uniqueness of the cost character before T5 J-uniqueness and the RCL are applied globally. It closes the elementary gap that would otherwise let a monotone character dip below the unit after a super-unit anchor, which would break the cut-squeeze that pins the whole arithmetic function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.