# Verification report — AMR-123-0003 (Propp, Trimer covers in the triangular grid, Problem 7: type-103 tilings of benzels with nonnegative Conway–Lagarias invariant)

Verification date: 2026-10-19.

**Verdict.** The note gives a **partial answer**; Problem 7 remains open in general. Every statement it makes
is proved, by a readable argument (Sections 2 and 3) or by stored certificates checked by a program
(Theorem 1.3).
- **Settled here.** For every D ≥ 2 the (4D−3, 5D−3)-benzel has a type-103 tiling (Theorem 1.2); for D ≥ 3
  these benzels lie in the open region R7. Every open case with |a−b| ≤ 7, every open case with
  max(a,b) ≤ 60, and 22 of the 27 open cases with |a−b| = 8 have a type-103 tiling (Theorem 1.3, a finite
  computation with 219 stored tilings). Hence Problem 7 holds whenever |a−b| ≤ 7 or max(a,b) ≤ 60
  (Corollary 1.4).
- **Known, not claimed.** The reduction to R7 (Proposition 2.2) combines published theorems: Defant–Li–Propp–
  Young (Combinatorial Theory 3 (2023), Theorem 1.1), Defant–Foster–Li–Propp–Young (SIAM J. Discrete Math. 39
  (2025), Theorem 1.1), Kim–Propp (Electron. J. Combin. 30 (2023), Theorem 3), and remarks of Propp. Lemma 3.3
  is a special case of DLPY Theorem 1.1 (a direct proof is given). The row (n, 2n−3) and the window
  max(a,b) ≤ 14 are covered by unrefereed 2026 preprints (A. C. Li, Zenodo 10.5281/zenodo.22315333,
  Theorem 1.1; The Clankers, Zenodo 10.5281/zenodo.20367029); the note reports them neutrally and does not use
  them.
- **Open.** The benzels (d+3J, 2d+3J) of R7 (d ≥ 3, 1 ≤ J ≤ (d−2)(d+1)/2) with b ≥ 61 and d ≥ 8, except the
  family of Theorem 1.2 and the eight certified benzels with d = 8 and b ≥ 61 (the row (n,2n−3) is covered only
  by the unrefereed preprints); among them the five cases (77,85), (80,88), (83,91), (86,94), (89,97). The smallest open cases by max(a,b) are (a,61),
  a ∈ {32, 35, …, 50}.
- **Evidence only.** Section 5 (evidence on ring inductions near the line I = 0) is labelled as evidence; it
  concerns the moves (3k+1, 3k+2) tested for small parameters, which do not reach the cases near I = 0.
- **Companion.** Problem 4 (record AMR-123-0002) is answered YES in an unrefereed preprint of A. C. Li
  (Zenodo 10.5281/zenodo.22306022, Theorem 2.1). The collar induction found independently in the computations
  behind this note is the same idea and is not claimed.

The note is unrefereed.

## Statement checked
- **Primary source.** J. Propp, "Trimer covers in the triangular grid: twenty mostly open problems", in *Open
  Problems in Algebraic Combinatorics*, Proc. Sympos. Pure Math. 110, AMS, 2024, pp. 261–273,
  doi:10.1090/pspum/110/02008 (Crossref, checked 2026-10-19); read as arXiv:2206.06472v4 (LaTeX source, 17
  January 2024), Sections 1–6. The published version was not compared; problem numbers follow the arXiv
  version, as does the corpus record.
  - Cells: (i,j,k) ∈ Z³, i+j+k = 1, centre i + jω + kω². (a,b)-benzel (2 ≤ a ≤ 2b, 2 ≤ b ≤ 2a): the cells with
    −(a−1) ≤ j−i, k−j, i−k ≤ b−1. Right stone = translate of the (2,2)-benzel; left stone = the other
    triangle; three bones; phones excluded. T_ijk: right stones allowed iff i = 1, left iff j = 1, k bone
    orientations.
  - Conway–Lagarias invariant (citing Conway–Lagarias 1990): right-stone area minus left-stone area, the same
    for all stones-and-bones tilings of a simply connected region; Propp's three formulas by a+b mod 3; for
    a+b ≡ 1 it equals the area (so the tiling is all right stones), which fixes the sign convention.
  - T_ijk(a,b) = T_ijk(b,a); the (n,2n)-, (n,2n−1)- and (n,2n−2)-benzels coincide.
  - Problem 7 (Section 6 of the arXiv version): whether type-103 tilings exist whenever the invariant is
    positive or zero; the preceding text notes that a negative invariant excludes them and that the table
    entries with nonnegative invariant are positive.
