{"id":"palomar/PALOMAR-2026-10-30-000011","url":"https://github.com/jkfarland-bot/SmallRatios/tree/7e757a973e1297239400c90182e1b507ea48b7c0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000011-v1.json","repo":"https://github.com/jkfarland-bot/SmallRatios","tags":["math.NT","msc:11F20","msc:11A55","msc:11M20","msc:68V20"],"score":0,"title":"SmallRatio: Dedekind sums along Euclid's algorithm and the small-ratio formula","trust":"high","domain":"math.NT","source":"palomar","authors":["Joseph S. Farland"],"reviews":0,"subject":"math.NT","summary":"For a prime p and 0 = 1 with uv < p/2, |12 s(h,p) - p sum ([hv = u mod p] - [hv = -u mod p])/(uv)| <= 6n <= 12 log_2 p + 6, where n is the length of Euclid's algorithm on (p, h). Summed over any set H of residues, in particular over a subgroup of odd order, this gives |12 sum_{h in H} s(h,p) - p S_H(p)| <= |H| (12 log_2 p + 6), where S_H(p) is the signed sum of 1/(uv) over the coprime pairs with uv < p/2 and u/v in H or -H. The development proves Dedekind reciprocity from scratch (by counting lattice points), the identities of Euclid's algorithm and the bound n <= 2 log_2 k + 1, the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"The small-ratio formula for Dedekind sums, formalized in Lean","identifier":"","relationship":"formalizes"},{"title":"Mean squares of Dirichlet L-functions at s=1 over characters of fixed order and over subgroups","identifier":"","relationship":"formalizes"}]}