RogersRamanujanSpecialValue
plain-language theorem explainer
This structure records a natural number n paired with a proposition that the Rogers-Ramanujan continued fraction at nome exp(-2 pi sqrt n) evaluates to an algebraic number in the golden ratio phi. Researchers cataloging q-series identities or tracing phi emergence in partition functions cite the record when listing special cases. The declaration is introduced as a bare structure definition carrying no computational obligations or lemmas.
Claim. A special value of the Rogers-Ramanujan continued fraction consists of a natural number $n$ together with a proposition asserting that $R(e^{-2π √n})$ is algebraic in the golden ratio $φ$, where $R(q)$ denotes the infinite continued fraction $q^{1/5} / (1 + q / (1 + q^2 / (1 + ⋯)))$.
background
The module treats continued fractions as sequential J-cost geodesics on the positive reals. The cost functional is defined by $J(x) = ½(x + x^{-1}) - 1$, which is strictly convex, attains its global minimum at $x=1$, and possesses the unique positive self-similar fixed point $φ = 1 + 1/φ$. In the Recognition Science setting the nome $q = e^{-2π √n}$ parametrizes a recognition temperature; the limit $q → 0^+$ recovers the ground state $R(q) → 1$. Upstream structures on phi-forcing and ledger factorization supply the convexity and uniqueness properties that force all infinite nestings to land on $φ$-algebraic numbers.
proof idea
The declaration is a structure definition. It introduces the record type directly with two fields and no attached lemmas, tactics, or reduction steps.
why it matters
The structure supplies the element type for the enumeration rr_special_values that lists the cases n=1 through n=5, each marked algebraic in phi. It therefore bridges the classical Ramanujan identities to the Recognition Science claim that phi is the unique attractor of J-cost optimization (T5 uniqueness of the J-minimum together with T6 self-similar fixed-point forcing). The record supports the argument that the continued-fraction recursion converges to phi-algebra because the cost landscape admits no other self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.