P67 variable circles in a fixed-perimeter rectangle: n = 3–9 proved optimal

The values

For n = 6 the value is 27/28 + (19/14)p + (3/14)p² − (6/7)p³ − (29/28)p⁴ − (3/14)p⁵, where p is the only positive root of p⁶ + 6p⁵ + 9p⁴ + 4p³ − 9p² − 2p − 1 (its coefficients change sign once, so by Descartes’ rule there is exactly one positive root), p ≈ 0.815815509453887. For n = 9 the value is the radius sum of the unique solution, inside a stated small box, of a system of 28 contact equations; no closed form is known. The table shows 15 digits, and our checker’s rational enclosure is 1.8 × 10⁻³⁹ wide. No continuous optimum lies on the grid, and except for n = 4 each grid maximum is below ⌊10⁹Mₙ⌋.

0. Setting

The rectangle is [0, W] × [0, H] with W + H = 2 and its lower-left corner at the origin; the answer chooses W. Circle i has centre (xᵢ, yᵢ) and radius rᵢ. The constraints are the four walls xᵢ − rᵢ ≥ 0, W − xᵢ − rᵢ ≥ 0, yᵢ − rᵢ ≥ 0, H − yᵢ − rᵢ ≥ 0 of every circle, and (xᵢ − xⱼ)² + (yᵢ − yⱼ)² − (rᵢ + rⱼ)² ≥ 0 for every pair (tangency allowed). Write z = (x₀, …, xₙ₋₁, y₀, …, yₙ₋₁, r₀, …, rₙ₋₁, W) ∈ ℝ³ⁿ⁺¹ with H = 2 − W; the objective is S(z) = Σrᵢ.

The proof works on the closed relaxation K, which allows rᵢ ≥ 0 and keeps every other constraint. Every coordinate of a point of K lies in [0, 2], so K is compact and S attains a maximum on it, written Mₙ. Every site answer lies in K, and the optimal configurations found below have all radii positive, so Mₙ is also the maximum of the site problem, and it is attained.

A site answer has at most nine decimals per number, so Z = 10⁹z is an integer vector in [0, 2·10⁹]³ⁿ⁺¹ and the score is the integer ΣRᵢ, with Rᵢ = 10⁹rᵢ.

The maps x ↦ W − x, y ↦ H − y and the swap (x, y, W, H) ↦ (y, x, H, W) generate eight symmetries of the rectangle; together with relabelling the circles they preserve K, S and the nine-decimal grid. Below, “congruent” means equal up to one such symmetry and a relabelling.

1. Coordinate orders and the angular relaxation

Lemma 1.1 (orders and symmetry reduction). Label the circles so that x₀ ≤ x₁ ≤ … ≤ xₙ₋₁ (ties in any way), and let π list the labels by increasing y (ties broken compatibly). The three generating symmetries act on π as follows: the left–right reflection replaces each πₖ by n − 1 − πₖ, the up–down reflection reverses π, and the axis swap replaces π by its inverse π⁻¹ (the new x order is the old y order). So one representative per orbit suffices. The checker confirms that the orbits of the chosen representatives cover all n! permutations: for n = 3, 4, 5 all 6, 24, 120 orders are used directly; for n = 6, 7, 8, 9, the 115, 694, 5,282 and 46,066 representatives cover 720, 5,040, 40,320 and 362,880 permutations.

Lemma 1.2 (angular rows). For i < j put σ = 1 if j comes after i in π and σ = −1 otherwise; then Δ = (xⱼ − xᵢ, σ(yⱼ − yᵢ)) lies in the closed first quadrant. Let

u(t) = ((1 − t²)/(1 + t²), 2t/(1 + t²)), 0 ≤ t ≤ 1,

a rational parametrisation of the quarter unit circle. A nonzero Δ has a unique direction parameter t; if Δ = 0, the pair constraint forces rᵢ = rⱼ = 0 and any t may be taken. If t ∈ [a, b], write u = u(a) and v = u(b) (rational unit vectors; a × b means a₁b₂ − a₂b₁). Then

