# Verification report — OWR-13498-011 (Propp–Kenyon, disk packings of maximum area)

Verification date: 2026-09-30.

**Verdict.** The answer is yes: the greedy (Ford-circle) packing has maximum area. Every packing of the curvilinear
triangle between the unit disks centred at (±1, 1) and the x-axis, by disks touching the x-axis, has total area at
most π(ζ(3)/ζ(4) − 1) = 0.3475435…, and the greedy packing attains this value. More generally, for any two tangent
disks A, B resting on a line, the greedy packing of the gap between them maximises Σ r^α for every α > 1. It also
maximises the Bose weight Σ 1/(e^{1/√r} − 1) and every superposition of rescaled copies of that weight. The proof
is complete and by hand. Uniqueness of the maximiser is not claimed. The note is unrefereed.

## Statement checked
- **Primary source.** G. Rote (collector), "Open problems in discrete differential geometry", in *Discrete
  Differential Geometry* (organised by A. I. Bobenko, R. Kenyon, P. Schröder), Oberwolfach Report 13/2015,
  Oberwolfach Rep. 12 (2015), issue 1, pp. 661–729, doi:10.4171/OWR/2015/13. Problem 7 (Jim Propp, Richard Kenyon),
  "Disk packings of maximum area", is on p. 722.
  - The PDF used has SHA-256 e3ba6ef5fc327cfe1ca2c3c52a30d8107fbe487f832ae799f6ccd3e8e3da25ca. The same file was
    fetched anonymously from EMS by both verifiers.
  - The problem: two disks of radius 1 with centres (±1, 1) enclose, with the x-axis, a curved triangle. Place
    infinitely many non-overlapping disks touching the x-axis in it so that their total area is as large as
    possible. The question is whether the greedy method of placing each new circle into an interstice, touching
    two previously placed circles, gives the maximum.
  - Some text extractions of the PDF drop or garble the ± sign: one extraction gave "p 1 ; 1 q", and Apple PDFKit
    reads "p˘1,1q" (the glyph is present but mis-mapped; found by referee 2). The rendered page, which we rendered on
    2026-09-30, shows "(±1, 1)".
- **Corpus record.** ulamai/UnsolvedMath v1.6.0, OWR-13498-011 (status `open`). It states the same question: disks
  tangent to the x-axis in the curvilinear triangle bounded by the x-axis and two unit disks centred at (±1, 1),
  maximising the total area.

## Readings
| Reading | Answer | Witness / reference |
|---|---|---|
| Total area of a packing of the curved triangle of the unit disks at (±1, 1) by disks touching the x-axis (source, corpus) | yes: greedy is optimal | Thm 1.1 |
| "Infinitely many" disks: any finite or countable packing | covered | Thm 1.1 holds for all packings |
| "Greedy": in each interstice, the disk touching both bounding disks and the axis | unambiguous | Lemma 2.4(i): this disk is unique and is the largest that fits |
| Centres read without the ± (an artifact of some text extractions) | not a meaningful reading | the rendered page shows ±; the theorem covers every tangent gap anyway |
| Any two tangent disks resting on a line; weight Σ r^α, α > 1 | yes | Thm 1.2(b) |
| Weight Σ r^α, α ≤ 1 | trivial: the greedy sum is infinite | Lemma 2.4(iii) |
| Bose weight Σ 1/(e^{1/√r} − 1), and superpositions of its rescalings | yes | Thm 1.2(a), Cor. 3.1 |
| Every increasing weight | no | Remark 3.2: for the weight 1_{r ≥ 1/9}, four disks of radius 1/9 in a row beat the three greedy disks of radius ≥ 1/9 |
| Uniqueness of the maximiser | not addressed | — |

## Results in the paper
- **Lemma 2.2.** Packings of the problem's triangle T by disks resting on the axis are exactly the packings of the
  tangent gap between the two unit disks (base point in (−1, 1), disjoint from both).
- **Lemmas 2.3–2.4.**
  - For w(s) = 1/(e^{1/s} − 1) (s = √r the "size"), the Farey step is w(a)w(b) = w(c)(1 + w(a) + w(b)) for
    1/c = 1/a + 1/b.
  - The greedy packing consists of the disks with 1/s = m/a + n/b and base point x_A + 2ans, (m, n) coprime
    (Stern–Brocot). Since x_{v′} − x_v = 2(mn′ − m′n)s_v s_{v′}, these disks have pairwise disjoint interiors (tangent
    iff |mn′ − m′n| = 1), so the greedy packing is a packing of the gap (added after referee report 2). Its Bose value
    is w(a)w(b). Its s^p-value is G_p(a, b) = Σ_{gcd(m,n)=1} (m/a + n/b)^{−p}, which is finite iff p > 2, and
    G_p(1,1) = ζ(p − 1)/ζ(p) − 1.
