Nonintersecting Unit Diagonals in Odd Square Arrays
Luyu Song
math.CO
Oct 16, 2026 · v1
TL;DR
Formalizes in Lean 4 with Mathlib the upper-bound reduction from diagonal selections to isometric grid path covers, assuming the Fisher–Fitzpatrick bound as a hypothesis.
Abstract
Let $D(n)$ be the maximum number of unit-square diagonals in an $n\times n$ square array such that no two selected diagonals share an endpoint and no unit square contains both diagonals. We prove that, for every odd positive integer $n$, $D(n)=n(n+1)/2+\lfloor(n+1)/6\rfloor$. The matching lower bound was established by Boyland, Roth, Pintér, Laukó, Schoenfield, and Wasielewski. We obtain the upper bound by transforming any admissible selection $M$ in a $(2k-1)\times(2k-1)$ square array into an isometric path cover of the $k\times k$ vertex grid with at most $2k^2-|M|$ paths. An auxiliary matching decomposes the original vertices into alternating paths. On each such path, all segments between blocks are either of type $da$ or of type $bc$. Projecting these paths to the block grid gives coordinate-monotone sequences, which become geodesics when diagonal steps are expanded. The Fisher–Fitzpatrick theorem then yields the sharp upper bound. We also describe a Lean verification of the upper-bound reduction, with the grid-cover theorem supplied as an explicit hypothesis.
Problem
D(n) is the maximum number of unit-square diagonals in an n×n array such that no two share an endpoint and no square contains both of its diagonals. The even case and a lower bound for odd n were known, but the odd-n formula remained a conjecture (OEIS A264041).
Approach
Any admissible selection in a (2k-1)×(2k-1) array is transformed into an isometric path cover of the k×k vertex grid with at most 2k^2-|M| paths. An auxiliary matching inside 2×2 blocks decomposes the vertices into alternating paths of uniform type, and these project to coordinate-monotone geodesics. The Fisher–Fitzpatrick theorem then gives the bound. A Lean 4.19.0 project with a pinned Mathlib dependency verifies the reduction, taking the Fisher–Fitzpatrick bound as an explicit hypothesis.
Results
For every odd n, D(n) = n(n+1)/2 + ⌊(n+1)/6⌋. The Lean formalization covers the diagonal encoding, route types, acyclicity, component count and cover transformation, but not the published lower-bound construction or the grid-cover theorem. A Python script checks lower-bound configurations for odd n up to 99.
