Orthodox queen domination: finite constructions and an asymptotic density gap
Yixiang Kong
math.CO
Sep 1, 2026 · v2
TL;DR
The main orthodox queen domination density bound (Theorem 2.3) is fully formalized in Lean 4 with Mathlib, supplemented by exact Python checks.
Abstract
An orthodox dominating set on an $n\times n$ chessboard occupies every row of one parity and every column of a possibly different parity. For $n\ge400001$, every such set contains more than $(1/2+1/80000)n-2$ queens, on odd and even boards and with attacking or boundary queens allowed. Second-moment estimates and an exact rational line-weight certificate give a stronger bound for $p$-covers; finite diagonal completion and board extension transfer it to orthodox covers. The cost of extending an arbitrary dominating set to an orthodox cover yields an inequality with an explicit defect term. The previously constructed independent, border-free Type-A $1$-cover of $Q_{221}$ with $111$ queens supplies a finite seed. Classical amplification gives ordinary and independent domination upper bounds with coefficients $112/221$ and $113/221$, respectively. Its order 221 is below the density threshold 400001. For admissible seeds whose orders tend to infinity, the lower limit of these coefficients is at least $1/2+1/16000$.
Problem
Orthodox dominating sets on an n×n chessboard occupy every row of one parity and every column of a possibly different parity. The question is how far their minimum size must exceed n/2 for large n.
Approach
Second-moment estimates on the indices of required lines constrain the diagonal structure of p-covers. An exact rational piecewise-linear line-weight certificate, verified by exact evaluation at cell vertices, gives a weak-duality capacity bound on a subset with distinct line indices. Diagonal completion and board extension then transfer the p-cover bound to relaxed and orthodox covers. A finite independent Type-A seed on Q_221 is amplified to give upper bounds.
Results
For n ≥ 400001, every orthodox cover has more than (1/2+1/80000)n−2 queens, and p-covers satisfy a stronger 1/2+1/16000 density bound. The paper also gives the upper bounds γ(Q_N) ≤ 112/221 N + O(1) and i(Q_N) ≤ 113/221 N + O(1). Theorem 2.3 is fully formalized in Lean 4 with Mathlib.
