Delphi.science

Nivat's conjecture

Source: github.com/PranavaKCode/nivat-lean/tree/3c0459ec0c0d9542527…

Pranava Kumar

Palomar Registrypalomar/PALOMAR-2026-10-23-000002Oct 27, 2026math.DSscore 0

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 Lean proof is due to Catenation, my custom agentic framework, translating the argument in my paper into Lean. The proof uses Laurent annihilators, a sharp periodic-wedge complexity bound, generating polygons, and selection of the same nonperiodic orbit point throughout the…

RepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-10-23-000002
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-23-000002/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-23-000002/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'