u × Δ ≥ 0, Δ × v ≥ 0, (u + v)·Δ ≥ (1 + u·v)(rᵢ + rⱼ).

Proof: the first two say that Δ lies in the cone of u and v, so Δ = αu + βv with α, β ≥ 0. Since |u| = |v| = 1, (u + v)·Δ = (1 + u·v)(α + β); the triangle inequality gives α + β ≥ |Δ| ≥ rᵢ + rⱼ; and u, v are at most π/2 apart, so 1 + u·v > 0. When Δ = 0 all three hold trivially.

A cell consists of an order π and an angular box ∏[aₖ, bₖ] ⊂ [0, 1]ᴾ (P = n(n − 1)/2 pairs), and gives the polyhedron {z ∈ [0, 2]³ⁿ⁺¹ : Az ≤ b}: 4n wall rows, n − 1 order rows xᵢ ≤ xᵢ₊₁ and 3 rows per pair, all with rational coefficients. Every packing with order π and directions in the box satisfies it. This is an outer model; no contact structure is assumed.

Lemma 1.3 (dual majorant). For any λ ≥ 0 and affine function f·z + f₀, on the polyhedron

f·z + f₀ ≤ λ·b + f₀ + 2 Σⱼ max(0, (f − λA)ⱼ).

Indeed f·z = λ·(Az) + (f − λA)·z, λ·(Az) ≤ λ·b, and each zⱼ lies in [0, 2]. Every certificate has this form: only the rational multipliers λ are stored, and the checker recomputes the bound from the problem definition.

Lemma 1.4 (covering). If finitely many closed boxes lie in the cube [0, 1]ᴾ, have total volume 1 and pairwise disjoint interiors, their union is the whole cube. Otherwise the complement is a nonempty relatively open subset of the cube, of positive volume, while the union has volume exactly 1. The checker verifies both conditions for every order’s group of boxes with exact integer volumes and a pairwise sweep, so every packing lies in at least one cell, boundary directions and coordinate ties included.

2. Branch and exclude: locating every high-scoring packing

For each n fix a rational threshold T slightly below the optimum, a half-width ε and a rational centre z⁰, and let B = {z : |zⱼ − z⁰ⱼ| ≤ ε for all j}. Every cell is of one of two kinds:

• excluded: Lemma 1.3 with f the radius indicator gives S < T on the cell;
• isolated: append the row −S ≤ −T (used only under the hypothesis S ≥ T) and state a symmetry g (whether to swap axes, two reflections, a relabelling). Each coordinate of g(z) is a rational affine function of z, and 2(3n + 1) multiplier vectors give ±g(z)ⱼ ≤ ±z⁰ⱼ + ε through Lemma 1.3, that is, g(z) ∈ B.

For n = 3–6 one cover suffices. For n = 7 and 8 there are two stages: cells of the first cover whose bound is at least T (the hard cells) are grouped by order, each group is enclosed in the coordinatewise hull of its angular boxes, and the checker confirms that every hard cell lies in its hull; each hull is then split into closed subboxes (coverage again by Lemma 1.4), each excluded or isolated. A hull is a superset, so clearing the hull clears the hard cells inside it; hulls need not be disjoint from each other or from cells already excluded. For n = 9 see §5.

For n = 7, 8, 9 the first number in the Excluded column counts cells excluded in the first cover, the second counts excluded subboxes of the refinement.

Lemma 2.1. Every point of K with S ≥ T is congruent to a point of B. Proof: by Lemmas 1.1 and 1.4 it lies (after a symmetry) in some first-cover cell; if that cell is hard, the point also lies in one of the subboxes of the cell’s hull. The cell or subbox holding the point cannot be excluded, so it is isolated, and its symmetry g moves the point into B.

3. The contact system inside the box

