# Verification report — AMR-122-0012 (Propp, Problem 12: the sum of the entries of the inverse Kasteleyn–Percus matrix of the Aztec diamond)

Verification date: 2026-10-18 (first version 2026-10-17; run C, which examined the final text, added on 2026-10-18).

**Verdict.** The note gives a **complete answer**: Propp's formula is proved for every order n ≥ 1.
- **Settled.** Let K_n be the Kasteleyn–Percus matrix of the Aztec diamond A_n of order n (rows: black squares,
  columns: white squares; entry −1 on every vertical domino whose white square is on top, +1 on the other dominoes).
  Then the sum of all entries of K_n^(−1) is (n+1)²/2 − 2^(n−1) = (n−1)(n+3)/2 − 2^(n−1) + 2 (Theorem 1.2).
  Moreover every row sum and every column sum of K_n^(−1) is an explicit Krawtchouk coefficient:
  (1 − κ_n((s+1)/2, t/2))/2 at the white square with coordinates (s, t), and (1 − κ_n((t+1)/2, s/2))/2 at the black
  square with coordinates (s, t), where κ_n(m, k) = [ξ^m](1 − ξ)^k (1 + ξ)^(n−k) (Corollary 1.3); in particular
  they lie in (1/2)Z.
- **Method.** K_n maps the constant 1/2 on the white squares to 1 at every black square except the n black squares
  of one edge Σ_S (Lemma 3.1); two transpositions give S_n = n(n+1)/2 + n/2 + (sum of K_n^(−1)1_{Σ_S} over the n
  white squares of an adjacent edge Σ_N) (Proposition 3.2); in rotated coordinates the vector K_n^(−1)1_{Σ_S} is
  −(1/2)κ_n((s+1)/2, t/2), proved by two polynomial identities (Lemma 4.2, Proposition 4.3); on Σ_N its values are
  −C(n, m)/2. The only input from the literature is the invertibility of K_n (Kasteleyn–Percus, with the count
  2^(n(n+1)/2) of Elkies–Kuperberg–Larsen–Propp), which the problem presupposes.
- **Credit.** The problem and the formula are Propp's (stated from computations for n ≤ 8). The matrix and the
  determinant method are due to Kasteleyn (1961; exposition for general planar graphs 1967) and Percus (1969); the
  Aztec diamond and its 2^(n(n+1)/2) domino tilings to Elkies, Kuperberg, Larsen and Propp (1992). Explicit formulas
  for the individual entries of the inverse Kasteleyn matrix of the Aztec diamond, as sums of products of Krawtchouk
  coefficients, are due to Helfgott (Brandeis thesis 1998, arXiv:math/0007136, 2000), whose coupling function differs
  from the inverse by an explicit sign factor (Remark 6.2), extended by Chhita, Johansson and Young (Ann. Appl.
  Probab. 25 (2015)) to different weights for horizontal and vertical dominoes; neither computes the entry sum or the
  row sums, and neither mentions Problem 12.
- **What the note adds.** An elementary proof of Propp's identity by an explicit solution of K_n u = 1, and the row
  and column sums of K_n^(−1).
- **Not claimed.** No priority: Propp expected the identity to follow from Helfgott's work, and specialists may
  regard it as a routine consequence of the known formulas. Other choices of the Kasteleyn signs are not covered
  (they give other sums, Remark 6.1).

The note is unrefereed.

## Statement checked
- **Primary source, 1998.** J. Propp, "Twenty open problems in enumeration of matchings", arXiv:math/9801060 (title
  page: December 9, 1996, last revised September 2, 1998), Problem 12. Read in the arXiv LaTeX source. The matrix is
  the Kasteleyn matrix of the Aztec diamond of order n "in which every other vertical domino has its sign flipped",
  the corresponding 1's of the bipartite adjacency matrix being replaced by −1's; Problem 12 asks to show that the sum
  of the entries of the inverse is (n−1)(n+3)/2 − 2^(n−1) + 2; the text adds that the formula works for n = 1 through
  n = 8 (no values are printed).
