Square Maximality for Spanning Trees of Induced Grid Subgraphs
Among induced square-lattice graphs on
Abstract
For a finite
with equality exactly for
where
Background. In 1999, Chung obtained boundary-sensitive estimates for spanning-tree counts in lattice subgraphs [Chu99]. In 2010, Swanepoel proposed on MathOverflow that square shapes should maximize the count at fixed cardinality [Swa10]. Procaccia and Tucker-Foltz recorded the conjecture in the research literature in 2022 [PTF22], and Tapp established general boundary-sensitive grid-graph bounds in 2024 [Tap24]. In 2026, Zhang proved exact balancing for free rectangular grids [Zha26a], then extended the extremal result to pure Cartesian-product families with free and periodic boundary conditions and, in the first version of that paper, formulated the induced-subgraph conjecture for all
1 Introduction
Let
We call every finite subgraph of
For positive integers
All logarithms are natural. We use
for Catalan’s constant.
Conjecture 1.1 ([PTF22]). Let
For a graph
so it suffices to consider induced subgraphs. If
Theorem 1.2 (Square maximality). Let
Equality holds if and only if
1.1 Outline of the proof
Theorem 1.2 follows from two finite inequalities carrying the same constant: one compares rectangles of different areas, the other compares a set with its rectangular hull.
-
Rectangular area penalty (Lemma 3.1). For positive integers
with and ,with equality only when
. The proof telescopes in one side length, drawing on the rectangular product and hyperbolic formulas, the trapezoidal estimate, and the residual bounds of [Zha26a]; the individual references are given in Section 3. -
Normalized rectangular-hull inequality (Lemma 4.1). Let
, suppose that is connected, and suppose that the smallest axis-parallel lattice vertex rectangle containing is after translation. ThenInterior vacancy components are controlled by planar duality and Tapp’s bound (Theorem 2.1). Boundary-attached vacancies are handled by Lemma 5.1 and the sliding-window and closed-walk arguments in Section 5.
-
Exact matching and square maximality (Theorem 1.2). If
is connected, , and the smallest axis-parallel lattice vertex rectangle containing is , thenand the two inequalities match exactly:
The strictness of the rectangular estimate forces
, after which equality of cardinalities forces , up to lattice symmetry.
1.2 Related Work
Kirchhoff’s Matrix–Tree Theorem is the classical starting point for exact spanning-tree enumeration [Kir47]. Square-lattice tree entropy and product formulas have been studied extensively; we use the standard closed-walk evaluation recorded, for example, in [SW00]. Tapp proved boundary-sensitive upper and lower bounds for arbitrary finite grid graphs [Tap24]. The rectangular balancing theorem gives the sharp finite comparison within the free rectangular family [Zha26a], while the product-grid extension studies other boundary conditions and higher-dimensional product families [Zha26b].
Organization. Section 2 fixes notation and records the external inputs. Section 3 proves the rectangular estimate. Sections 4 and 5 prove the normalized hull inequality. Section 6 completes the proof of Theorem 1.2, and Section 7 discusses the argument.
2 Preliminaries and Notation
Empty products and
The square-lattice tree entropy is
For
Let
Theorem 2.1 ([Tap24, Theorem 9]). If
We also use two standard facts about spanning trees. First, if
Second, if
The transfer-current theorem represents this probability as a principal minor of a positive semidefinite
kernel [BP93]. Hadamard–Fischer therefore implies that, for an integer
3 Rectangular Area Penalty
We first compare a rectangle whose area is at least
Lemma 3.1 (Rectangular area penalty). Let
Equality holds if and only if
Proof. Both cases below telescope
For
Set
The rectangular product formula, its hyperbolic reduction, and the trapezoidal estimate in [Zha26a, Proposition 2.1, equations (3.1)–(3.2), Lemmas 3.1, 3.2, and 5.1, and equation (5.6)] give
The identification of the integral in the main term with
For positive integers
The same hyperbolic formula gives
and
Since
For integers
The residuals telescope to give
For
therefore gives the uniform bound
Suppose first that
Telescoping (3.3) and using symmetry gives
Substituting (3.3) splits the right side of (3.5) into a
We bound the two in turn.
The area condition
By (3.2) the
In the residual part the subtracted sum is nonnegative, and the first sum is less than
It remains to consider
The
The first residual,
With
Since
If
when
If
Indeed, before the last inequality the right side is at most
which is strictly smaller because
which is (3.1). The first summand is strict when
4 Normalized Rectangular-Hull Inequality
For a finite nonempty
Its minimal rectangular vertex hull is
Thus, after translation, the hull is
Lemma 4.1 (Normalized hull inequality). Let
The proof runs to the end of Section 5. Passing to the planar dual converts the deletion of a set of vertices into the event that a prescribed forest is contained in a uniform spanning tree; the missing vertices are then split into king components, and negative correlation reduces the lemma to one bound per component. Components disjoint from the perimeter are handled below by counting the spanning trees of a union of unit squares in the dual, the rest by the determinant estimate of Section 5.
If
4.1 Dual Contractions
Let
and let
Whenever
Planar tree duality also gives
Call a component nontrivial if it contains at least one edge, and let
where
For
Partition
Here
We record why all deletion graphs used here are connected. Every king component
Applying (4.2) and (2.1) to the disjoint forest edge blocks gives
The factor indexed by
4.2 Interior Vacancy Components
For each
By Theorem 2.1,
For every spanning tree
These events are pairwise incompatible: the union of two distinct spanning trees on the same vertex
set contains a cycle, while
which with the preceding consequence of Tapp’s theorem yields
The argument used that
5 Boundary-Attached Vacancies
What is proved here is a comparison of two determinants. Both
Retain the boundary-vacancy set
Let
index the unit faces of
An interval component is a maximal nonempty set of consecutive integers. Let
Every row and column contains a vertex of
5.1 One-Dimensional Windows
We begin with an elementary interval estimate.
Lemma 5.1. Let
that meet
Proof. A boundary run of length
For an integer
Applying Lemma 5.1 in each row gives
5.2 A Sliding-Window Injection
For an integer
The second ingredient is
It is proved in two steps: each internal interval component of
To prove it, form the full run graph, whose vertices are the maximal vertical runs of
Fix once and for all a rooted spanning tree in every component of the full run graph. Use a
marked run as the root whenever possible, and otherwise use a run in column
If the chosen run is not the root, its parent lies outside the window; otherwise the parent would belong
to the same induced component at a smaller depth. Parent and child lie in adjacent columns. If the parent
is to the left, then
inject into the unmarked vertices of the full run graph. These vertices are exactly the vertically internal
runs of
Every internal interval component of
For integers
Applying Lemma 5.1 vertically and then using (5.1) and (5.2) gives, for every integer
5.3 Closed-Walk Charging
For an integer
Define its partial-sum set by
and set
Let
We use two exact closed-walk sums. The first is the standard square-lattice tree-entropy identity [SW00]:
This series is absolutely convergent:
We include the proof of (5.5). Let
Thus
This reflection is a bijection with unrestricted walks of length
For even
There are no closed words for odd
At
which proves (5.5).
Define
Its bounding face rectangle has
5.4 The Determinant Estimate
Recall that
For
Primal bridges become dual loops and do not affect the determinant. When
The horizontal edges of
Since the graph is connected, Euler’s formula, together with
and therefore
The spectral radius of the rectangular face adjacency is
Since
Both log-determinant series are absolutely convergent by the preceding spectral-radius bound.
The trace difference counts precisely the closed-walk starts in
All terms used below are nonnegative, and (5.4)–(5.5) show that the dominating series are finite. Thus
Tonelli’s theorem justifies the ensuing interchanges of sums. Subtract the two instances of (5.9), substitute
(5.10), and apply the charging bound (5.6). Evaluating the three resulting series by (5.4) and (5.5), the
We have proved the boundary factor
Completion of the proof of Lemma 4.1. Substitute (4.4) and (5.11) into (4.3). Since
Both tree counts are positive because
6 Proof of Square Maximality
Proof of Theorem 1.2. Let
Assume that
Applying Lemmas 3.1 and 4.1 and adding their log-difference estimates gives
This proves the inequality.
If
7 Discussion
The rectangular area penalty bounds the gain available from enlarging the hull, and the normalized hull inequality charges every omitted vertex by exactly the same entropy constant. In log-difference form the two estimates add, their constants cancel, and strictness comes entirely from the rectangular estimate.
Use of AI tools
A substantial part of the reasoning in this paper was developed with the assistance of a large language model. Both runs used Work mode with Speed mode enabled. GPT-5.6 Sol, at the Extra High reasoning setting, worked on the initial prompt below for 87 minutes 7 seconds and returned incomplete results. GPT-5.6 Sol Ultra continued from those results under the shorter follow-up prompt and produced its result after 199 minutes 9 seconds. The raw output became the basis for a substantial part of the present argument, in particular Lemmas 3.1 and 4.1. I manually checked the argument, prepared the bibliography, checked each citation against its source, and wrote the present note. Both prompts are published below.
Current task statement
Let \(\mathcal L\) be the standard nearest-neighbor square-lattice graph with vertex set \(\mathbb Z^2\): distinct vertices \(x,y\in\mathbb Z^2\) are adjacent exactly when \(\|x-y\|_1=1\). For a finite set \(S\subset\mathbb Z^2\), let \(\mathcal L[S]\) be the induced subgraph. For a finite connected graph \(G\), let \(\tau(G)\) denote its number of spanning trees. Set \(\tau(G)=0\) when \(G\) is disconnected. Let
\[
Q_n=P_n\square P_n=\mathcal L[\{0,1,\ldots,n-1\}^2]
\]
be the \(n\times n\) square grid graph, which has \(n^2\) vertices.
Resolve the following conjecture completely in dimension two:
SQUARE-MAXIMALITY THEOREM. For every integer \(n\ge 1\) and every finite set \(S\subset\mathbb Z^2\) with \(|S|=n^2\),
\[
\tau(\mathcal L[S])\le \tau(Q_n).
\]
Moreover, equality holds if and only if \(S\) is an \(n\times n\) lattice square, up to an automorphism of the square lattice; equivalently, up to translation, reflections, and interchange of the two coordinates.
The disconnected case is immediate under the convention \(\tau=0\), so the substantive case is that \(\mathcal L[S]\) is connected. The theorem must cover arbitrary connected induced subgraphs. Shapes may be nonconvex, have holes, have cutvertices or bridges, have disconnected intersections with individual rows or columns, and have long tentacles.
REQUIRED BACKGROUND
Read the following two papers in full before committing to a proof route:
1. https://arxiv.org/abs/2605.23773
2. https://arxiv.org/abs/2606.24016v1
Treat their proved theorems as available background, with precise citation and hypothesis checking. In particular:
- For rectangular grids, if \(AB=ab\) and \(A\le a\le b\le B\), the first paper proves
\[
\log\tau(P_a\square P_b)-\log\tau(P_A\square P_B) \ge \operatorname{arsinh}(1)\bigl((A+B)-(a+b)\bigr),
\]
with strict inequality unless the two rectangles agree. Consequently, \(Q_n\) is already the unique maximizer among rectangular grids with \(n^2\) vertices.
- The second paper proves the analogous perfect-power result within pure Cartesian-product families and states the induced-subgraph conjecture above as its \(d=2\) case.
- Every connected induced \(n^2\)-vertex lattice subgraph satisfies
\[
|E|\le 2n(n-1), \qquad |E|-|V|+1\le (n-1)^2,
\]
with equality only for \(Q_n\). These edge-count and cycle-rank facts are useful but are explicitly too coarse by themselves.
- The product-spectrum and hyperbolic-residual arguments in the papers rely essentially on Cartesian-product structure. Do not silently extend them to arbitrary induced subgraphs without a new comparison theorem and complete error control.
You may use standard results such as Kirchhoff's Matrix-Tree Theorem, the weighted matrix-tree theorem, Rayleigh monotonicity, the transfer-current theorem, Wilson's and Aldous-Broder algorithms, planar duality for spanning trees, Schur complements, determinant identities, Cauchy-Binet, and standard majorization or rearrangement theorems. Every invoked result must nevertheless be stated precisely enough that its hypotheses and the direction of its implication can be audited.
For this benchmark, work under the premise that an exact affirmative finite proof is available to be found. A response that only labels the conjecture open, difficult, plausible, asymptotically supported, or computationally verified is not responsive. If exact integer calculations produce a genuine counterexample, that supersedes the premise and gives a complete negative resolution; approximate numerical evidence does not.
The finished argument must establish the stated theorem for every \(n\ge1\), including all equality cases. It may not impose extra conditions such as simple connectivity, orthogonal convexity, row- or column-convexity, bridgelessness, bounded aspect ratio, or product structure.
WHAT DOES NOT COUNT
Intermediate advances are useful internally, but the delivered solution must settle the whole theorem. None of the following, standing alone, is an acceptable endpoint:
- proving only the rectangular, Ferrers, Young-diagram, convex, simply connected, or hole-free cases;
- proving an asymptotic inequality, an inequality only up to \(e^{o(n^2)}\), or a statement only for sufficiently large \(n\);
- observing that the square minimizes boundary or maximizes edges, average degree, face count, or cycle rank;
- applying a general upper bound on \(\tau(G)\) that remains above \(\tau(Q_n)\);
- asserting without proof that a compression, symmetrization, hole-filling operation, or boundary-vertex transfer increases the number of spanning trees;
- reducing the theorem to a new lemma that is equivalent or nearly equivalent in strength, without proving that lemma;
- proving a comparison for one eigenvalue or a few spectral moments while the full determinant comparison remains missing;
- computational verification through any fixed \(n\), or floating-point determinant comparisons;
- omitting strictness or the equality case;
- invoking a theorem whose hypotheses fail for induced lattice subgraphs with holes, bridges, cutvertices, or nonsimple planar duals.
MULTIAGENT RESEARCH MANAGEMENT
Exploit multiagent v2 at full scale, coordinating as many as 64 simultaneous agents when useful. Allocate agents adaptively rather than reserving a predetermined number for each strategy. Launch the search with a broad collection of mathematically independent directions. In the early stages, keep the leading hypothesis private from most agents so that the group does not collapse onto one seductive but incomplete route. The initial collection should span genuinely different mechanisms, including:
- Minimal-counterexample and structural induction. Try to prove that an extremizer has no holes, no bridges, interval row or column sections, orthogonal convexity, or some other structure that eventually forces a rectangle.
- Lattice-specific compressions and local vertex transfers. Derive exact determinant or effective-resistance formulas for moving an exposed vertex into a concavity while preserving cardinality, connectedness, and inducedness.
- Grounded-Laplacian determinant comparison. Explore Schur complements, rank-one or low-rank updates, log-determinant inequalities, Gaussian-free-field integral representations, and weighted interpolations between shapes.
- Heat-trace or spectral-zeta comparison. Seek a valid rearrangement inequality strong enough to integrate to the determinant, while explicitly testing whether pointwise heat-trace domination is even true.
- Planar methods. Explore dual spanning trees, deletion-contraction in the primal and dual, the Temperley bijection, Kasteleyn determinants, dimers, electrical networks, and face-by-face transformations, with explicit treatment of holes and bridges.
- Uniform-spanning-tree and random-walk methods. Explore Wilson and Aldous-Broder, transfer currents, loop-erased random walk, and a sharp extension of Tapp's multiplier and escape-probability framework.
- Graphic-matroid and tree-polynomial methods. Explore basis-generating polynomials, strong log-concavity, negative dependence, injections between spanning-tree sets, and lattice-aware edge-exchange maps.
- Extremal graph theory constrained by the lattice. Explore degree sequences, planar embeddings, block decompositions, and bounds that exploit lattice geometry rather than merely maximum degree.
- Exact computation for discovery and falsification. Enumerate small lattice animals up to translation and lattice symmetry, compute \(\tau\) by exact integer determinants, test proposed local moves, and locate the first failure of every candidate sublemma.
Regard this as a menu of independent research programs, not as an indication that one route is intended. Sustain several mutually incompatible proof architectures over multiple rounds.
Two especially clean possible endgames are:
1. Construct a finite sequence of shape operations that preserves the admissible class, never lowers \(\tau\), is strictly improving away from a square, and terminates at \(Q_n\).
2. Prove a direct determinant or tree-count inequality valid for every admissible \(S\), with equality precisely at \(Q_n\).
Any other fully rigorous architecture is equally valid.
Keep a live research ledger indexed by genuine mathematical mechanism. Each entry should record:
- the key statement in fully quantified form;
- the exact role that statement would play in a complete proof;
- every hypothesis on which it depends;
- exact computational experiments already run;
- counterexamples to natural stronger versions;
- the narrowest unresolved step;
- a status tag such as active, blocked, disproved, or merged.
Classify routes by mathematical content rather than cosmetic differences in presentation. When too many agents cluster around one idea, move some of them to neglected directions. Elegance of a reduction is not evidence of completion: a route that merely renames the main difficulty as a “compression theorem,” “rearrangement principle,” or “extremal-domain lemma” has made little progress until that statement is proved. If a program reaches a missing lemma essentially as hard as the original theorem, freeze that program. Resume it only after a new invariant, construction, exact identity, or induction mechanism appears.
Delay cross-fertilization until independently developed routes are mature enough that their actual advantages and defects are visible. Demand mathematical artifacts from every agent: complete lemma proofs, exact formulas, determinant quotients, resistance estimates, explicit tree maps, certified counterexamples to subsidiary claims, or finite certificates that another agent can check. Discard vague progress summaries, unsupported confidence, continuum analogies with no finite discretization, and assertions that a global compatibility step is automatic.
All computational evidence used in reasoning must be exact. Suitable tools include fraction-free Bareiss elimination, symbolic determinants, and independently reproduced integer Matrix-Tree calculations. Use computation to reveal patterns and destroy false claims, not as a substitute for the uniform proof. Archive the coordinates and exact tree counts of every shape that refutes a proposed local rule.
ADVERSARIAL AUDIT REQUIREMENTS
Maintain dedicated skeptical review throughout the search. Every prospective proof must survive checks for the following errors:
- confusing a vertex set in \(\mathbb Z^2\) with a polyomino made of unit cells, thereby shifting the graph or miscounting vertices, faces, or boundary;
- inferring a tree-count comparison from boundary size or edge count when the graphs are not nested;
- invoking Rayleigh monotonicity without a valid common network and an actual conductance increase;
- using a vertex relocation that changes cardinality, breaks connectedness, fails to produce an induced subgraph, leaves an isolated component, or has no well-founded termination measure;
- comparing cofactors based on inconsistent roots or vertex identifications;
- dropping the Laplacian zero mode, the Matrix-Tree normalization, or a sign in a determinant or heat-kernel integral;
- asserting coordinatewise eigenvalue order or spectral majorization rather than proving it;
- using planar duality while ignoring bridges, dual loops, parallel dual edges, holes, the unbounded face, or disconnected collections of faces;
- proposing a combinatorial tree map without a complete proof of well-definedness and of injectivity or surjectivity as required;
- establishing weak monotonicity but leaving unexplained nonsquare equality cases;
- replacing the target by an equivalent “domain monotonicity,” “compression,” or “entropy” assertion and treating that assertion as known;
- using an asymptotic expansion to decide finite changes whose logarithmic gain can stay bounded;
- relying on computed positivity without a symbolic estimate uniform in \(n\).
Every proposed geometric move must come with a full certificate containing:
1. its precise definition on lattice vertex sets;
2. preservation of \(|S|\) and of the induced-subgraph interpretation;
3. preservation of connectedness, or a complete analysis of any exceptional case;
4. an exact formula for the resulting tree-count ratio or difference;
5. a proof of its sign in every allowed configuration;
6. the full characterization of equality;
7. a well-founded quantity that guarantees termination;
8. proof that terminal configurations are exactly the squares, or a justified final passage to the established rectangular theorem.
Every determinant, spectral, or heat-kernel route must supply:
1. the precise matrices or operators;
2. a common ambient space, or a rigorous embedding or intertwining construction;
3. correct handling of the zero eigenvalue and all normalization factors;
4. a proved Loewner, majorization, trace, or integral comparison with the needed orientation;
5. convergence and endpoint estimates for all integral formulas;
6. equality conditions propagated through every step.
The coordinating agent should repeatedly combine results, attack them, redirect effort, and initiate further rounds. A failed opening round is not a stopping condition. Once a serious lemma emerges, send independent agents to seek separate proofs, construct exact counterexamples, analyze equality, and test whether the lemma merely restates the target. Retain multiple distinct routes until one closes the entire argument.
Before endorsing a proof, commission a clean-room review by agents who did not build it. They must reconstruct the dependency graph, verify citations and algebra, test local assertions on exact small examples, and actively try to break the proof. Correct all defects and repeat this review until no gap remains.
FINAL-ANSWER REQUIREMENTS
Return a self-contained, publication-quality mathematical proof, not a research diary. The final response must:
- state the theorem precisely;
- define all notation;
- state and prove every new lemma in dependency order;
- identify precisely which results are cited from the two supplied papers or standard literature;
- prove the inequality for every \(n\ge1\);
- separately prove the equality characterization;
- include exact finite verification only where genuinely needed for finitely many base cases;
- contain no unsupported “clearly,” “routine,” or “by symmetry” at a substantive step;
- contain no appeal to the multiagent process, numerical evidence, or the premise that a proof exists.
Failure of the current collection of ideas is not a reason to terminate. Start additional rounds and revisit frozen routes only when a substantively new device appears. Deliver the main answer only after a complete argument has passed the independent audit.
If a nonnegotiable execution limit interrupts the investigation, never disguise a conjectural chain as a proof. Report only rigorously established lemmas, exact failures of attempted routes, and a single precisely formulated outstanding obstacle, all clearly marked incomplete. This is an emergency fallback, not a chosen endpoint.
Allocate no less than eight hours of sustained search before considering termination. Internet lookup is permitted for the two supplied papers, routine background, and standard named results. Do not use web search to hunt for a preexisting solution to this exact benchmark, and do not substitute an “open problem” report for the requested investigation.
Please build upon these initial results and resolve the conjecture. Aim for a breakthrough and consider a diverse set of approaches, not limited by previous work. Please try for at least 8 hours before returning an incomplete result.
I am deeply grateful to Sloan Nietert for many helpful suggestions and insightful discussions. I also thank him for collaborating with me on the prompting strategy for this problem and, in particular, for his “breakthrough” prompt.
Final verification (August 22, 2026). The square-maximality theorem as stated here for arbitrary finite square-lattice subgraphs, together with its equality characterization and complete proof chain, has been formalized in Lean 4 and checked by the Lean kernel. The formalization and its reproducible trust audit are available in the public repository. I also completed a paper-to-Lean specification audit matching the definitions, hypotheses, intermediate results, and conclusions in the formalization to the mathematical claims in this manuscript.
Palomar registration (August 23, 2026). The Lean verification has been registered in the Palomar Registry at a fixed commit of the public submission repository. The registration metadata records the role of the model and the subsequent human and kernel-level checks.
References
- [BP93] Robert Burton and Robin Pemantle. Local characteristics, entropy and limit theorems for spanning trees and domino tilings via transfer-impedances. The Annals of Probability, 21(3):1329–1371, 1993. doi:10.1214/aop/1176989121.
- [Chu99] Fan R. K. Chung. Spanning trees in subgraphs of lattices. In Applications of Curves over Finite Fields, volume 245 of Contemporary Mathematics, pages 201–219. American Mathematical Society, 1999. doi:10.1090/conm/245/03734.
- [Kir47] Gustav Kirchhoff. Ueber die Auflösung der Gleichungen, auf welche man bei der Untersuchung der linearen Vertheilung galvanischer Ströme geführt wird. Annalen der Physik, 148(12):497–508, 1847. doi:10.1002/andp.18471481202.
- [PTF22] Ariel D. Procaccia and Jamie Tucker-Foltz. Compact redistricting plans have many spanning trees. In Proceedings of the 2022 Annual ACM-SIAM Symposium on Discrete Algorithms, pages 3754–3771. SIAM, 2022. doi:10.1137/1.9781611977073.148.
- [SW00] Robert Shrock and F. Y. Wu. Spanning trees on graphs and lattices in
dimensions. Journal of Physics A: Mathematical and General, 33(21):3881–3902, 2000. doi:10.1088/0305-4470/33/21/303. - [Swa10] Konrad J. Swanepoel. Comment on “Number of spanning trees in a grid.” MathOverflow, January 7, 2010.
- [Tap24] Kristopher Tapp. Spanning tree bounds for grid graphs. The Electronic Journal of Combinatorics, 31(1):P1.26, 2024. doi:10.37236/12130.
- [Zha26a] Jiechen Zhang. The balancing theorem for spanning trees of rectangular grid graphs. arXiv preprint arXiv:2605.23773, 2026. arXiv:2605.23773.
- [Zha26b] Jiechen Zhang. Extremal spanning trees in product grid graphs. arXiv preprint, 2026. arXiv:2606.24016v1 (original conjecture); v2 (revised version).