- **Corpus record.** ulamai/UnsolvedMath, AMR-123-0003 (dataset snapshot d371ee9, status `open`): its
  statement is the source text of Problem 7 with the paragraph before it.
- **Status page.** jamespropp.org/benzels.html (fetched 2026-10-19; last modified August 6, 2025): Problem 7
  listed as open (status of June 2025).

## Readings
| Reading | Answer | Where |
|---|---|---|
| Problem 7 as a universal question over all admissible (a,b) with I(a,b) ≥ 0 | open in general; settled outside R7 by published theorems, and inside R7 for the family (4D−3,5D−3) and for |a−b| ≤ 7 or max(a,b) ≤ 60 | Proposition 2.2, Theorems 1.2, 1.3, Corollary 1.4 |
| "positive or zero" includes I = 0 | yes; these are the pentagonal benzels, bone-tileable by Kim–Propp | Proposition 2.2(a) |
| the coincident benzels (n,2n) = (n,2n−1) = (n,2n−2) | same cell set and same invariant; covered by DLPY Theorem 1.1 | Proposition 2.2(a), check_note [1] |
| sign convention of the invariant | right stones count positively (Propp's own remark for a+b ≡ 1); pinned again by T103(3,3) = 0, T013(3,3) = 3 | check_note [2] |
| mirror pairs (a,b), (b,a) | reduced by T103(a,b) = T103(b,a) (map (i,j,k) → (i,k,j)) | Proposition 2.2(c) |

## Results in the paper
- **Lemma 2.1.** Coordinates u = j−i, v = k−j, w = i−k: cells ↔ triples with sum 0 and v ≡ u+1 (mod 3);
  bone steps; right stones as centres (U,V,W) with U ≡ V ≡ W; the rotation ρ.
- **Proposition 2.2.** The open region of Problem 7 is exactly R7 = {(d+3J, 2d+3J): d ≥ 3, 1 ≤ J ≤
  (d−2)(d+1)/2} and mirror images; a type-103 tiling there has d(d−1)/2 − J right stones.
- **Theorem 1.2 (Section 3).** t = D−1, B = B(4t+1, 5t+2) = {−4t ≤ u,v,w ≤ 5t+1}; H = {u,v,w ≥ 1−t};
  V = {u ≤ −t, w ≥ −t} minus {u = −t, v ≤ −t}, S = ρ(V), F = ρ²(V). Lemma 3.1: partition. Lemma 3.2: each
  vertical line u − w = c (c ≡ 1 mod 3) meets V in consecutive cells, [c−t, −t] (−3t < c ≤ 0), [−4t, −t−1]
  (−6t < c < −3t) or [−4t, c+5t+1] (c < −6t), of lengths 1−c, 3t, c+9t+2, all divisible by 3. Lemma 3.3: H is
  the disjoint union of the t(t−1)/2 right stones with centres ≡ 2−t (mod 3) and ≥ 2−t. Remark 3.4: sizes;
  the Z3 certificates (which presuppose Lemma 3.2(a)); relation to Li's finite-defect theorem.
- **Theorem 1.3 (Section 4).** 219 stored type-103 tilings of benzels of R7 (Table 1).
- **Section 5 (evidence).** For residue-0 (a, a+d) and moves (x,y): 2ΔI = 3(y−x)(2d+y−x) − (x+y); for
  x − y ≤ 2d a nonnegative change needs y > x; the moves (3k+1, 3k+2) carry d−k right stones. SAT tests:
  rings exist only for J ≤ k+1 (k = 0, 1 with 2 ≤ d ≤ 5; k = 2 with d = 3, 4; J ≤ 7).

## Computations (programs and outputs in reproducibility/)
No proof in Sections 2 and 3 depends on a computation; Theorem 1.3 is a computation.
- **Program of the note** (`check_note.py`, standard library, 3.8 s; ALL CHECKS PASSED): formulas and
  classification for a ≤ b ≤ 120; 36 table values; Theorem 1.2 for 2 ≤ D ≤ 40 (largest (157,197), 29,952
  cells) with Lemmas 3.1–3.3 checked separately; all 223 certificate files and the coverage; the identities of
  Section 5. Negative controls: a removed tile, a changed letter, a missing file and a file under a wrong name
  are reported; t = D−2 makes part [3] fail.
- **Original computation** (`original/`): the exact-cover encoding against Propp's tables of T013 and T103 for
  a, b ≤ 10 (45 benzels, including T103(10,10) = 655721 and T013(9,9) = 73454); SAT searches producing
  `certificates/original` (136 files: 132 in R7, 4 with I = 0); the rule search that suggested the family; the
  family for D ≤ 16; the Z3 certificates (P1 partition, P2 H = B(t,2t), PV/PS/PF whole bones; all `unsat` for
  all integers D ≥ 2; negative control t = D−2: PV, PS, PF `sat`); `verify_tilings.py` (136 + 87 files, 0
  failures); ring tests.
- **Re-runs** (2026-10-19, from copies): check_note, verify_tilings (both folders), the Z3 scripts (SMT files
  byte-identical), vA_F1.py 30, vA_check.py on both certificate folders, t2_F1.py 40, t7_coverage.py; all as
  recorded (`RERUN_LOG.txt`).

## Independent verification runs
The results were first obtained with the programs in `original/`. Three independent verification runs, all
AI-assisted, followed; each wrote its own programs from Propp's definitions. Runs A and B examined the
computation before the note was written and did not see each other's report; run C examined the text of the note.
- **Run A.** Read the record and Propp's arXiv source (definitions, Problems 4–7, Problem 14); confirmed the
  statement and the readings. Re-derived the reduction to R7 from the statements of DLPY Theorems 1.1–1.3, DFLPY
  Theorem 1.1 and Kim–Propp, checked in the arXiv sources. Re-derived the proof of Theorem 1.2: the partition,
  the case analysis of the vertical runs (cases A/B/C, which became Lemma 3.2(a)), and a direct proof of the
  right-stone tiling of H by the centre residue (which became Lemma 3.3). Re-ran the Z3 files (all `unsat`;
  control `sat`). Own program `vA_F1.py`: the family for 2 ≤ D ≤ 30, exact cover. Own checker `vA_check.py`:
  Propp's tables for a, b ≤ 7 (22 + 21 entries, 0 mismatches), area and invariant on 37 benzels, all 136
  original certificates (0 failures), R7 counts 50 (d ≤ 7) and 107 (b ≤ 45). Literature: Li's three preprints
  and The Clankers' preprint read and quoted correctly; Semantic Scholar HTTP 429; zbMATH: nothing new.
  Verdict: CONFIRMED_WITH_FIXES, status PARTIAL.
- **Run B.** Own programs written before reading the original scripts: Propp's tables T103, T013, T102 (41
  entries each, a, b ≤ 10), area formula and coincidences, the mirror map, the invariant on 468 stones-and-bones
  tilings; R7 recomputed (slices 2, 5, 9, 14, 20, 27, 35; 107 with b ≤ 45). A solver-free proof of Theorem 1.2
  (Section 2 of its report). Own build of the family for 2 ≤ D ≤ 40 (failing for t = D−2). All 136 original
  certificates re-checked with labels ignored (0 failures; every corrupted input rejected: a removed, duplicated or
  shifted tile, two tiles mixed, a phone, a tiling of another benzel, a tiling with left stones). The original
  scripts re-run with identical outputs. SAT search on the 87 benzels of R7 with 46 ≤ b ≤ 60 not yet certified:
  all 87 found (CaDiCaL; Glucose; a ρ-symmetric encoding for (47,55), (46,56), (45,54), (51,60)); no UNSAT;
  `t7_coverage.py`: 223 benzels valid. Literature: arXiv, OpenAlex, Zenodo, zbMATH, OEIS, two web searches;
  Crossref for all DOIs. Verdict: CONFIRMED with minor fixes, status PARTIAL.