- **Theorem 1.2(a)** (Bose weight). Every packing P of a tangent gap satisfies Σ_P w(s_D) ≤ w(a)w(b).
  - Proof: in a packing with n disks that has maximal weight among the packings with at most n disks, every disk is
    tangent to a neighbour on each side, so the packing contains a tangent chain from A to B. Induction on n then
    reduces the claim to the chain inequality (Prop. 4.2).
  - The chain inequality is proved by induction on the chain length. A degenerate chain splits into two shorter
    chains. A non-degenerate chain is moved along a two-disk move whose ends are degenerate. Along the move, the value
    is a constant plus f_{s₃}(θ)·f_{s₀}(log K − θ).
  - Key lemma (Lemma 5.1): f_ρ(λ) = 1 + w(e^λ − ρ) + w(ρ) is log-convex. Its second log-derivative is a positive
    multiple of Ω(q, x) = x(X−1)U₁ + (X−1)U₂ + xU₃ + U₄, whose double Taylor series has non-negative coefficients
    (closed forms derived in the text), so Ω ≥ q⁵/6.
- **Theorem 1.2(b) and Theorem 1.1.** Rescale the gap by t, apply (a), multiply by t^{p−1} and integrate. Tonelli
  and ∫ t^{p−1} w(s/t) dt = Γ(p)ζ(p)s^p give Σ_P s^p ≤ G_p(a, b). With p = 4 and a = b = 1, the area is at most
  π(ζ(3)/ζ(4) − 1).
- **Corollary 3.1.** For every positive Borel measure μ, the weight W(s) = ∫ w(s/t) dμ(t) is maximised by the greedy
  packing, with values in [0, ∞] and no further hypotheses.

## Computations (scripts and outputs in reproducibility/)
All proofs are by hand; no statement depends on a computation.
- **Lead** (`lead/verify_owr13498011.py`, standard library only, about 15 s; `ALL CHECKS PASSED`).
  - Exact checks:
    - the Farey step identity and the identity for h;
    - w′ and w″, by formal differentiation;
    - the polynomial identity between the three forms of Ω, and the Ψ–Ω identity at 1000 random rational points;
    - the greedy packing of the problem's gap down to size 1/40 (489 disks), which equals the coprime pairs, with
      exact disjointness;
    - Remark 3.2;
    - the coefficient closed forms for m ≤ 160, and no negative coefficient of Ω for m, n ≤ 160.
  - Numerical checks: the lattice identity for w (60 digits); Σ φ(q)/(e^q − 1) = 1/(e − 1)²; ζ(3)/ζ(4) − 1 with a
    tail bound; (log f_ρ)″ at 300 points (80 digits); convexity on 400 two-disk moves; 625 hill-climbed chains; the
    p = 4 superposition integral.
  - `lead/bose_chain_opt.py` (scipy SLSQP, k ≤ 6, six gaps with 0.02 ≤ a, b ≤ 40; 900 random recursive packings).
    The optimiser converges to Farey chains, where Φ = w(a)w(b). Excesses of at most 1.2·10⁻⁹ occur only at points
    that violate a constraint by a comparable amount (the slack is printed).
  - `lead/revision2_checks.py` (standard library, exact, about 10 s; `ALL CHECKS PASSED`), written after referee
    report 2 for the text added then.
    - Lemma 2.4(ii), in the unit gap and six random rational gaps (511 greedy disks each, built by recursive
      insertion): every greedy disk is D_v, with 1/s_v = m/a + n/b and x_v = x_A + 2ans_v; neighbouring vectors
      have determinant 1; x_{v′} − x_v = 2(mn′ − m′n)s_v s_{v′} for all pairs, A and B included; pairwise disjoint
      interiors, with tangency iff |mn′ − m′n| = 1.
    - Related work: the real Möbius map g(z) = ((x_B/b − x_A/a)z + x_A/a)/((1/b − 1/a)z + 1/a), of determinant 2,
      maps the Ford circle at p/q ∈ [0, 1] onto the greedy disk D_{(q−p, p)} (q ≤ 12, seven gaps).
    - The lead's `verify_owr13498011.py` was rerun after a docstring correction and gave the same output (apart
      from the timing).