Inside B select M = 3n + 1 constraints, the selected contacts, forming the map G = (g₁, …, g_M): wall constraints are affine, pair constraints are (xᵢ − xⱼ)² + (yᵢ − yⱼ)² − (rᵢ + rⱼ)². Let J(z) = DG(z). Wall rows are constant; the nonzero pair-row entries ±2(xᵢ − xⱼ), ±2(yᵢ − yⱼ) and −2(rᵢ + rⱼ) each vary by at most 4ε on B. Put J₀ = J(z⁰), K₀ = (J₀ᵀ)⁻¹ (exact rational inverse), c the radius indicator, λ₀ = −K₀c, and let θ be the ∞-norm of |K₀| times the matrix of 4ε windows. Then for every matrix J whose entries lie in the 4ε windows around J₀, including J(z) for z ∈ B and the average of J along any segment in B,

‖K₀(Jᵀ − J₀ᵀ)‖∞ ≤ θ.

The checker verifies three things exactly: (i) θ < 1; (ii) λ_low = min λ₀ − θ/(1 − θ)·‖λ₀‖∞ > 0; (iii) every unselected wall and pair has a strictly positive lower bound on B (affine bounds for walls, interval squares with each difference widened by ±2ε for pairs), and the radii, W and H are positive on B. By the Neumann series Jᵀ = J₀ᵀ(I + K₀(Jᵀ − J₀ᵀ)) is invertible, and λ(J) = −(Jᵀ)⁻¹c satisfies ‖λ(J) − λ₀‖∞ ≤ θ/(1 − θ)·‖λ₀‖∞, so every component of λ(J) is at least λ_low > 0. For J = J(z) this reads ∇S = c = −J(z)ᵀλ(z).

Circle labels follow the certificate centre z⁰ (and the lists in §4); θ, λ_low and the lower bounds are approximations of the exact rationals the checker computes. n = 9 uses ε = 1/1000, the others ε = 1/10⁴.

Lemma 3.1 (every selected contact is tight at a maximiser). If z ∈ B is a local maximiser of S on K, then G(z) = 0. Proof: suppose gₗ(z) > 0. As J(z) is invertible, the inverse function theorem gives a smooth curve z(τ) with G(z(τ)) = G(z) − τeₗ for small τ ≥ 0. The other selected constraints are unchanged and gₗ stays positive; the unselected constraints, the radii, W and H are strictly positive on B and stay so for small τ by continuity. So the curve is feasible (it need not stay in B or keep the labelling order). Since J(z)z′(0) = −eₗ, dS/dτ = c·z′(0) = −λ(z)ᵀJ(z)z′(0) = λₗ(z) > 0, contradicting local maximality.

Lemma 3.2 (injectivity). G is injective on B. For z, w ∈ B, G(z) − G(w) = J̄(z − w) with J̄ = ∫₀¹ J(w + s(z − w)) ds. B is convex, so every entry of J̄ lies in its 4ε window and J̄ is invertible; G(z) = G(w) forces z = w. (Pointwise invertibility alone would not give injectivity; the estimate is applied to the averaged matrix.)

Lemma 3.3 (witness). The explicit configuration w* of §4 satisfies, in exact algebraic arithmetic: all 4n + P constraints are ≥ 0, exactly M of them vanish and these are the selected contacts in the table, all radii are positive, w* ∈ B, and S(w*) = αₙ > T. (For n = 9, w* comes from the Banach certificate of §5.)

Theorem 3.4. Mₙ = αₙ. Proof: w* is feasible, so Mₙ ≥ αₙ > T. Take a maximiser (K is compact); by Lemma 2.1 it is congruent to some z ∈ B, which is again a maximiser; Lemma 3.1 gives G(z) = 0; also G(w*) = 0, so Lemma 3.2 gives z = w*. Hence Mₙ = S(w*) = αₙ.

Corollary 3.5 (uniqueness). The same argument shows that every maximiser is congruent to w*: the optimal configuration is unique up to the symmetries of the rectangle and relabelling. No further certificate is needed; only the facts verified above are used.

