{"id":"palomar/PALOMAR-2026-10-23-000002","url":"https://github.com/PranavaKCode/nivat-lean/tree/f698e1e702c0b9124dd677be1bfe3d943266bccc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000002-v1.json","repo":"https://github.com/PranavaKCode/nivat-lean","tags":["math.DS","math.CO","msc:37B10","msc:68R15","symbolic-dynamics","nivat-conjecture","formalization"],"score":0,"title":"Nivat's conjecture: formalization of Pranava Kumar's argument","trust":"high","domain":"math.DS","source":"palomar","authors":["Pranava Kumar"],"reviews":0,"subject":"math.DS","summary":"For every configuration on the integer plane over an arbitrary finite alphabet, a positive k by n rectangle with at most k*n occurring translated patterns forces a nonzero global period of the original configuration. The statement includes equality at the complexity threshold and rectangles of width or height one. The proof formalizes Pranava Kumar's manuscript through Laurent annihilators, a sharp periodic-wedge complexity bound, generating polygons, and selection of the same nonperiodic orbit point throughout the periodic-background construction. Its mathematical setting is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"A proof of Nivat's conjecture","identifier":"https://github.com/PranavaKCode/nivat-lean/blob/3cbea761cbc5cb8039ef1a5990f52be3ba2a23bd/inputs/paper101.pdf","relationship":"formalizes"},{"title":"Rectangular complexity, periodic regions, and local observables","identifier":"https://doi.org/10.5281/zenodo.22666792","relationship":"formalizes"}]}