rationalTrace_nat_eq_two_of_two_eq_two
plain-language theorem explainer
If an anchor-free native cost map has rational doubled-trace equal to 2 at the integer 2, then that trace equals 2 at every positive natural. Cited when ruling out the degenerate constant-trace character before extracting a nontrivial real ratio character. The proof sandwiches the value between the universal lower bound 2 and the power-of-two case, using n ≤ 2^n and monotonicity.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). If the rational doubled trace of $F$ at $2$ equals $2$, then for every natural number $n \ge 1$ the rational doubled trace of $F$ at $n$ equals $2$.
background
In the real-character factorization of native cost, one studies maps $F$ on ratio orbits under the anchor-free pack SansAnchorHypotheses: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. The rational doubled trace is the honest real-valued display of that cost on rational arguments, obtained by sending a rational to its ratio orbit and reading the trace display.
A basic lower bound already holds: for every natural $n \ge 1$, the rational trace is at least $2$. Monotonicity of $F$ on positive integer orbits upgrades this to monotonicity of the rational trace along the naturals. Separately, if the trace equals $2$ at the integer $2$, induction on a two-step scheme forces the trace to equal $2$ at every power of two.
The present statement closes the gap between those two facts: once the value at $2$ is pinned, the trace cannot rise above $2$ on any positive natural, so it is constantly $2$ on $\mathbb{N}_{\ge 1}$.
proof idea
First prove the elementary bound $n \le 2^n$ by induction on $n$ (base $0$ by norm_num; successor uses $1 \le 2^k$ and omega).
Fix $n \ge 1$. The lower bound rationalTrace_nat_ge_two gives $2 \le$ rational trace at $n$. Monotonicity rationalTrace_nat_mono with $n \le 2^n$ gives rational trace at $n$ $\le$ rational trace at $2^n$. Cast $2^n$ as a rational power, then apply rationalTrace_two_pow_eq_two (using the hypothesis that the trace at $2$ is $2$) to replace the upper bound by $2$. Conclude by linarith.
why it matters
This is the natural-number step in the degenerate-trace dichotomy for real ratio characters. Its sole downstream consumer is rationalTrace_pos_eq_two_of_two_eq_two, which lifts the same conclusion from positive naturals to all positive rationals (via numerator extraction).
In the Recognition cost stack, a constantly-$2$ doubled trace is the trivial character; the complementary case (trace at $2$ strictly above $2$) feeds the nontrivial linear extraction and the real ratio character used to rebuild native cost. The argument sits inside the PRC native-cost uniqueness line (anchor-free structural hypotheses), not the T5–T8 forcing chain itself, but it clears the degenerate branch before cost-from-character reconstruction proceeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.