- **Run C (the third run of the note, made on its text; programs and outputs in
  `reproducibility/independent_run_2/`).** Read the
  sources again: Propp's arXiv source (definitions, Sections 4 and 6 with the tables and Problems 4 and 7), the
  status page, the theorem statements of DLPY (1.1), DFLPY (1.1) and Kim–Propp (3) in the arXiv sources, Li v6
  (Theorems 1.1 and 7.2), Li v1.0.2 (Theorem 2.1 and the outline of its proof), The Clankers (window theorem,
  shell results, summary), BCL (abstract and the opening of its section on Problems 8–11). Checked every proof
  of Sections 2 and 3 line by line (Lemma 2.1, Proposition 2.2, Lemmas 3.1–3.3 with the three cases of
  Lemma 3.2(a), the proof of Theorem 1.2, Remark 3.4). Own programs: the classification for a ≤ b ≤ 120 and R7
  (slices 2, 5, 9, 14, 20, 27, 35; 107 and 206), 18 + 18 table values by exact counting and the sign pattern of
  Propp's whole T103 table; the family for 2 ≤ D ≤ 30 with each sector cut along its own lines and checked by
  its own checker; all 223 certificates accepted (0 failures) and every corrupted input rejected (removed,
  duplicated or shifted tile, changed letter, wrong benzel, exchanged cells, a phone, a tiling with left
  stones); the coverage of Table 1 recomputed (all R7 with b−a ≤ 7 or b ≤ 60; b−a = 8: 22 of 27; 219 = 206 + 13;
  largest (74,82), 5958 cells); the identities of Section 5 and the 80 ring tests re-run with its own SAT
  encoding (same pattern J ≤ k+1). Re-ran the package from an extracted copy of `source.zip`: all recorded
  outputs reproduced. Literature (arXiv API, OpenAlex, zbMATH, Zenodo, Crossref for every DOI, one web
  search): nothing new. Verdict: CONFIRMED with fixes, status PARTIAL; no fatal error.
