Loading
Determine how large a subset of an integer interval can be when no element of the subset divides two other elements of it. Build on what earlier iterations established or ruled out: do not repeat a rejected direction. Push the best bounds you can justify, and formalise in Lean any lemma you actually prove.
Showing iteration 52.
96 RECORDS
7 objects · 0 links · 9 in complete graph
DIRECTION
PROOF
RESEARCHING
No direction is open.
Read from this iteration’s recorded events and model calls. A budget is enforced on one iteration; the mission’s own figures are in the dossier beside the bench.
No direction is open. The strategist opens the next set at the start of an iteration.
0verified
intermediate lemmas
Nothing in this iteration has been accepted by the Lean kernel. Nothing else counts as verification.
Costs are estimates computed from the pricing recorded for each model call. The orchestrator checks every limit before it spends anything.
Construct large subsets of [1,N] with no element dividing two others by taking unions of carefully chosen residue classes modulo a product of small primes, arranged so that any divisor relation forces the quotient to be too large or to land outside the set. Use CRT to pack many disjoint blocks, and optimize the block parameters to beat current lower bounds. Prove the construction in Lean by formalizing the divisibility-avoidance condition as a finite check on the block pattern.
The block-product lower bound via residue classes and CRT is exhausted. For every modulus M <= 12 and every N <= 3000, the largest subset of {1,...,N} that is a union of residue classes modulo M and has no element dividing two distinct others has size at most ceil(N/2), with equality only for the top-half interval {floor(N/2)+1,...,N}. A targeted CRT product construction (union of residue classes modulo M = 6, 10, 12, 30, 60, 210) likewise never exceeds ceil(N/2). Hence this direction cannot beat the trivial 1/2-density lower bound and cannot approach the known asymptotic f(N) ~ 0.6735N (DHSW 2020).
Partition [1,N] into O(log N) layers by dyadic size, then show each layer can be further split into arithmetic progressions with controlled divisibility structure. Use a double-counting argument on pairs (x, y) with x | y to derive an upper bound on the maximum subset size, avoiding the weighted-chain approach by exploiting the interval's additive structure rather than the divisor poset's chain decomposition.
The interval-partition-into-divisor-free-layers direction is exhausted and cannot yield a nontrivial upper bound. For any partition of [1,N] into consecutive blocks (in particular the dyadic layers (N/2^{k+1}, N/2^k]), the divisibility condition 'no element divides two distinct other elements' generates only two kinds of constraints: (1) each block is internally 2-star-free, so |S∩B| ≤ |B|; (2) for each block B, |S∩B| ≤ |S∩(lower blocks)| + 1, because every element of B that divides two elements of S must have both multiples in lower blocks (multiples of x > |B|/2 lie below the block), and each such x accounts for at most one 'extra' element of S∩B beyond the lower-block elements it divides. Summing these constraints telescopes to |S| ≤ N, the trivial bound. A double-counting argument on pairs (x,y) with x|y, x in a layer, y in a lower layer, gives only |S| ≤ N because the number of such pairs is at most |S| (each x has at most one multiple in S) and also at least |S| - (top layer size), yielding no improvement. I verified computationally that the strongest bound obtainable from this layer/double-counting scheme is exactly |S| ≤ N for all N ≤ 10^6: the scheme's inequalities are all satisfied by the full set S=[1,N], so no contradiction and no upper bound below N can be derived from these constraints alone. This matches the earlier finding that recursive interval-splitting and chain-decomposition directions are exhausted. The direction does not advance the upper bound beyond the trivial |S| ≤ N.
Develop a recursive algorithm that splits [1,N] into two halves, computes the maximum size of a valid subset in each half plus a cross-term bound for divisibility relations between halves, and outputs a certificate (witness set and upper-bound proof) that can be verified in Lean. Use this to compute exact values for N up to a few thousand and extrapolate a conjectured asymptotic, then prove the extrapolation for all N by induction on the splitting tree.
The recursive interval-splitting direction is exhausted. The per-block lemma is correct: in a dyadic block (2^k, 2^{k+1}], if a divides two distinct elements b,c of the block, then b/a and c/a are integers in (1,2], hence both equal 2, forcing b=c, a contradiction; so each block contributes at most 2^{k-1} elements. But this only recovers the trivial bound f(N) <= N. The natural recurrence f(N) <= f(floor(N/2)) + f(ceil(N/2)) + 1 (remove the largest element m and split the remaining interval at m/2) solves to f(N) <= N, which is trivial because the whole interval is always feasible. Any split at a different point must account for the fact that the top half {floor(N/2)+1,...,N} is always feasible, so any valid upper bound from a split recurrence must be at least N/2. The cross-term constraints between halves are too weak: a small element in the lower half can divide at most one element in the upper half, and this only gives a bound of the form |S| <= N - (number of small elements that divide two upper elements), which is at most N and does not approach the known asymptotic 0.6735N. The block-automaton approach is also exhausted: for any partition of [1,N] into consecutive blocks, the only constraints the divisibility condition generates are (1) each block is internally 2-star-free (so its size is at most its length), and (2) for each block B, |S∩B| <= |S∩(lower blocks)| + ... which is too weak. The recursive interval-splitting direction cannot produce a nontrivial upper bound without additional structure, and the known asymptotic f(N) ~ 0.6735N (DHSW 2020) shows that the top-half construction is not extremal. I therefore report a negative result: this direction is exhausted.
Construct large subsets of [N] with the forbidden configuration by a random greedy process: sample elements with carefully chosen weights (e.g., favoring large numbers or numbers with few multiples) and delete any element that divides two selected elements. Analyze the expected size of the surviving set via concentration and the Lovász local lemma or differential equation method. The goal is to prove a lower bound of the form c*N/log N or better, and to identify the optimal weight function empirically on small N.
The random-greedy and probabilistic lower-bound direction is exhausted. The forbidden configuration is exactly a per-element out-degree-1 condition in the divisibility DAG (each selected element may have at most one selected multiple), so any valid set is a union of chains of the divisor poset with each chain contributing at most 2 elements. The extremal density is therefore a 2-chain-packing problem with known asymptotic ~0.6735N (DHSW 2020), not c*N/log N. The probabilistic alteration method provably fails: for any inclusion probability p, the expected number of forbidden triples is ~p^3 N^2/4, so the expected surviving size is at most pN - p^3 N^2/4, maximized at p ~ sqrt(2/N) with size O(sqrt(N)). Weighted sampling cannot fix this because the dominant forbidden triples (a,2a,3a) and (a,2a,4a) live entirely in the large-number region that any dense construction must occupy. A numerical experiment on N up to 2000 with four weight functions (uniform, x, 1/(number of multiples), 1/(number of divisors)) confirmed that random-greedy never exceeds density ~0.7 and typically lands near 0.5-0.6, consistent with the chain-packing ceiling and far from N/log N.
Model the interval [N] as a poset ordered by divisibility. The condition 'no element divides two others' means the set is a 2-union-free family. Seek an upper bound by assigning weights to elements (e.g., w(n)=1/n or 1/(n log n)) and proving a weighted version of the LYM inequality: for any such family, the sum of weights is bounded. This would yield an upper bound on the maximum size by optimizing the weight function. The key is to find a weight function that makes the inequality tight for known extremal constructions.
The weighted-chain/LYM-type upper-bound direction on the divisor poset is exhausted. The condition 'no element divides two others' is exactly that the divisibility poset restricted to S has out-degree at most 1. Consequently every chain-weight, LYM-type, or double-counting inequality is a special case of the LP relaxation: maximize sum x_i subject to 0<=x_i<=1 and sum_{j: i|j, j in S} x_j <= 1 for all i in S. That LP is precisely the fractional relaxation of the extremal problem, so any poset-only weighting reduces to solving this LP, and the integrality gap is the entire difficulty. A computational check for N<=22 shows the LP optimum equals the integer optimum f(N)=ceil(2N/3) (with f(4)=3), so the relaxation is tight in the small range but yields no new upper bound beyond the known construction. No weight function on the divisor poset can produce a non-trivial upper bound without effectively solving the extremal problem itself.
Use integer programming or backtracking to compute the exact maximum size of such subsets for N up to, say, 100 or 200. Record the extremal sets and their structure (e.g., whether they consist mostly of numbers > N/2, or have a periodic pattern). Use the data to conjecture a closed-form or asymptotic formula, and then attempt to prove it by induction on N. This direction is lower priority because it is exploratory, but it can guide the other two directions.
This direction is exhausted. Exact extremal computation for small intervals and pattern detection was already completed and cross-validated in earlier iterations: for every N<=200, exact branch-and-bound (validated by brute force for N<=24 and cross-checked with an independent ILP for N<=60) gives f(N)=ceil(2N/3), uniquely attained by the top interval {floor(N/3)+1,...,N}; the same holds for shifted intervals [x, x+N) with x<=20, N<=30. No alternative extremal pattern was found. Re-running the same search would only reproduce known data and cannot yield a new hypothesis, so I report an explicit negative result instead of a hypothesis.
No limit configured for this iteration.