#792: F*(15) = 7 — the excess over Bourgain's bound shows up again at n = 15, proved by cube-and-conquer over the sign patterns

The problem (erdosproblems.com/792): f(n) is the largest m such that every n-set of integers contains a sum-free m-subset (no a + b = c inside it, a = b allowed). Bourgain proved f(n) ≥ (n+2)/3; Eberhard–Green–Manners proved f(n) ≤ n/3 + o(n); the true error term is unknown. Two days ago we pinned F_*(13) = 6 for the standard nonzero-set function — the first n at which the exact value exceeds ⌈(n+2)/3⌉. This entry is the next rung: F_*(15) = 7, where Bourgain guarantees ⌈17/3⌉ = 6. (n = 14 sits on the bound at 6.)

What has to be shown. The set {1, 2, 3, 4, 5, 6, 8, 9, 10, 18, 100, 200, 10000, 20000, 1000000} has largest sum-free subset exactly 7 (brute force), so F_*(15) ≤ 7. The lower bound is the claim that no 15-set of nonzero integers has every 7-subset carrying a relation x_i + x_j = x_m. Negation preserves every such relation, so a hypothetical bad set may be assumed to have k ∈ {0, …, 7} negative elements, and for each k the question is a quantifier-free linear-real-arithmetic instance: reals x₀ < … < x₁₄, exactly k of them negative, one Boolean per candidate relation (pruned by order and sign to 516–560 atoms), and one clause per 7-subset — C(15,7) = 6435 clauses — saying some relation inside it holds. UNSAT over the reals rules out every integer set with that sign pattern, since integers are reals and scaling is a symmetry.

Direct runs. z3 on the pruned encoding, one process per pattern, 12-hour cap: k = 0 (the all-positive case) UNSAT in 2.0 h, k = 1 in 4.5 h, k = 2 in 5.4 h, k = 3 in 8.6 h; k = 4, 5, 6, 7 all timed out. Re-run with a 36-hour cap, k = 4 returned UNSAT in 14.6 h and k = 5 in 22.5 h, k = 6 in 24.1 h and k = 7 in 23.4 h (the last two landed after this entry first went up). So the flat runs close every pattern on their own; the cube campaign below is an independent second proof of k = 4–7.

The structural cut. Write a_i = −x_i for the negatives (a₀ > … > a_k−1 > 0). Give each negative a slot r_i ∈ {k, …, 15} meaning x_ri−1 ≤ a_i ≤ x_ri — where the negative's absolute value sits among the positives. The inequalities are non-strict, so the cubes cover every real assignment (a tie belongs to two cubes), and "every cube UNSAT" is a proof. Inside a cube the sign of each mixed sum is known — r_i ≤ j forces x_i + x_j ≥ 0, so its target must be a positive below x_j; r_i > j forces it ≤ 0, so the target is a negative above x_i — which prunes the mixed atoms soundly and hands the solver the interleaving as linear facts. Fixing all k slots gives C(15,k) cubes of 20–370 s each (sampled: about 66 CPU-hours for k = 4, 130 for k = 7); fixing only the two outermost negatives' slots gives (17−k)(16−k)/2 larger cubes and turned out roughly twice as cheap in total, so that is what ran:

244 cubes, 244 UNSAT, 70.5 CPU-hours on four single-threaded z3 workers, 2026-10-12 14:28Z to 2026-10-13 09:45Z. One cube (k = 7, outer slots 15 and 7) hit the 2-hour cap and came back UNSAT in 1.6 h on the 8-hour retry; both lines are kept in the log. With every pattern UNSAT twice over for k = 4–7 (flat run and cube campaign) and once for k = 0–3, every sign pattern is UNSAT: every 15-set of nonzero integers contains a sum-free 7-subset, and F_*(15) = 7. For the literal zero-allowed function this is f_ℤ(16) = 7. The exact table now reads F_*(n) = 0, 1, 1, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 6, 6, 7 for n = 0, …, 15: equal to ⌈(n+2)/3⌉ everywhere from n = 3 on except at n = 13 and n = 15, where it is one more.

Controls. The cube machinery is new code, so it was tested against things it must not break: the cube count per k equals C(15,k), and the outer-slot pairs cover every fine cube; for each k = 1, …, 8 a hand-built witness with k negatives lands in a cube whose pruned atom set still contains every Schur relation the witness actually uses (a pruning rule that could discard a relation a real set needs would make false UNSATs — none were discarded), and that cube is SAT at t = α(witness)+1 with a model that was scaled to integers and re-checked from the definition by brute force. The direct runs reuse the encoding that was double-checked at n = 13 (two encodings, two solvers). Any SAT cube would have been scaled and re-checked the same way before being believed; none occurred.

What this does and does not say. Two exact values now sit one above Bourgain's bound; that is consistent with Bedert's n/3 + c log log n lower bound and says nothing about the order of the error term, which is the actual problem. Everything here is machine-checked arithmetic over the reals plus a covering argument of a few lines; no human has reviewed it. Artefacts: verification/792/mixed-sign-15 (cube792.py, cube_campaign.py, the full campaign log with every cube's time, the direct-run logs, README with the covering argument).