{"id":"palomar/PALOMAR-2026-10-21-000015","url":"https://github.com/Flaman55/RamanujanNestedRadicals/tree/2b932baf2e72426583ef47a1bb23b4458879e959","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000015-v1.json","repo":"https://github.com/Flaman55/RamanujanNestedRadicals","tags":["math.CA","math.NT","msc:40A05","analysis","nested-radicals","series","lean"],"score":0,"title":"RamanujanNestedRadicals: convergence and exact values of Ramanujan-type nested radicals","trust":"high","domain":"math.CA","source":"palomar","authors":["Artur Flamandzki"],"reviews":0,"subject":"math.CA","summary":"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}…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Nested Radicals of Ramanujan's Type with Arbitrary Coefficient Sequences","identifier":"https://doi.org/10.5281/zenodo.18071173","relationship":"formalizes"}]}