4. The optimal configurations for n = 3–8

Write s = √2. Each circle is given as (x, y; r), listed in label order 0, 1, …. Every identity is checked in exact algebra: for n = 3, 4, 5, 7, 8 in the degree-four extension with basis 1, s, t, st and relations s² = 2, t² = A + Bs (evaluation at the positive real roots is a ring homomorphism, so algebraic identities hold for the real numbers; every inverse is checked by multiplying back; signs are decided by 80-digit rational intervals). For n = 6 the arithmetic is in ℚ[p]/(P), P(p) = p⁶ + 6p⁵ + 9p⁴ + 4p³ − 9p² − 2p − 1: the checker confirms that P changes sign across [0.815815509453887086444194883699, 0.815815509453887086444194883700] and that P′ is positive there, so the interval holds exactly one root.

n = 3

r = (14 − 4s)/41, R = 2r, H = 4r, W = (26 + 16s)/41 ≈ 1.186035. Circles: (R, R; R), (W − r, r; r), (W − r, H − r; r). S = 4r = 8(7 − 2√2)/41 = 8/(7 + 2√2). The large circle touches the left, bottom and top walls, each small circle touches the right wall and one horizontal wall, and the three are pairwise tangent.

n = 4

W = H = 1 (the optimal rectangle is a square). t = √(4 − 2s), R = 1 − s/2, r = 2 − s/2 − t. Circles: (1 − r, 1 − r; r), (R, 1 − R; R), (1 − R, R; R), (r, r; r). S = 2R + 2r = 6 − 2√2 − 2√(4 − 2√2).

n = 5

t = √(1 + 4s), u = (t − 1)/2 (so u(u + 1) = √2), R = 2/(u² + 2u + 5), r = Ru², a = R(2 − u²)²/(4u²), W = 4R ≈ 1.110454, H = 2 − W. Circles: (W − r, r; r), (W − R, H − R; R), (R, H − R; R), (2R, a; a), (r, r; r). S = 2R + 2r + a = (407 + 920√2 − 307√(1 + 4√2) − 34√(2 + 8√2))/712.

n = 6

p as above, m = (p + 1)(p² + 1)/(4p), h = (1 + p)², w = 1 + p² + 2m(p + 1), R = 2/(h + w), b = Rp², a = Rm², W = Rw ≈ 1.208214, H = Rh, x = R(p² + 2pm). Circles: (x, H − a; a), (R, R; R), (W − R, H − R; R), (b, H − b; b), (W − x, a; a), (W − b, b; b). S = 2(R + a + b), which reduces in ℚ[p]/(P) to the quintic expression given under the table of values.

n = 7

t = √(2 − s), R = 1/(3 + 2t), r = (2 − s)R, a = (2s − 2)R, W = 4R ≈ 0.882859, H = 2R(1 + 2t). Circles: (r, H/2; r), (W − r, H/2; r), (W − R, R; R), (W − R, H − R; R), (R, H − R; R), (R, R; R), (W/2, H/2; a). S = 4R + 2r + a = 6R = 6/(3 + 2√(2 − √2)).

n = 8

t and u as for n = 5, R = 1/(u² + 2u + 2), r = Ru², a = R(2 − u²)²/(4u²), W = 2R(u² + 2u) ≈ 1.048584, H = 4R. Circles: (a, H/2; a), (W/2, H − R; R), (r, H − r; r), (r, r; r), (W/2, R; R), (W − r, r; r), (W − a, H/2; a), (W − r, H − r; r). S = 2R + 4r + 2a = (3 + 13√2 + √(1 + 4√2) − 5√(2 + 8√2))/4.

For every n the checker also confirms that an 80-digit decimal evaluation of the closed form agrees with the exact enclosure to within 10⁻⁷⁰ (the enclosures are narrower than 10⁻⁷⁸), and that w* lies in B under the stated symmetry.

5. n = 9

