{"id":"palomar/PALOMAR-2026-09-10-000002","url":"https://github.com/yuma-mizuno/KR-mod9-lean/tree/d8b921339ecc655aa14b38b556605dbf81f7b87b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-10-000002-v1.json","repo":"https://github.com/yuma-mizuno/KR-mod9-lean","tags":["math.NT","math.CO","msc:11P84","msc:33D15","msc:11F03","q-series","partition-identities","lean","number-theory"],"score":0,"title":"KR-mod9-lean","trust":"high","domain":"math.NT","source":"palomar","authors":["Yuma Mizuno"],"reviews":0,"subject":"math.NT","summary":"Lean 4 proofs of the three Kanade-Russell identities modulo nine as identities of integer formal power series, including coefficientwise summability of the defining double sums. The development includes concrete vertex-operator spanning bounds and the character evaluations used to identify the sums with their infinite products.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-10","reactions":{},"formalized":true,"formalizes":[{"title":"The three Kanade-Russell identities modulo nine","identifier":"https://arxiv.org/abs/2609.09653v1","relationship":"formalizes"},{"title":"A vertex operator reformulation of the Kanade-Russell conjecture modulo 9","identifier":"https://arxiv.org/abs/2211.12351v3","relationship":"adapts"}]}