- **Primary source, 1999.** J. Propp, "Enumeration of matchings: problems and progress", in New Perspectives in
  Algebraic Combinatorics (Berkeley, CA, 1996–97), Math. Sci. Res. Inst. Publ. 38, Cambridge University Press, 1999,
  pp. 255–292 (pages and DOI 10.1017/9781009701587.008 from Crossref; the arXiv journal reference gives 255–291);
  arXiv:math/9904150, read in the LaTeX source. The convention is fixed: −1 on "every vertical domino with its white
  square on top", relative to a fixed checkerboard colouring. Problem 12 has the same formula. Progress paragraph
  (paraphrase): Helfgott has solved "a similar problem" with the main result of his thesis; Problem 12 can probably
  be proved similarly; Helfgott's thesis uses a different sign convention, which gives different signs and "a
  different sum" for the inverse; Kuperberg and Zare have ideas on inverses of Kasteleyn–Percus matrices. No proof
  is given; the problem was open in 1999.
- **Progress report.** J. Propp, "Twenty open problems in enumeration of matchings: progress report",
  arXiv:math/9801061 (dated September 2, 1998): entries for several problems, none for Problem 12.
- **Corpus record.** ulamai/UnsolvedMath, record AMR-122-0012 (dataset version 1.8.0; status open; proposer Propp;
  source arXiv:math/9801060, Problem 12). The record statement is the 1998 text of Problem 12.

## Readings
- **The 1999 convention** (−1 exactly on the vertical dominoes with the white square on top): this is the matrix of
  the note. The remaining choices — which checkerboard colouring, which colour indexes the rows, and the mirror
  convention "white square at the bottom" — do not change the entry sum (Lemma 2.3; also checked exactly for n ≤ 8).
- **The second reading of the 1998 wording** (−1 on all vertical dominoes of every other column): also a Kasteleyn
  signing, but its entry sums are 1, 5/2, 4, 6, 9, 25/2, 16, 20 for n = 1..8 (either choice of the columns), which
  differ from the formula for n = 4..8. It is excluded by the 1999 text and by Propp's statement that the formula
  works for n ≤ 8 (Remark 2.4).
- **Other matrices.** The 2N × 2N symmetric matrix [[0, K],[Kᵀ, 0]] would have entry sum 2S_n and the
  skew-symmetric version 0; the problem explicitly concerns the signed bipartite adjacency matrix. Other Kasteleyn
  signs (gauges) give other sums (Remark 6.1); weighted Aztec diamonds are not treated.

## Results in the paper
- **Theorem 1.2** (the formula for every n ≥ 1): proved (Section 5).
- **Corollary 1.3** (row and column sums of K_n^(−1)): proved (Section 5).
- **Lemma 2.1** (coordinates p = x + y + n, q = x − y + n; colours; neighbours on the four edges; colours of the
  edges), **Lemma 2.3** (independence of the conventions), **Lemma 3.1** (K_n(1/2) = 1_B − 1_{Σ_S},
  K_nᵀ(1/2) = 1_W − 1_{Σ_N}), **Proposition 3.2** (reduction to the Σ_N × Σ_S block), **Lemma 4.1** (corner
  coordinates s, t), **Lemma 4.2** (the two polynomial identities), **Proposition 4.3** (the explicit solution
  φ = K_n^(−1)1_{Σ_S}): proved.
- **Proposition 2.2** (|det K_n| = 2^(n(n+1)/2)): the geometric part is proved in the note (every bounded face of the
  dual graph is the 4-cycle of a 2 × 2 block, which carries exactly one −1); the determinant statement is
  Kasteleyn's theorem in Percus's form, and the count is Elkies–Kuperberg–Larsen–Propp; both are cited.
