{"id":"palomar/PALOMAR-2026-08-28-000001","url":"https://github.com/yuningyang19/parameter_free_gradient_p/tree/f71215fa936fe01aff8a765c62b399e131df963b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-28-000001-v1.json","repo":"https://github.com/yuningyang19/parameter_free_gradient_p","tags":["math.OC","msc:90C25","optimization","lean","gradient-methods","oracle-complexity"],"score":0,"title":"yuningyang19/parameter_free_gradient_p","trust":"high","domain":"math.OC","source":"palomar","authors":["Yuning Yang"],"reviews":0,"subject":"math.OC","summary":"A Lean 4 formalization of three results about exact value-gradient oracle complexity in finite-dimensional l_p geometry: strict-local scale-identification impossibility at fixed LR/epsilon = 4, the known-parameter p > 2 upper/lower exponent p/(p+2) with its stated horizon and dimension qualifications, and a post-secant-initialization parameter-free runtime family with the three p regimes. The Comparator surface contains exactly these three declarations; the other certified results remain supporting proof infrastructure.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-28","reactions":{},"formalized":true,"formalizes":[{"title":"Optimal Parameter-Free Gradient Minimization in l_p Geometry","identifier":"https://github.com/yuningyang19/parameter_free_gradient/blob/68483ace24e4e6e6094f6116fd5f4214f6676d7f/paper/manuscript_v7/main.tex","relationship":"formalizes"}]}