no_rational_character_at_trace_three
plain-language theorem explainer
There is no rational number r with r + 1/r = 3. Anyone working the RS cost/character factorization at ratio two cites this: a cost that is rational at two cannot carry a rational multiplicative character there. The proof clears r ≠ 0, rewrites the trace as the quadratic r² − 3r + 1 = 0, and reduces to the nonexistence of a rational square root of five.
Claim. There is no rational $r$ such that $r + r^{-1} = 3$.
background
In the cost layer, a multiplicative character on positive reals is tracked through its trace $u + u^{-1}$. The equation $r + r^{-1} = 3$ is the integer-trace instance that appears when one asks whether a cost that is rational at the ratio two can be realized by a rational character at that same ratio.
The real (irrational) solution is the square of the golden ratio: $\varphi^2 + \varphi^{-2} = 3$. Thus the obstruction is arithmetic, not analytic. The only upstream lemma needed is that no rational squares to five, proved by five-adic valuation (a square has even valuation; five has valuation one).
Locally the module develops the arithmetic of rational traces of real powers, feeding the six-exponentials input that forces positive real exponents with rational traces on small integer bases to be positive integers.
proof idea
Assume $r\in\mathbb{Q}$ satisfies $r+r^{-1}=3$. First $r\neq 0$ (else the equation is absurd by norm_num). Clearing the denominator with field_simp and rearranging by linarith yields the monic quadratic $r^2-3r+1=0$.
From that identity, $$(2r-3)^2=4r^2-12r+9=4(r^2-3r+1)+5=5.$$ So $2r-3$ would be a rational square root of five. Discharge by applying no_rational_sqrt_five to the witness $2r-3$, with the squared identity checked by nlinarith.
why it matters
This is the elementary arithmetic gate that blocks a rational character at trace three. Downstream, rat_of_trace_rat_of_pow_rat uses the same circle of ideas: a rational trace plus any positive rational power forces the base itself to be rational, so genuinely quadratic units never have rational powers. That lemma, together with this nonexistence, feeds exponent_is_positive_integer, the arithmetic half of the gauge-orbit classification under the six-exponentials input (analytic half is Howe).
It also appears in the primitive recognition calculus ledger: cubeGeneratedNativeCost_two_not_canonical rules out a cube-generated native cost at two as canonical on the ratio orbit. In framework terms the golden-ratio fixed point (T6) is exactly the real witness whose square has trace three; the theorem says that witness cannot be rational, so carrier-valued rational characters are too strong a demand at this cost value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.