- **Remark 5.1** (a second evaluation of S_n from the sum of φ over all white squares): proved; added at the writing.
- **Remarks 2.4, 6.1** (other signs give other sums; explicit gauges; where the convention enters Lemma 3.1) and
  **Remark 6.2** (Helfgott's formula and its sign factor): computations and readings of the literature, not used in
  the proofs.
- **Not included.** An observation on the individual entries of the Σ_N × Σ_S block of K_n^(−1) (a closed form
  checked for n ≤ 11, not proved) is not part of the note.

## Computations (sanity and exactness checks; program and output in reproducibility/)
No statement of the note depends on a computation. `check_note.py` (Python 3, standard library, exact arithmetic,
about 2 seconds; recorded output `check_note_output.txt`, 38 checks, all passed) builds K_n from the definition and
checks: Lemmas 2.1 and 4.1 and the block condition of Proposition 2.2 (n ≤ 30); Lemma 3.1 (n ≤ 30); Lemma 4.2
(n ≤ 30); K_n(2φ) = 2·1_{Σ_S} and K_nᵀ(2ψ) = 2·1_{Σ_N} (n ≤ 30); the values −C(n, m)/2 on Σ_N, Proposition 3.2 with
the closed form, the formula and Remark 5.1 (n ≤ 30); the exact inverse for n ≤ 8 (K_n K_n^(−1) = I,
|det K_n| = 2^(n(n+1)/2), entry sums 1, 5/2, 4, 9/2, 2, −15/2, −32, −175/2, the block sum 1/2 − 2^(n−1), all row and
column sums as in Corollary 1.3); Lemma 2.3 (n ≤ 8); the alternate-columns sums 1, 5/2, 4, 6, 9, 25/2, 16, 20 and
the Kasteleyn–Wilson sums 1, 5/2, 11/2, 8, 13, 31/2, 45/2, 23 (both readings of the row), each with an explicit
±1 gauge to K_n and a consistency check against the exact inverse (n ≤ 8); four negative controls (all detected).
The folder `reproducibility/independent_run_2/` contains the programs and recorded outputs of run C (below).

## Independent verification runs
The result was first obtained with a written proof and exact programs (S_n by exact elimination for n ≤ 8; the
explicit vectors against the exact inverse for n ≤ 9; the equations for the explicit vectors exactly for n ≤ 40;
S_n in floating point for n ≤ 26). Two independent verification runs, both AI-assisted, followed; each re-derived
the proof step by step and wrote its own programs, and neither read the other's report.
- **Run A** (statement and proofs). Read both versions of Propp's text anew and checked the record against the 1998
  text. Re-derived the coordinates and the neighbour table, both "constant 1/2" statements for both parities of n,
  the reduction, the corner coordinates, the explicit solution (index map, existence conditions, the identities, the
  cases m = 0, 1 ≤ m ≤ n − 1, m = n and n = 1), the conclusion, the row and column sums, and the symmetries. Own
  programs: exact S_n for n ≤ 9 for −1 on the white-on-top and on the white-at-bottom dominoes and for the
  alternate-columns signs, in both colourings (formula values 1, 5/2, 4, 9/2, 2, −15/2, −32, −175/2, −206 for the
  first two; 1, 5/2, 4, 6, 9, 25/2, 16, 20, 25 for the third; |det| = 2^(n(n+1)/2) in all 72 cases); the explicit
  vectors, the edges and the constant-1/2 statements for n ≤ 60 and against the exact solutions for n ≤ 8; the
  identities symbolically for n ≤ 15. Re-ran the original programs with consistent results. Verdict: confirmed,
  complete answer. Required fixes: (1) the statement that "black square on top" is the only other reading of the
  1998 wording was incomplete — the alternate-columns reading exists, gives other sums from n = 4 on and is excluded
  by Propp's n ≤ 8 data; (2) the values 1, 5/2, … are the values of the formula, not values printed by Propp;
  (3) (optional) state the geometric fact behind the Kasteleyn signing or cite Kasteleyn–Percus and
  Elkies–Kuperberg–Larsen–Propp for invertibility. All three were done (Remark 2.4; Section 1.1 and the caption of
  Table 1; Proposition 2.2 with its proof).
- **Run B** (independent computation, literature). Built the matrix independently; exact S_n for n ≤ 12 in both
  colourings, certified by the exact residual and the determinant; the full exact inverse summed for n ≤ 8; the
  explicit vectors on its own matrix for n ≤ 60; S_n modulo two primes for n ≤ 40; other signs (alternate columns,
  Helfgott's Kasteleyn–Wilson signs, a complex convention) and random ±1 gauges, all giving other sums; negative
  controls; the original programs re-run with byte-identical outputs. Literature: Helfgott read in full;
  Chhita–Johansson–Young, Chhita–Young and Lai searched in full text; arXiv, zbMATH Open, Crossref and Semantic
  Scholar searches; three web searches. Verdict: confirmed, complete answer. Required fixes: (1) as A(1); (2) full
  bibliographic data for Kasteleyn 1961, Percus 1969, Elkies–Kuperberg–Larsen–Propp 1992 and the published version
  of Lai's survey; (3) nothing to be claimed about Helfgott's signs beyond what was computed. All were done
  (Remark 2.4; references.bib, checked with Crossref; Remark 6.2 states the source-level sign factor of Helfgott's
  Proposition 9 and the computed comparison only, and says that the gauge relating the two was not determined).
- **Run C** (final text; 2026-10-18; programs and outputs in `reproducibility/independent_run_2/`). Examined the
  written note, including the parts added at the writing (Remark 5.1, the gauges and the last sentences of Remark 6.1,
  Remark 6.2, Figure 1, `check_note.py`). Read again Problem 12 in both versions of Propp's text with the 1999
  progress paragraph (arXiv LaTeX sources), Helfgott's Sections 1 and 2 (LaTeX source, including the definition of the
  Aztec diamond in coordinates, Lemma 1, the sign computation before Proposition 9, Proposition 9, Corollary 10,
  Theorem 11) and the EPS source of his Figure 17, and the abstract of Chhita–Johansson–Young. Re-derived every lemma,
  proposition and proof from the text as written, including the geometric part of Proposition 2.2 (every edge lies in
  the named 2 × 2 block; the unit squares are those centred at (i, j) with |i| + |j| ≤ n − 1; star-shaped union; the
  bounded faces are exactly these squares) and Remark 5.1; found no error. Own programs (exact arithmetic, another
  encoding of the diamond): Lemmas 2.1, 3.1, 4.1, 4.2, Propositions 3.2 and 4.3, Corollary 1.3 and Remark 5.1 for
  n ≤ 40; the exact inverse for n ≤ 8; S_n for n ≤ 10 in both colourings, with the −1 on top or at the bottom, and for
  the transposes (1, 5/2, 4, 9/2, 2, −15/2, −32, −175/2, −206, −903/2); Lemma 4.2 symbolically for n ≤ 12; the faces of
  the plane graph of Proposition 2.2 traced from its rotation system for n ≤ 25; the sums, gauges and the analysis of
  the interior squares of Remarks 2.4 and 6.1 for n ≤ 8; Figure 1 against the tikz code; Helfgott's Proposition 9,
  Corollary 10 and coupling function against the exact inverse of his matrix for n ≤ 7 (see "Closest prior work").
  Re-ran `check_note.py` from the release archive: output identical except the timing field. Verified the ten DOIs with
  Crossref and repeated the literature search (arXiv, zbMATH Open, Crossref, OpenAlex, one web search). Verdict:
  confirmed, complete answer; no mathematical fix. Required fixes: the account of Helfgott's signs in Remark 6.2 and
  the credit to Helfgott in the abstract made precise (his Proposition 9 is in the same normalisation as K_n; only the
  coupling function differs, by the sign factor); Kasteleyn's exposition of 1967 cited next to Kasteleyn 1961 and
  Percus 1969; the date; the Verification paragraph (the requirement on Helfgott's signs had come from the writing
  stage, not from run B). All were done.

## Relation to the literature, novelty and scope
- **Closest prior work.** Helfgott, arXiv:math/0007136 (2000; Brandeis thesis 1998): Proposition 9 gives every entry
  of the inverse of his Kasteleyn matrix of the Aztec diamond as (−1)^(d0+d1+w1) 2^(−n) times a sum of products of
  two Krawtchouk coefficients (Corollary 10: the remaining cases); the coupling function of his main result
  (Theorem 11) omits this sign, which is of product form (a gauge). Helfgott's kr(m, n, k) is the note's κ_n(m, k).
  Run B found that the coupling function, transcribed with coordinate ranges inferred from the formula, has for n ≤ 7
  the same multiset of absolute values as K_n^(−1) but other signs. Run C resolved the relation: Helfgott's matrix
  (the vertical-edge-count signing of his Section 2.1, used from his Section 2.4 on) coincides edge for edge with the
  matrix of Problem 12 in the note's colouring for even n and in the other colouring for odd n (in every pair of
  adjacent rows the lower square of the leftmost vertical domino has x + y ≡ n mod 2; both signings alternate along
  the row), so the entry sum of its inverse is S_n for every n by Lemma 2.3; with the coordinates read from the source
  of his Figure 17, Proposition 9 and Corollary 10 with the sign factor reproduce every entry of the inverse of his
  matrix for n ≤ 7 (for one of the two orientations of the board left open by the text; up to a gauge for the other),
  and the coupling function has the entry sums 1, 1/2, 4, 11/2, 16, 57/2, 64 for n = 1..7. So the omitted sign factor
  is exactly the gauge between his coupling function and K_n^(−1), and Theorem 1.2 is equivalent to a double-sum
  identity for his formula, which the note does not evaluate. Which convention of the 1998 thesis Propp's remark on
  "a different sum" refers to cannot be decided from the texts (the coupling function and the Kasteleyn–Wilson matrix
  of his Section 2.1 both give other sums). Helfgott computes neither the entry sum nor the row sums and does not
  mention Problem 12. Chhita–Johansson–Young (Ann. Appl. Probab. 25 (2015) 1232–1278) extend Helfgott's formula to
  different weights for horizontal and vertical dominoes; Chhita–Young (Adv. Math. 259 (2014) 173–251) compute the
  inverse for three weightings; neither computes entry or row sums or mentions Problem 12.