Lemma 5.1 (subset rows). Removing any one of the nine circles leaves eight circles in K for n = 8, so Σⱼ≠ᵢ rⱼ ≤ M₈ = α₈ for each i. From the exact enclosure of α₈ the checker confirms α₈ < 1.430221728, so every cell gains nine subset rows Σⱼ≠ᵢ rⱼ ≤ 1.430221728, for 161 rows in all (36 walls, 8 order rows, 108 pair rows, 9 subset rows). The n = 9 proof therefore depends on Theorem 3.4 for n = 8.

Cover and isolation. 46,066 order representatives and 663,484 cells, each with a dual bound below 1.529 (as a by-product, nine radii always sum to less than 1.529). At T = 1.52831276, 15,978 cells have a bound of at least T; each is split directly (no hulls) for 34,310 subboxes in all: 34,253 with S < T, and 57 that isolate S ≥ T into B = z⁰ ± 1/1000, where z⁰ is a nine-decimal point. So Lemma 2.1 holds for n = 9.

Estimates on the box. The 28 selected contacts are in the table of §3 (circle 2 touches no wall). On B with ε = 1/1000, θ ≈ 0.0940 < 1, λ_low ≈ 0.0837 > 0, and the 44 unselected constraints are bounded below by about 0.2046 > 0, so Lemmas 3.1 and 3.2 hold for n = 9.

Lemma 5.2 (the Banach root). The certificate gives a rational point c with 50 decimals and the cube Q = {z : |z − c|∞ ≤ 10⁻⁴⁰}. Let P = J(z⁰)⁻¹ (exact rational inverse, checked by PJ(z⁰) = I) and N(z) = z − PG(z). On Q the entries of J differ from those of J(c) by at most 4·10⁻⁴⁰, so for z, z′ ∈ Q, N(z) − N(z′) = (I − PJ̄)(z − z′) with

κ = ‖ |I − PJ(c)| + |P| · (4·10⁻⁴⁰ windows) ‖∞ ≈ 7.85 × 10⁻⁹, η = ‖PG(c)‖∞ ≈ 4.74 × 10⁻⁵¹, η + κ·10⁻⁴⁰ < 10⁻⁴⁰.

Hence ‖N(z) − c‖∞ ≤ η + κ·10⁻⁴⁰ < 10⁻⁴⁰: N maps Q into itself and is a contraction, so by Banach’s fixed-point theorem it has exactly one fixed point q* in Q. P is invertible, so q* is the unique zero of G in Q. The 44 unselected constraints are bounded below by about 0.2085 > 0 on Q, and the radii, W and H are positive, so q* is a valid packing. The radius sum is linear, so S(q*) ∈ [Σc_r − 9·10⁻⁴⁰, Σc_r + 9·10⁻⁴⁰]:

1.528312768293629548847967448450491425410401 ≤ M₉ ≤ 1.528312768293629548847967448450491425412201.

The checker also confirms Q ⊂ B (|cⱼ − z⁰ⱼ| + 10⁻⁴⁰ ≤ 1/1000 for every coordinate) and that the lower end of the enclosure exceeds T. With w* = q*, Theorem 3.4 and Corollary 3.5 give M₉ = S(q*), with the optimal configuration unique up to symmetry and relabelling. Approximately, W ≈ 1.017300, H ≈ 0.982700, and the nine radii in label order are 0.176412, 0.115815, 0.174625, 0.192626, 0.140793, 0.140793, 0.218210, 0.176412, 0.192626; the site record answer is a nine-decimal approximation of it.

6. The grid: n = 3–8

Let τ be the record plus 1. After scaling by 10⁹, a cell’s rows become AZ ≤ 10⁹b with Z an integer vector; the symmetries preserve the grid. The claim is that no integer Z satisfies all constraints with ΣRᵢ ≥ τ.

