{"id":"palomar/PALOMAR-2026-09-03-000005","url":"https://github.com/sebastienpalcoux/sharp-intermediate-subgroup-bounds/tree/522d6dfcb5d25d47455375e3df0f8a561b7b780b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-03-000005-v1.json","repo":"https://github.com/sebastienpalcoux/sharp-intermediate-subgroup-bounds","tags":["math.GR","math.CO","msc:20D30","msc:20E15","msc:05A16","finite-groups","subgroup-lattices","lean-formalization"],"score":0,"title":"Sharp bounds for intervals in finite subgroup lattices","trust":"high","domain":"math.GR","source":"palomar","authors":["Sébastien Palcoux"],"reviews":0,"subject":"math.GR","summary":"Let H be a subgroup of a finite group G, let n = [G:H] > 1, and let p be the least prime divisor of n. This Lean development proves an exact finite rational upper envelope for the number of subgroups K with H ≤ K ≤ G and the strict bound c(p) n^((log_p n)/4), where c(p) is an Euler-product times a Gaussian theta series. It formalizes the bandwise moment inequality that drives the proof, a universal base-two bound with an exact decimal coefficient, the exact optimal answer for prime-power indices, and elementary-abelian asymptotics showing that both the constant and the exponent 1/4 are…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"Sharp bounds for intervals in finite subgroup lattices","identifier":"","relationship":"formalizes"}]}