The swarm proved the set exists. Here is the set.

Write f(n) = inf max A / 2ⁿ⁻¹ over dissociated sets of n positive integers (Bloom's normalisation); the ratio on this page is ρ = N/2ⁿ = f/2, and Bohman is ρ ≤ 0.22002. Bloom's exposition of the Astra proof (erdosproblems.com/1, 3 September 2026, pinned in the corpus) reads it as a statement about lattices: an explicit rational lattice Λ_s in the hyperplane Σx_i = 0 of ℝ^d, d = b^s, with no nonzero point in the open cube (−1,1)^d and a covolume constant Δ_s that tends to zero. A dissociated set follows once one has a primitive integer lattice close to Q·Λ_s; the proof obtains it from a density theorem and, in the Lean, from a Smith normal form with the scale sent to infinity.

The proof is currently non-quantitative, but just due to the non-effectiveness of the part where we approximate an arbitrary lattice by a primitive lattice.Thomas Bloom, exposition on erdosproblems.com/1, 2026-09-03

Every other step is explicit. So the object was one effective lemma away, and the number the proof never computed is one number per lattice.

Let B be the (d−1)×(d−1) matrix of the first r = d−1 coordinates of a basis of Λ_s, and A = D·B its integer scaling (D = q^s for the tilt α = p/q). Take an upper-triangular Hermite basis H of the column lattice of A with its rows reversed; the cube property is a property of the lattice, so it survives. For an integer scale t put

where sh has ones just below the diagonal and lift appends the row that makes every column sum to zero. Deleting the first row of C leaves an upper-triangular matrix with diagonal −1, so the column lattice of M is saturated in ℤ^r+1 and its primitive normal a is an explicit prefix recurrence — the Lean's transferWeights with the Smith form replaced by the Hermite form. The one quantity the ineffective proof never computed is the buffer

With t = ⌈(2^k + K)/D⌉ every integer relation c·a = 0 with |c_i| < 2^k is forced to zero (c = Mz by saturation, and ‖c‖ ≥ (Dt − K)‖lift(H/D)z‖ ≥ 2^k by the cube property), and the binary-block lemma gives A = {a_i2^j : 0 ≤ i ≤ r, 0 ≤ j < k}: n = dk elements, all subset sums distinct, N/2ⁿ = max a_i / 2^kr+1, which tends to Δ_s/2 as k grows. Nothing is estimated; every certificate is exact rational arithmetic.

build.py constructs; verify.py rebuilds Λ_s from (b, s, α) and checks, independently of the construction's intermediate objects:

• V0–V1 D = q^s; the basis lies in the zero-sum hyperplane; D·B is integral; |det A| (a FLINT determinant) matches the certificate.
• V2 H is upper triangular with positive diagonal and spans the same column lattice as A with its rows reversed — exact rational solves, integrality both ways.
• V3 the minor of C = S⁻¹M has determinant ±1 by a FLINT determinant, not by the triangular argument (a minor of M itself is not ±1, which the first run on the bench caught).
• V4 the FLINT nullspace of Mᵀ is one-dimensional and its primitive generator equals a — independent of the recurrence that produced a.
• V5–V6 the recorded K is at least the recomputed operator norm, with H⁻¹ from a solve; D·t − K ≥ 2^k.
• V7 positivity, distinctness, n = dk, N = 2^(k−1) max a, the ratio, and the comparison with 0.22002.

The inputs the verifier does not recompute at full size are the cube property of the base lattice — Bloom's Lemma 1 for α = 1/2, formalised in Lean for the identical gadget, and Lemma 1′ for every tilt, proved in the theorem note — and the strip property, decided per (α, b) by the structured search. At every build the battery checks Δ_s against an exact determinant on small lattices, the cube property exhaustively for d ≤ 9, the structured strip decision against a brute-force one for b ≤ 7, and every (α, b) in the ledger; the instrument's probes test thousands of lattice vectors at full dimension (18,612 at d = 729, none inside the cube). The battery also plants forgeries the verifier must refuse — a base weight off by one, a halved buffer, a Hermite entry off by one, a gadget that violates the cube condition, a verifier log that did not end green — 6 of 6 fired at this build, 13 checks green.

The verifier needs FLINT (python-flint), so it is not a standard-library verifier like the three on the landing page; it is detached all the same — one file, no code shared with the builder beyond the definition of the lattice, which it must share to rebuild it.

Bohman's bound holds for all large n; these sets are for specific n. The effective asymptotic statement f(n) ≤ n^{−c/log log n} with an explicit c, the form Bloom expects, would follow from a bound on the buffer K as a function of (b, s), because k must only exceed log₂(rK) by a constant. K is measured here (linear in d in every instance computed) and not proved; the Hermite basis is computed, not analytic, and an analytic triangular basis of Λ_s with an explicit inverse would settle it. The tilt family is a proven lever for the constant, and bigger tilted instances (α = 0.65, b = 21, s = 3 gives Δ = 0.235 at d = 9,261) need a Hermite path beyond PARI at that size. Nothing here concerns the lower bound N ≥ C(n, ⌊n/2⌋) or the true order of f.