- **Finder** (`claimant/`).
  - `key_lemma_exact.py` checks the closed forms and non-negativity of the coefficients exactly for m, n ≤ 80.
    `omega_series.py` expands Ω independently.
  - `verify_chain.py` and others give double-precision evidence for the weights s^p: the Ψ–Ω identity, the integral
    representation, convexity along two-disk moves for p ∈ {2.2, 2.5, 3, 4, 6}, and random chains.
  - Rerun from a scratch copy on 2026-09-30: all recorded outputs were reproduced exactly (apart from numpy warnings
    on stderr).
- **Independent verifiers** (`referee/verifier1/`, `referee/verifier2/`; own implementations. Verifier 2 wrote its
  code before reading the finder's scripts).
  - Exact Ψ–Ω identity (500 and 400 random points).
  - Exact double series of Ω, from the bracket form (degree ≤ 60) and from the U-form (m ≤ 120, n ≤ 60): no negative
    coefficient, and the closed forms match.
  - Finite differences of (log f_ρ)″ with 80, 90 and 200 digits.
  - G_p by Hurwitz zeta sums, by the integral, and by brute force; the recursion.
  - Convexity on 150 + 150 random arcs.
  - SLSQP, Nelder–Mead and random-walk maximisation of chains (k ≤ 7, p from 2.02 to 12, gaps down to (1, 0.01)),
    and 400 random recursive packings. No chain value exceeded the greedy value by more than numerical error (about
    10⁻¹¹ relative); where the optimiser converged, it converged to Farey chains.
  - Verifier 2's recorded outputs were reproduced byte for byte on 2026-09-30.
  - Two caveats about verifier 1's scripts, explained in the README:
    - its grid tests report "violations" of size 10⁻⁴⁹ (80 digits) and 10⁻¹¹⁹ (200 digits). These are rounding noise
      where the true value is of order e^{−1/s}, for example about 8·10⁻¹³³ at s = 0.0032;
    - two sampling scripts stop early when no random feasible chain is found.
- **Referee 2** (`referee/referee2/`; written from the text of the paper before any author or finder script was
  read).
  - `ref2_exact_algebra.py` (exact): Ψ derived from its definition equals q²EΩ/((E−1)⁴x(X−1)) as a rational-function
    identity; every displayed formula of Section 6; the identities for h and for L, K; no negative coefficient
    m! n! [q^m xⁿ]Ω for m, n ≤ 400 (160,801 coefficients), in exact agreement with the closed forms.
  - `ref2_greedy_values.py`: the greedy packing of the unit gap to size 1/60 (1101 disks) equals the Ford
    description, with exact disjointness; the values of Sections 2 and 3; Remark 3.2; Lemma 2.2 by sampling.
  - `ref2_keylemma_numeric.py` (150 digits): (log f_ρ)″ > 0 at 600 random points by pure finite differences; h″ > 0
    at 3000 points of 300 random two-disk moves.
  - `ref2_greedy_general_gap.py` (exact): the base points and the identity x − x′ = 2(nm′ − n′m)ss′ in six rational
    gaps (255 disks each), with exact disjointness.
  - `ref2_chain_opt.py`: 1225 SLSQP runs over k-chains (k = 2…8, seven gaps from (0.05, 0.08) to (100, 3)); every
    output repaired so that (C1) holds exactly and re-evaluated in 50 digits; largest feasible ratio
    Φ/(w(a)w(b)) = 0.99999999999999326, and 1148 runs ended within 10⁻⁶ of 1 (the value at Farey chains). The
    11 repaired outputs that violated some (C2) by a rounding-size amount all had ratio < 1. A large-scale limit
    Σ(t_i + 1/t_i) ≤ 3k + τ + 1/τ of the chain inequality (maximum of the difference −2·10⁻¹¹) and the chain
    inequality for the area weight (maximum ratio 0.999999999992) were also tested.
  - All recorded outputs end with `ALL PASSED`. They were reproduced from the release copy on 2026-09-30, apart
    from the printed running times.

## Independent adversarial audit
Two independent verifiers (round 3, 2026-09-29 and 2026-09-30) checked every step by hand, tried to refute the
claim, fetched the source anonymously and wrote their own code. They checked the finder's version of the argument,
which is organised around the weights s^p. Their verdicts:

| Item | Verifier 1 | Verifier 2 |
|---|---|---|
| Classification | PAPER_CANDIDATE | PAPER_CANDIDATE |
| Mathematics correct | yes (every step re-derived) | yes (every step re-derived) |
| Answers the question as intended | yes | yes (source PDF has the same SHA-256; ± reading confirmed) |
| Suggested corpus status | solved (yes), new unrefereed proof | solved (yes), new unrefereed 2026 proof, not a literature citation |
| Scripts | finder's `verify_chain.py`, `key_lemma_exact.py` reproduced; own code agrees | six finder scripts reproduced; own code agrees |
| Novelty | no prior solution found | no prior solution found |

Required fixes (the two lists overlap) and how they were applied:
1. **Citing works of the report (OpenAlex W1579881657, 4 citing works; both verifiers).**
   Done on 2026-09-30, after the OpenAlex daily budget reset, with an anonymous request
   (`lead/openalex_citing_W1579881657_2026-09-30.json`). The four works, with their abstracts read, are:
   - "The model of adjacency region of the 'crack' defect in a digital image", ScienceRise 2016,
     doi:10.15587/2313-8416.2016.65947 (image processing);
   - G. Rote, "Characterization of the response maps of alternating-current networks", Electron. J. Linear
     Algebra 2020, doi:10.13001/ela.2020.4981 (it concerns Problem 3 of the same session, Skopenkov's inverse
     problem for alternating-current networks);
   - Y. Wang, "Free-form surface representation and approximation using T-splines", dissertation,
     doi:10.32657/10356/19090 (OpenAlex dates it 2009, so the citation link is probably spurious);
   - "Developable approximation via Isomap on Gauss image", IEEE TVCG 2025, doi:10.1109/TVCG.2025.3566887 (also the
     only work listed by OpenCitations).

   None of them concerns Problem 7. The paper's Scope paragraph says so.
2. **Step 1 perturbation (both).** S is now the largest size among P* ∪ {A, B}, so it bounds a and b. The slack η is
   the minimum over all E ∈ P* ∪ {B} to the right of D, and in the mirror case over P* ∪ {A} to the left. The proof
   also checks that the moved disk stays inside the gap (paper, Section 4).
3. **Definition of C_k (verifier 2).** The definition now requires all s_i > 0. The pair (0, k+1) is excluded from
   (C2) and is covered by (C1). The bound s ≤ ab/(a+b) is derived for disks of a packing from the two genuine
   inequalities with A and B (Section 2). In the revised proof neither a bound on C_k nor compactness of C_k is
   needed, because the chain inequality is proved at every point of C_k (see 5).
4. **Lemma 4: domain, positivity, convergence (both).**
   - The two-disk move is stated with its θ-domain I = (log s₃, log(K/s₀)).
   - The moving function is now finite: h(θ) = f_{s₃}(θ) f_{s₀}(log K − θ) − (1 + w(s₀))(1 + w(s₃)), with both
     factors ≥ 1.
   - The integral over t is used once, in Section 3, applied to the final inequality between non-negative terms
     (Tonelli). So the question of splitting a divergent integral no longer arises.
   - For the record, the verifier's u-form u₀ + u₁ + u₂ + u₃ + u₀u₁ + u₁u₂ + u₂u₃ of the old integrand is exactly the
     Bose value h + w(s₀) + w(s₃) at scale t.
5. **Proposition 3, non-degenerate case (both).**
   - The degenerate bound is stated to hold at every degenerate point.
   - Tightness at the ends of J follows from the continuity of the finitely many constraints: if all constraints
     involving index 1 or 2 were strict at θ₊, a neighbourhood of θ₊ would be feasible.
   - The tight pair involves index 1 or 2, so it is not (0, k+1).
   - The maximiser on C_k was dropped, since the argument bounds Φ at every non-degenerate point.
6. **Lemma 6: closed forms in the text (both).** Section 6 states m![q^m] q^j e^{γq} = m!/(m−j)! γ^{m−j}, with
   examples. It derives the four coefficient formulas, the three combined formulas, and their signs.
7. **Remark 7: precise class of weights (both).** Replaced by Corollary 3.1, with its proof.
   - The class is W(s) = ∫ w(s/t) dμ(t) = ∫ dμ(t)/(e^{t/s} − 1) for any positive Borel measure μ on (0, ∞). This is
     verifier 2's class. By Bernstein's theorem it is also verifier 1's class Σ_m Λ(m/s) with Λ completely monotone;
     an atom of the representing measure at 0 would make every weight infinite.
   - No finiteness or continuity hypothesis is needed, because the corollary integrates the scaled inequality (1)
     between [0, ∞]-valued quantities.
   - The analogue of Lemma 5 is Lemma 2.4(iii) (greedy Bose value w(a)w(b)) together with Lemma 2.3(ii).
   - Remark 3.2 shows that some restriction on the weight is necessary.
8. **The ± sign (verifier 2).** Stated in the Scope paragraph of the paper and above. We rendered report p. 722,
   which shows (±1, 1). (The wording was revised after referee report 2; see fix 3 there.)
9. **HF report (both).** The suggested status is "solved (answer yes)", with this note labelled as a new, unrefereed
   2026 proof, not as literature.

Beyond the required fixes, the proof was reorganised so that the Bose weight comes first (Theorem 1.2(a)). The power
weights and Theorem 1.1 then follow by superposition (Section 3). The ingredients are the finder's: the reduction to
chains, the two-disk move, and the key lemma, which is unchanged. The new identities introduced by the
reorganisation are:
- the greedy Bose value w(a)w(b);
- the Farey step for w;
- the product form of h.

All three are checked exactly by `lead/verify_owr13498011.py`.

### Referee 2 (2026-09-30)
An independent adversarial referee then checked the released version line by line. That version had 11 pages and
PDF SHA-256 3df3d74a…d045; it is the version 1.0 deposited on Zenodo. The referee wrote its own code from the text
of the paper before reading any author or finder script, reran the author's and the finder's scripts, fetched the
Oberwolfach report anonymously and repeated the literature search. Its code and outputs are in
`reproducibility/referee/referee2/`. Verdicts:

| Item | Verdict |
|---|---|
| Statement fidelity | CONFIRMED |
| Proofs | CONFIRMED (every step checked; no mathematical error; one completeness line requested, fix 4) |
| Computations | CONFIRMED (independent code; the author's and the finder's scripts rerun and reproduced) |
| Novelty | CONFIRMED as far as can be checked (no prior statement or solution found; claims appropriately modest) |
| Presentation / house style | CONFIRMED WITH MINOR FIXES |
| Fatal | no |

All seven required fixes were applied:
1. **Abstract.** It now says "Along such a move the value is, up to an additive constant, a product of two
   log-convex functions", as the body does. The Zenodo description was changed in the same way.
2. **[RZ15] → [RZ17].** The published version is cited: Z. Rudnick and X. Zhang, Münster J. Math. 10 (2017)
   131–170, doi:10.17879/33249449333, with arXiv:1509.02989 as a note. The DOI is registered with DataCite, not
   Crossref. We checked it anonymously on 2026-09-30 against the DataCite record and the first page of the
   published PDF (both requests are in `queries.log`). The literature lists below and in `RESULT.md` were updated.
3. **The ± sentence.** The claim that the ± is "lost in the text layer" depended on the extraction tool. The Scope
   paragraph of the paper now says that some text extractions of the source PDF drop or garble the sign ± and that
   the rendered page shows (±1, 1). "Statement checked" and "Readings" above and `RESULT.md` say the same.
4. **G(A, B) is a packing.** Lemma 2.4(ii) now states that the disk with vector (m, n) has base point x_A + 2ans and
   that G(A, B) is a packing of the gap. The proof defines D_v by 1/s_v = m/a + n/b and x_v = x_A + 2ans_v and uses
   the identity x_{v′} − x_v = 2(mn′ − m′n)s_v s_{v′}.
   - The two vectors bounding each gap of the Stern–Brocot construction have determinant 1, so by Lemma 2.4(i) the
     inserted disk is D_{v+v′}.
   - Distinct coprime vectors have mn′ − m′n ≠ 0, so Lemma 2.1 gives disjoint interiors, with tangency iff
     |mn′ − m′n| = 1.
   - The same identity with (1, 0) and (0, 1) places the base points strictly between x_A and x_B.
5. **[Agu26].** The redundant note "September 2026" was removed; the entry now ends "arXiv:2609.15554, 2026".
6. **Query-log bookkeeping.** The sentence on `queries.log` below is now qualified.
7. **Release refresh.**
   - This subsection was added.
   - The paper's Verification paragraph has a new item 4 on the referee's checks and code.
   - `audit/referee2/` was copied to `reproducibility/referee/referee2/`, and the reproducibility README lists it.
   - paper.pdf, source.zip, the three Zenodo files and their sha256, size and md5 were regenerated.
   - The Zenodo description reproduces the amended abstract.

Optional suggestions taken up:
- Lemma 2.3(i) now uses σ = e^{1/a} and τ = e^{1/b}, so there is no clash with the exponent α or the function β of
  Lemma 2.2. Section 6 says that x = 1/ρ is not a base point there.
- Related work now says that the greedy packing of a tangent gap is the image of the Ford circles at the fractions
  in (0, 1) under a real Möbius transformation, instead of calling it "the Ford-circle packing". The map used in
  `lead/revision2_checks.py`, where this is checked exactly, is affine exactly when a = b.
- Idea of the proof: the sentence on maximisers is now stated for a packing with n disks that has maximal weight
  among the packings with at most n disks, which is what Section 4 proves.
- The docstring of `lead/verify_owr13498011.py` had an old title and running time; both were corrected. The program
  is otherwise unchanged.

Not taken up: the suggested one-sentence remark on the large-scale limit and on double-precision accuracy for very
large gaps. The double-precision checks reported in the paper use gaps with a, b ≤ 40, and the referee's runs on
larger gaps were re-evaluated in 50-digit arithmetic. The referee's large-scale test is recorded above.

Parts written after referee report 2, and checked by the author only (with `lead/revision2_checks.py`):
- the text of the packing argument in the proof of Lemma 2.4(ii); its two formulas were also checked exactly by
  the referee's `ref2_greedy_general_gap.py`;
- the Möbius sentence in the Related work paragraph;
- the rewording in "Idea of the proof".

## Relation to the literature, novelty and scope
- **Searches (September 2026).**
  - arXiv API: Ford circles with packing, area or greedy; horoball packing; osculatory and Apollonian packings;
    au:Propp.
  - Crossref, zbMATH, OpenAlex (mostly HTTP 429), OpenCitations, the StackExchange API, Semantic Scholar (HTTP 429
    on 2026-09-30), and one web search per agent.
  - Referee 2 (2026-09-30) repeated the search independently: arXiv API (Ford circles with optimal, maximal or
    maximum; disks tangent to a line with greedy; Propp and Kenyon; horodisk packings; total area with circle
    packing; Oberwolfach with disk packing), Crossref, OpenAlex, OpenCitations v2, zbMATH ("Ford circles", all 61
    records read by title) and one web search. It found no statement or solution of the problem.
  - All requests were anonymous. The finder's literature queries and the requests of the paper audit, of referee 2
    and of this revision are logged in `queries.log` in the problem folder. The triage requests that first fetched
    the source are in the log of the parent folder. The two verifiers' requests are not all in these logs. In
    particular, verifier 2's OpenCitations and StackExchange requests are, according to referee 2, documented only
    in verifier 2's own report. Referee 2 repeated the OpenCitations request on 2026-09-30 (logged); it returns the
    same single citing work.
- **Findings.** No statement or solution of the problem apart from the source. The closest works address different
  questions:
  - Boyd, on exponents of osculatory packings: Canad. J. Math. 23 (1971) 355–363; Canad. Math. Bull. 15 (1972)
    341–344.
  - Kocik, areas of Apollonian coronas via a zeta function (arXiv:1909.09941).
  - Rudnick–Zhang, gap distributions in circle packings: Münster J. Math. 10 (2017) 131–170,
    doi:10.17879/33249449333 (arXiv:1509.02989).
  - Aguilar Martín, greedy packing of nested rings (arXiv:2609.15554, September 2026).
  - Dumitrescu–Tóth, Beitr. Algebra Geom. 56 (2015) 515–532, §3.2. They use the same greedy packing of a gap
    between two tangent disks resting on a line, identified with the Ford disks, for a lower bound Ω(log n) on the
    total perimeter of n greedy disks touching the boundary of a square. This was found through the web search and
    checked in the arXiv version.
- **Citing works of the report.** OpenAlex lists four and OpenCitations one (included in the four). None concerns the
  problem; see fix 1 above.
- **Caveats.** Full-text searches of recent conference proceedings and of Propp's and Kenyon's own later writings
  were not done systematically. This negative search is not a proof of priority.
- **Scope.**
  - Proved: the answer to Propp–Kenyon as posed. Also every tangent gap, every α > 1, the Bose weight and its
    superpositions.
  - Not addressed: uniqueness of the maximiser; gaps between disjoint, non-tangent disks; packings whose disks need
    not touch the line.

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