{"id":"palomar/PALOMAR-2026-09-15-000002","url":"https://github.com/nihargargava/IntegralMatrices/tree/4124db884ee55ef0da9e899d44d1bec5bfe432ea","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-15-000002-v1.json","repo":"https://github.com/nihargargava/IntegralMatrices","tags":["math.NT","msc:11R04","msc:11H06","number-theory","lean-formalization","algebraic-codes","matrix-counting"],"score":0,"title":"Integral Matrices of Fixed Rank over Number Fields: Lean formalization","trust":"high","domain":"math.NT","source":"palomar","authors":["Nihar Gargava"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of the fixed-rank asymptotic count for integral matrices over a number field and the convergence of moments of lifts of algebraic codes. The public results preserve the submission PDF's main scale, error terms, echelon-integral limit, and denominator normalization. The intermediate-rank height-counting input attributed to Schmidt is an explicit hypothesis; it is not silently assumed as an axiom.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-15","reactions":{},"formalized":true,"formalizes":[{"title":"Integral matrices of fixed rank over number fields","identifier":"arXiv:2510.11673","relationship":"formalizes"},{"title":"Short Bases of Lattices over Number Fields","identifier":"doi:10.1007/978-3-642-14518-6_15","relationship":"adapts"},{"title":"Integral matrices of fixed rank","identifier":"doi:10.2307/2160455","relationship":"adapts"}]}