- **What was read.** Propp 1998 and 1999 in their arXiv LaTeX sources (the printed version of 1999 was not compared);
  Propp's progress report of 1998 completely; Helfgott in full (run B), at the writing Sections 1 and 2.1,
  Proposition 9, Corollary 10 and Theorem 11, and by run C also Section 2.4 (the definition of the Aztec diamond in
  coordinates, Lemma 1, the sign computation) and the source of Figure 17; Chhita–Johansson–Young, Chhita–Young and
  Lai's survey (Proc. Sympos. Pure Math. 110 (2024) 293–332; its Problem 12 is a different problem, and it does not
  include the still-open problems of the 1999 list) searched in full text. Kasteleyn 1961 and 1967, Percus 1969,
  Elkies–Kuperberg–Larsen–Propp 1992 and Kenyon 1997 are cited for background and were not read for the note.
- **Searches** (17 and 18 October 2026): arXiv (inverse Kasteleyn matrices; the Aztec diamond with Kasteleyn or
  Krawtchouk; Kasteleyn–Percus; Propp and Helfgott; the Kasteleyn matrix of the Aztec diamond, 100 most recent),
  zbMATH Open (including the five works citing Zbl 0937.05065 = Propp 1999), Crossref, OpenAlex (Propp 1999 =
  W1715153673, 102 citing works; the citing lists could not be retrieved), Semantic Scholar (the 145 works citing
  arXiv:math/9904150, filtered by keywords in titles and abstracts), seven web searches in all. No printed proof of
  the identity, and no statement of the row sums or of the solution of K_n u = 1, was found; the arXiv items of 2026
  on the inverse Kasteleyn matrix (2605.03896, 2603.27906) concern other dimer models.
- **Not available.** Propp's chapter "Enumeration of tilings" in the Handbook of Enumerative Combinatorics (CRC
  Press, 2015; doi:10.1201/b18255-15, listed by Crossref under the title "Tilings"): no open copy, not read.
  Helfgott's thesis in its original 1998 form (the arXiv version was read). The citation lists of Propp 1998 in
  Semantic Scholar and OpenAlex and of Propp 1999 in OpenAlex (could not be retrieved).
- **Caveat.** A search that finds nothing is not a proof of novelty; the result is new to us, not certainly
  unpublished.
- **Scope.** The note answers Problem 12 as posed (the 1999 convention), for every n ≥ 1, with the row and column
  sums as a by-product. No priority is claimed.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/