- **Corrections required by run C, all made:** the ring evidence stated at its actual scope (abstract,
  introduction, title of Section 5); the remark on translates restricted to a ≤ b ≤ 2a−2, where the bounds of
  B(a,b) are attained (for b = 2a−1, 2a they are not); Li's parameter written 2a−b = 3k in Remark 3.4(c); "Li
  proves" replaced by "gives a proof, which we have not checked"; the companion paragraph reduced to a plain
  non-claim; Conway–Lagarias marked as not read and the reading of BCL stated; the version records of the
  Zenodo preprints added; the description of run B's negative controls corrected; the searches updated.
- **Corrections required by runs A and B, all made:**
  the proof of the one-interval-per-line property added (Lemma 3.2(a)); the published citation PSPUM 110 (2024)
  261–273 used, with DFLPY pages and Conway–Lagarias JCTA 53 (1990) 183–208; the SSRN DOI 10.2139/ssrn.7410520
  sourced by Crossref (title and author match); the row (n,2n−3) described as covered only by unrefereed
  preprints; Lemma 3.3 proved directly; the condition x − y ≤ 2d added; Problem 4 described as answered in an
  unrefereed preprint; the 87 certificates of run B added after `check_note.py`, `verify_tilings.py` and run A's
  checker had accepted them; the docstring reference `p7_verify_tilings.py` corrected.

## Relation to the literature, novelty and scope
- **Searches (18–19 October 2026).** arXiv API (benzel(s), tribone(s), "stones and bones", "Conway–Lagarias
  invariant", trimer/trihex tilings; newest first): only Propp, Kim–Propp, DLPY, DFLPY and Byun–Ciucu–Lee
  among relevant hits, nothing after 2406.18419v3. OpenAlex (benzel tilings; works citing Propp, DLPY, DFLPY,
  Kim–Propp, BCL): the 2026 Zenodo/SSRN preprints of A. C. Li and The Clankers. Zenodo API (benzel). zbMATH
  (benzel, tribone): DLPY, DFLPY, BCL, Kim–Propp. OEIS (benzel): enumeration sequences, no existence theorem for
  type 103. Crossref for every DOI. Semantic Scholar refused automated requests (HTTP 429), so its citation lists
  were not used; three web searches (two in run B, one in run C) found nothing new. Run C (19 October 2026):
  arXiv API (benzel, benzels, tribone, "stones and bones", trihex, "Conway-Lagarias invariant", "trimer
  covers"), OpenAlex ("benzel" since 2025; works citing the PSPUM version of Propp), zbMATH API (benzel),
  Zenodo records of the three preprints: nothing beyond the items above.
  - No printed answer to Problem 7 was found in these sources. Propp's status page lists it as open.
  - The family (4D−3, 5D−3) (on the diagonal b = 2a − 3(D−1)) was not found in Propp, DLPY, DFLPY, Kim–Propp,
    BCL, Li's three preprints or The Clankers' preprint; their infinite families in R7 are the row (n,2n−3).
  - A search that finds nothing is not a proof of novelty; no priority claim is made.
- **What was read.** Propp: arXiv v4 Sections 1–6. DLPY, DFLPY, Kim–Propp: statements of the theorems used, in
  the arXiv sources. Li, "Finite-defect path models …" (v6) and "An explicit collar recursion …" (v1.0.2): full
  PDF texts. The Clankers: LaTeX source. Byun–Ciucu–Lee: the abstract and the opening of the section on
  Problems 8–11 (tilings without vertical bones; nothing on type 103), in the arXiv source. Conway–Lagarias was
  not read; its theorem is quoted from Propp, Section 1. The proofs of the cited theorems and preprints were not
  checked; Li's Lean code was not run.
- **Scope.** The note answers Problem 7 for the family of Theorem 1.2 and for the finite set of Theorem 1.3, on
  top of the published reduction; the general case is open.

## 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/