n = 4. Every one of the 202 cell bounds is below 1.006788475 (the largest is about 1.00678847493), so 10⁹S < 1,006,788,475 and the integer score is at most 1,006,788,474. This also follows directly from α₄ ≈ 1.0067884746690.

Other n: branch trees. For n = 3, 5, 6 the roots are the first-cover cells, each with the integer box [0, 2·10⁹]³ⁿ⁺¹ (the checker confirms that each order’s roots cover its angular cube and that the orders cover every permutation). For n = 7, 8 a grid version of the first cover comes first: cells with bound below τ/10⁹ are excluded directly, the rest lie in per-order hulls, and these hulls, each with the full integer box, are exactly the tree roots. A node splits in one of two ways: an integer split replaces a coordinate range [L, U] by [L, k] and [k + 1, U]; an angle split replaces [a, b] by [a, c] and [c, b]. Both cover every integer point of the parent; the checker verifies the child boxes, that every node has exactly one parent, and that the forest is acyclic and fully reachable.

Leaf certificates: append the target row −ΣRᵢ ≤ −τ, write B̂ = 10⁹b (target row included), let the leaf’s integer box be L ≤ Z ≤ U, and take multipliers λ ≥ 0 with a = λA and e = c − a. Every leaf satisfies one of:

λ·B̂ + Σⱼ eⱼ·(Uⱼ if eⱼ ≥ 0, else Lⱼ) < τ or Σⱼ aⱼ·(Lⱼ if aⱼ ≥ 0, else Uⱼ) > λ·B̂.

The first gives ΣRᵢ = a·Z + e·Z ≤ λ·B̂ + e·Z < τ, contradicting ΣRᵢ ≥ τ (an upper-bound leaf). In the second the left side is the minimum of a·Z over the box, while a feasible point has a·Z ≤ λ·B̂ (an infeasible leaf). So no leaf contains a grid packing scoring τ or more.

For each n the record answer is checked in integers (W + H = 2·10⁹, positive radii, every wall and pair constraint), and its score is exactly the tabulated grid maximum.

7. The grid: n = 9

τ = 1,528,312,767. A grid packing scoring at least τ has S ≥ τ/10⁹ > T, so by §5 it is congruent to a point z of B, still on the grid.

Lemma 7.1 (localisation). For a feasible z ∈ B let J̄ be the average of J along the segment from q* to z (which lies in B). Then G(z) = G(z) − G(q*) = J̄(z − q*), and every component of λ̄ = −J̄⁻ᵀc is at least λ_low, so

M₉ − S(z) = c·(q* − z) = λ̄·G(z) ≥ λ_low ‖G(z)‖₁ (G(z) ≥ 0).

Also J̄ = (I + E)J₀ with ‖E‖₁ ≤ θ, so z − q* = J₀⁻¹(I + E)⁻¹G(z) and

|zᵢ − q*ᵢ| ≤ maxⱼ |(J₀⁻¹)ᵢⱼ| · ‖G(z)‖₁/(1 − θ) ≤ maxⱼ |(J₀⁻¹)ᵢⱼ| · (α⁺ − τ/10⁹) / ((1 − θ) λ_low),

where α⁺ is the upper end of the enclosure in §5 and α⁺ − τ/10⁹ ≈ 1.29 × 10⁻⁹. Adding |q* − c| ≤ 10⁻⁴⁰ and rounding inward to integers gives an offset range for each Zᵢ = Cᵢ + δᵢ (Cᵢ = 10⁹z⁰ᵢ): every coordinate has only 8 to 32 possible integers (the widest is −16 ≤ δ ≤ 15). The ranges re-derived by the checker coincide with the stored tree root.

Necessary linear rows on a box. The 12 selected walls are affine in δ. For a selected pair (i, j), with integer centre differences (d₁, d₂), radius sum ρ, offset differences (ξ, ζ) and offset radius sum ω,

(d₁ + ξ)² + (d₂ + ζ)² − (ρ + ω)² = d₁² + d₂² − ρ² + 2d₁ξ + 2d₂ζ − 2ρω + (ξ² + ζ² − ω²) ≥ 0,

