{"id":"palomar/PALOMAR-2026-10-23-000017","url":"https://github.com/novou/spanning-tree-isoperimetry-lean/tree/ab2ab3932cfad3eeac9a9f75d29c8982cffad54d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000017-v1.json","repo":"https://github.com/novou/spanning-tree-isoperimetry-lean","tags":["math.CO","cs.DM","msc:05C05","msc:05C35","msc:05C50","msc:05A16","spanning-trees","square-lattice","isoperimetry"],"score":0,"title":"Spanning-Tree Maximization Forces Isoperimetry in the Square Lattice","trust":"high","domain":"math.CO","source":"palomar","authors":["Jiechen Zhang"],"reviews":0,"subject":"math.CO","summary":"Lean formalization of spanning-tree maximization over finite connected induced subgraphs of the square lattice. The development establishes edge isoperimetry of every maximizer, the maximum count and all maximizing lattice-isometry classes at every positive cardinality, and uniqueness of the canonical corner-strip domain for N >= 18. Nonuniqueness occurs exactly at N = 3, 8, 10, 13; the canonical count has exceptions at N = 7, 14, 17. It also establishes the sharp square-cardinality stability inequality, an exact scalar product formula and rational recurrence for corner-strip counts, the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Spanning-Tree Maximization Forces Isoperimetry in the Square Lattice","identifier":"https://arxiv.org/abs/2605.23773v3","relationship":"formalizes"},{"title":"Determinant computations for some classes of Toeplitz-Hankel matrices","identifier":"https://arxiv.org/abs/0804.3073v1","relationship":"adapts"}]}