RamanujanNestedRadicals: convergence and exact values of Ramanujan-type nested radicals
Lean 4 / Mathlib formalization of the results of the author's paper "Nested Radicals of Ramanujan's Type with Arbitrary Coefficient Sequences" (Flamandzki, 2026). For a coefficient sequence a : N -> R, the radical of depth d is built by the recursion R_k = sqrt(1 + a_k R_{k+1}) from a seed; `Submission.rollUp a T d` is the depth-d truncation with seed T and `Submission.truncRadical a d` uses the seed 1. For a root order n >= 2 the square root is replaced by the n-th root (`Submission.rollUpN`) and, for the classical unbounded family, by the signed recursion with radicand (-1)^n + a_k R_{k+1}…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-21-000015
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-21-000015/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-21-000015/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'