A companion Lean repository contains 122 theorems formalizing parts of the greedy nested-ring packing results.
Abstract
We study packings of annuli of a common width, allowing each ring to nest inside the hole of a larger one. The objectives of maximizing contact area and cardinality diverge: area is superadditive in the radius, cardinality is not. Under superincreasing radii, every descending greedy maximizes every positive, strictly increasing, superadditive objective. More strongly, any choice among feasible containers yields the lexicographically maximal feasible set, for containers of arbitrary shape in every dimension. This placement irrelevance holds unconditionally for at most three rings and fails at four in disks and squares; twin instances exclude every universal rule based only on the observable state. Write $ρ=\max_i(\sum_{j>i}r_j)/r_i$. The additive model has threshold exactly $1$. For disks we prove the exact global threshold $τ=\varphi$, with no failure at $ρ\le\varphi$, for every finite inventory, even with independent hole radii. The key geometric theorem states that, under golden tail bounds, an entire disk list fits a circular container if and only if its three largest disks fit; this supplies the uniform exchange of parents that the threshold proof needs. The Tribonacci constant $T\approx1.83929$ remains the exact floor of a rigid subfamily. A dimension-reduction lemma transfers spherical sharpness results to all dimensions $d\ge2$, and a separate argument proves the golden threshold for at most five rings in those dimensions. For square pans, a Cartesian confinement criterion gives twins and a family proving $τ_{\square}\le Y\approx1.6845$; its optimality is open. For independent holes, the exact universal area guarantee under $ρ\leκ<1$ is $\min(1,κ^{-2}-1)$, with threshold $1/\sqrt2$. The repository has 122 Lean theorems. Euclidean geometry, forest assembly and continuity remain written proofs; numerical checks do not substitute for them.
Problem
Packing annuli (rings) of common width into a container, allowing recursive nesting, to maximize either contact area or cardinality. The question is which objectives a greedy algorithm optimizes and when the choice of placement is provably irrelevant.
Approach
Radii satisfying superincreasing/tail-ratio conditions play the role of divisibility. The authors prove that descending greedy placements produce the lexicographically maximal feasible set for arbitrary containers and dimensions under superincreasing radii. Threshold parameters (additive threshold 1, golden ratio, Tribonacci constant) are established via geometric exchange arguments. A Lean repository holds 122 theorems, while Euclidean geometry, forest assembly, and continuity arguments remain written proofs.
Figure 4: Top: the minimal divergence instance; area optimum (left) versus cardinality optimum (right). Bottom: phase diagram of the divergence band for uniform width.
Results
Placement irrelevance holds unconditionally for at most three rings and fails at four in disks and squares. The exact global threshold for disks is proven to be the golden ratio, with the Tribonacci constant as the floor of a rigid subfamily; square pans give a bound of about 1.6845.
Figure 1: The n=4 counterexample of Theorem 13 : best fit (left) nests the 5 and loses the 4.8 ; the witness (right), realized by worst fit, places all four rings.