no_rational_sqrt_five
plain-language theorem explainer
There is no rational whose square is five. The lemma is the arithmetic step behind ruling out a rational solution of the trace equation r + r^{-1} = 3, which the cost module needs when asking whether a rational character can sit at ratio two. The proof is a short five-adic valuation parity argument: squares have even valuation while five has valuation one.
Claim. There is no rational number $s \in \mathbb{Q}$ such that $s^{2} = 5$.
background
In the cost/trace setting of this module one studies multiplicative characters attached to recognition cost on positive ratios. The natural algebraic relation for a unit-circle (or reciprocal) character is the trace equation $r + r^{-1} = t$ for a prescribed real $t$. Clearing denominators turns $t = 3$ into the quadratic $r^{2} - 3r + 1 = 0$, whose discriminant is five.
Thus rationality of a root is equivalent to rationality of $\sqrt{5}$. The present lemma records the classical negative fact in Lean: five is not a square in $\mathbb{Q}$. The argument is local at the prime five, using the five-adic valuation on rationals (padicValRat), which is additive on products and therefore multiplies by the exponent on powers.
The surrounding module then lifts the non-existence of $\sqrt{5}$ in $\mathbb{Q}$ to non-existence of a rational character at trace three, blocking an overly strong demand that factorization of a rational cost value produce a carrier-valued rational character.
proof idea
Assume for contradiction $s \in \mathbb{Q}$ with $s^{2} = 5$. First $s \neq 0$ (else $0 = 5$). The five-adic valuation multiplies under powers: $\mathrm{v}{5}(s^{2}) = 2,\mathrm{v}{5}(s)$ via padicValRat.pow. On the other side $\mathrm{v}{5}(5) = 1$ by padicValRat.self. Substituting $s^{2} = 5$ yields $1 = 2,\mathrm{v}{5}(s)$, impossible for an integer valuation; omega closes the contradiction. The only setup is the Fact (Nat.Prime 5) instance needed by the valuation API.
why it matters
The sole direct consumer is no_rational_character_at_trace_three, whose doc-comment states the framework point: the demand for a carrier-valued character is too strong. A cost that takes the perfectly rational value $1/2$ at ratio two still has no rational character at that ratio, because $r + r^{-1} = 3$ has no rational solution. That non-existence is exactly the quadratic whose discriminant is five, so this lemma is the number-theoretic bottleneck.
In Recognition Science the same quadratic is the characteristic equation for the golden ratio fixed point (T6): the self-similar scale $\varphi$ satisfies $\varphi + \varphi^{-1} = \sqrt{5}$ shifts of the same shape, and rational character demands would collapse the $\varphi$-ladder arithmetic. Blocking a rational root keeps the cost factorization from over-claiming a rational multiplicative character where only an irrational (golden) one exists. The result is pure arithmetic scaffolding inside the Cost domain; it does not itself invoke J-uniqueness or the eight-tick octave, but it protects the integrity of later character and exponent arguments that do.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.