and on the current integer box ξ² + ζ² − ω² ≤ Q_max = max ξ² + max ζ² − min ω², so −2d₁ξ − 2d₂ζ + 2ρω ≤ d₁² + d₂² − ρ² + Q_max is necessary. With the target row −Σδ_r ≤ ΣC_r − τ there are 29 rows Aδ ≤ b.

The integer tree. Starting from the localisation box, each integer split separates δᵢ ≤ k from δᵢ ≥ k + 1. There are 655 nodes, 327 splits and 328 leaves; every leaf gives λ ≥ 0 with λ·b + Σⱼ max(gⱼLⱼ, gⱼUⱼ) < 0 (g = −λA), so λ·(b − Aδ) is negative on the whole box, contradicting Aδ ≤ b. The smallest separation is about 1.09 × 10⁻⁴. Hence no grid packing scores 1,528,312,767 or more; the record 1,528,312,766 (checked in integers against all 36 walls and 36 pairs) is the grid maximum, two units below ⌊10⁹M₉⌋ = 1,528,312,768.

8. Our verification

zzzcy #308 emailed the proof package on 6 October 2026, stating that it was generated with AI assistance. Under the site’s rules we ran none of its scripts; we read only its JSON/JSONL data (cover cells and multipliers, hulls, trees, isolation and Banach certificates, the localisation box, grid answers) and decided every step with our own checker, tools/p67-certificates.py. It rebuilds every row (walls, order rows, cone rows, subset rows) from the problem definition, recomputes every dual bound in exact rational arithmetic with Python’s Fraction (stored bound values in the package are not read), checks every cover group as in Lemma 1.4 and the orbit cover of all permutations under the three generators, rebuilds each witness of §4 in exact algebra and takes the selected contacts to be exactly its vanishing constraints, recomputes θ, λ_low and the lower bounds of §3, the Banach constants of §5 and the localisation box of §7, and checks the structure of every tree and every leaf.

All 16 parts pass, in about 106 seconds in total with parallel workers. Every certificate count stated in the package (cells, hard cells, hulls, subboxes, nodes, leaves) agrees with our output; only the number of pairwise comparisons in a cover check depends on the sweep used, and for the n = 7 and 8 hull refinements it differs from the package’s figure, which does not affect the result. To rerun, unpack the package into a directory (containing _expanded/ and the n = 9 grid appendix P67_n9_grid_optimum_1528312766_appendix/) and run

python tools/p67-certificates.py --pkg <package-dir> [--jobs N] all

or list parts by name: n3c n3g n4c n4g n5c n5g n6c n6g n7c n7g n8c n8g n9local n9cover n9iso n9grid (n9iso and n9grid rely on n9cover also passing, and n9cover relies on the theorem checked by n8c). Any failure raises an error.

The program checks finitely many exact inequalities; the analytic steps that turn them into the theorem are Lemmas 1.2–1.4, 2.1, 3.1–3.3, 5.2 and 7.1, which we re-derived for this page and which agree with the package’s argument. The uniqueness in Corollary 3.5 follows from the same verified facts; the package states it explicitly only for n = 9. The package also contains a hand solution of the n = 3 contact equations and remarks on zero-radius circles; this proof does not need them and we did not review them separately.

Credit and scope

These configurations were known: Erich Friedman’s Circles in Rectangles table credits the n = 3–5 and 7–9 constructions to David W. Cantrell (2011), and the package attributes n = 6 to him as well; the table’s n = 6 entry currently prints an impossible 1.525+, so the site compares that row with the public repository of Berthold, Kamp, Mexi, Pokutta and Polik, which also supplied the site’s reference answers for these rows. This proof shows the configurations are optimal and settles the highest grid score. The adopted contribution earns zzzcy #308 one permanent +2 proof award.

Friedman · Berthold–Kamp–Mexi–Pokutta–Polik · Open P67