rationalTrace_nat_ge_two
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the doubled rational trace of any positive integer display is at least 2. Cost and gauge-orbit arguments cite this as the uniform lower bound on natural points. The proof is a one-line reduction to the positive-integer-orbit display bound via the rational-orbit embedding.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). Then for every natural number $n\ge 1$, the real doubled trace of $F$ at the rational display $n$ obeys $2\le T_F(n)$.
background
In the real-character factorization of native cost, maps $F$ act on RatioOrbit (integer numerator over nonzero orbit denominator). The doubled trace is first carrier-valued, then displayed as a real via traceDisplay, which coerces the doubled-trace rational to $\mathbb{R}$. The specialization rationalTrace F x is that display on the orbit of a rational $x$.
SansAnchorHypotheses packages the structural native-cost conditions without a fixed anchor: base-sans-two, sign-reversing, monotone, and zero-calibration of the doubled trace. Upstream, traceDisplay_posInt_ge_two already gives $2\le\mathrm{traceDisplay},F,q$ whenever $q$ is a positive-integer orbit. The present statement is the same bound written on natural numbers through the rational-orbit embedding.
proof idea
Term-mode one-liner. Rewrite the goal as $2\le\mathrm{traceDisplay},F,(\mathrm{ratioOrbitOfRat},n)$ by unfolding rationalTrace. Apply traceDisplay_posInt_ge_two to $hF$, supplying the witness that the orbit of $n$ is a positive-integer orbit: the triple $\langle n,,1\le n,,\mathrm{ratioOrbitOfRat_toRat},n\rangle$. No further arithmetic.
why it matters
Gives the uniform floor $T_F(n)\ge 2$ on every positive integer display, the quantitative starting point for character nondegeneracy on $\mathbb{N}$. Downstream, charges_positively_at_two uses the $n=2$ case to turn nonvanishing of $F$ at orbit two into a strict positivity statement. nontrivialCharacterValue_pos_on_nat needs the same lower bound to keep nontrivial character values positive on naturals, and rationalTrace_nat_eq_two_of_two_eq_two uses it as the comparison side when the trace is pinned at two. In the Recognition cost story this is the integer-display half of the uniqueness pipeline that forces the J-cost shape (T5) once the doubled trace is calibrated and monotone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.