rr_special_values
plain-language theorem explainer
This definition enumerates the known special values of the Rogers-Ramanujan continued fraction at nomes q = exp(-2π√n) for n = 1 to 5, each marked algebraic in φ. Researchers tracing Ramanujan evaluations to the golden ratio fixed point would cite it as concrete anchoring data. The construction is a direct list of five structure instances asserting the algebraic property for each n.
Claim. The finite list of pairs (n, algebraicInPhi) for n = 1,2,3,4,5 in which each entry satisfies that the Rogers-Ramanujan continued fraction R(q) at q = e^{-2π√n} evaluates to an algebraic expression in the golden ratio φ.
background
The module treats continued fractions as sequential J-cost optimization on the positive reals. The functional J(x) = ½(x + x^{-1}) - 1 is strictly convex, attains its unique minimum at x = 1, and possesses the self-similar fixed point φ satisfying x = 1 + 1/x. The Rogers-Ramanujan continued fraction R(q) is the q-deformation of the simple φ-continued fraction; as q → 0^+ it approaches the ground state 1, while at the discrete nomes q = e^{-2π√n} the values remain algebraic in φ. The upstream structure RogersRamanujanSpecialValue packages each such nome n together with the proposition that the evaluation is algebraic in φ.
proof idea
The definition is a direct list literal that constructs five instances of the RogersRamanujanSpecialValue structure, one for each n from 1 to 5, with the algebraicInPhi field instantiated to True.
why it matters
The entry supplies the concrete data supporting the module claim that all known special values of R(q) are algebraic in φ. It thereby illustrates the RS interpretation that φ is the unique attractor of the J-cost recursion and that the continued-fraction iteration converges to the ground-state geodesic. No downstream theorems currently depend on it; the list serves as an explicit witness inside the Ramanujan bridge section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.