traceDisplay_two_ge_two
plain-language theorem explainer
Under the anchor-free native-cost hypotheses on a map F of ratio orbits, the real doubled-trace display at the orbit 2 is at least 2. Cost and PRC uniqueness arguments cite this when extracting the anchor root from the doubled trace evaluated at 2. The proof is a one-line specialization of the positive-integer-orbit lower bound, packing the orbit 2 as a positive integer orbit via its rational value.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost hypotheses (base without two, sign-reversing, monotone, and zero-calibrated doubled trace). Write $\mathrm{tr}_F(q)$ for the real display of the carrier-valued doubled trace of $F$ at orbit $q$. Then $2 \le \mathrm{tr}_F(2)$, where $2$ denotes the ratio orbit with numerator the signed orbit of two and denominator one.
background
In the real-character factorization of native cost, maps $F$ on ratio orbits are constrained by an anchor-free hypothesis pack: base without two, sign-reversing, monotone, and zero-calibrated doubled trace. That pack matches the structural native-cost hypotheses with the anchor clause stripped.
A ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). The distinguished orbit two is the ratio orbit whose rational value is exactly $2$. The real display of the doubled trace sends an orbit $q$ to the real number obtained by casting the carrier-valued doubled trace of $F$ at $q$ through its rational presentation.
The upstream bound states that under the same hypotheses, every positive-integer orbit $q$ satisfies $2 \le \mathrm{tr}_F(q)$. The present result is the instance at the orbit of two.
proof idea
One-line wrapper. Apply the positive-integer-orbit lower bound to $F$ under the given anchor-free pack, supplying the witness that the orbit of two is a positive-integer orbit: natural $2$, a trivial positivity check, and the simp fact that its rational value equals $2$. No further algebra.
why it matters
This specialization is the numerical gate for the anchor root extracted from the doubled trace at 2. Downstream, the lower bound $1 \le$ anchor root is obtained by feeding the inequality into the real-trace-root comparison, and the identity anchor root plus its inverse equals the rational trace at 2 is obtained the same way via the add-inverse root lemma.
In the Recognition cost story the doubled-trace display is the real shadow of the native cost character; bounding it at 2 pins the hyperbolic fixed-point data that later recovers the J-cost shape $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar scale $\varphi$ (T6). Without $2\le\mathrm{tr}_F(2)$ the anchor root is not guaranteed to sit in $[1,\infty)$, and the factorization into a real character collapses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.