Let $A$ be a finite set and$$B=\{n\ge 1:a\mid n\text{ for some }a\in A\}.$$Is it true that, for every $m>n\ge \max (A)$,$$\frac{|B\cap [1,m]|}{m}<2\frac{|B\cap [1,n]|}{n}?$$

Erdos #488 (OPEN): for finite A (2<=a), B={n: a|n some a in A}, is |B cap[1,m]|/m < 2|B cap[1,n]|/n for all m>n>=max(A)? Cheap exact verifier (inclusion-exclusion); zero counterexamples across ~16000 families + fresh probes. Likely TRUE & tight (constant 2 unattained). The |A|=2 case may admit an elementary Lean-checkable proof -- the one cheap partial worth attempting.

CORRECTED STATEMENT (anti-confabulation): the REAL problem is a|n (divisibility). The page's Cambie/Alexeev/Aristotle counterexamples are for the TYPO VARIANT a-does-not-divide-n from [Er61]; do NOT cite them against the real problem. Extremal family: single-element A={a} at n=2a-1,m=2a gives worst ratio EXACTLY 2-1/a (a=2,3,5,8,13,30 -> 1.5,1.667,1.8,1.875,1.923,1.967), approaching 2 from below, never reaching -> tight-but-true. Multi-element families peak lower; |A|=2 worst ~1.816 (A={13,14},n=25), dominated by one element near its m=2a boundary. Cheap verifier YES; full positive close = analytic/sieve at a tight constant (HIGH wall, falsification empirically exhausted). The ONLY close-shaped sub-goal in the whole candidate sweep: an elementary proof of the |A|=2 (union of two APs) case -> one focused GPT-Pro attempt, HARD STOP, no escalation to the universal proof. Sources: [Er61],[Er66],[Gu04 E5]; formalized with sorry in formal-conjectures 488.lean.

#488 |A|=2 extremal structure PINNED: F(x)=floor(x/a)+floor(x/b)-floor(x/lcm); the ratio F(m)/m / (F(n)/n) over m>n>=b has TIGHT sup = 2, approached by consecutive A={a,a+1}, n=2a-1, m=a^2 with exact ratio (2a-1)^2/(2a^2) -> 2^- (never reaching 2 since a>1/4). Holds strictly; constant 2 is tight even at |A|=2.

Empirical (Opus, exact Fraction): worst |A|=2 ratio found 9801/5000=1.9602 at A={50,51},n=99,m=2500; the maximizing family is consecutive coprime a,a+1 with n=2a-1 (F=2) and m=a^2 (F=2a-1), ratio (2a-1)^2/(2a^2): 1.99990 at a=20000, ->2 from below. So a slack/soft proof CANNOT work (no room at the boundary); a correct |A|=2 proof must be exact at the consecutive-element boundary. Crude bound F(x)<=x*delta+1, F(x)>x*delta-2 closes only the regime b>5a; the hard regime b<=5a (comparable elements, incl. the extremal b=a+1) needs exact floor analysis. This is the one close-shaped sub-goal of the #488 sweep -- a real, bounded, Lean-targetable lemma, NOT the universal |A|>=3 case (analytic wall). NOTE: workflow's earlier '1.816' was small-a undersampling; the true sup is 2.

#488 |A|=2 EXACT REDUCTION (Opus): with F(x)=floor(x/a)+floor(x/b)-floor(x/L), delta=1/a+1/b-1/L, theta(x)={x/a}+{x/b}-{x/L} in (-1,2), the target 2m F(n) > n F(m) is EXACTLY mn*delta + n*theta(m) - 2m*theta(n) > 0. Separated one-sided bounds CANNOT work (ratio->2, zero slack); proof needs the joint m,n coupling.

Reduction: F(x)=x*delta - theta(x). 2m F(n) - n F(m) = mn*delta + n*theta(m) - 2m*theta(n). DISPROVED CLEAN LEMMAS (both verified to fail): (1) 'F(n) > n(1/a+1/b)/2 for n>=b' FAILS (1053 cases, all a|b / large-gcd where B = multiples of a only; the 1/a+1/b upper bound on F(m)/m is too loose). (2) '2F(n) >= n*delta+1 for n>=b' FAILS on the extremal family (there 2F(n)-n*delta = 6/(a+1)->0+). So NO separated bound works -- the inequality is tight (sup ratio exactly 2). OBSTRUCTION LOCATED: bad term -2m*theta(n) bites only when theta(n)->2 (n~2a-1); bad term -n*theta(m) bites only when theta(m)->-1 (m~a^2); the latter forces m>>n so n/m->0 and kills it -- coupling is essential. Extremal margin EXACT: 2mF(n)-nF(m)=4a-1>0 at A={a,a+1},n=2a-1,m=a^2 (vanishing vs ~4a^2). REMAINING: delicate case analysis (split n<L vs n>=L, and b/a ratio regime) -- handed to GPT-Pro. Hard stop: do NOT attempt |A|>=3 (analytic wall).

PROVEN (#488, |A|=2 case): for all integers 2<=a<b and all m>n>=b, F(m)/m < 2 F(n)/n, where F(x)=floor(x/a)+floor(x/b)-floor(x/lcm(a,b)) counts B={k: a|k or b|k} in [1,x]. The two-element case of the Erdos #488 doubling inequality holds. Elementary proof (GPT-Pro), independently verified by Opus.

Proof (GPT-Pro, Opus-verified). Prove the STRONGER F(m)/m < 2F(n)/(n+1) (=> F(m)/m<2F(n)/n). Two-case split on a|b vs a-not-divides-b (NO gcd split, NO finite check). CASE a-not-divides-b: b in B is not a multiple of a, so F(n)>=floor(n/a)+1; writing n=qa+r (0<=r<a), floor(n/a)+1=q+1>=q+(r+1)/a=(n+1)/a, giving F(n)>=(n+1)/a [VERIFIED a*F(n)>=n+1]. And F(m)<=floor(m/a)+floor(m/b)<=m/a+m/b<2m/a (since b>a). Hence F(m)/m<2/a<=2F(n)/(n+1). CASE a|b: then b>=2a and B=multiples of a, F(x)=floor(x/a); for n>=b, q=floor(n/a)>=2; 2mF(n)-nF(m) >= 2mq - n(m/a) = m(2q-n/a) > m(2q-(q+1))=m(q-1)>=m>0. Margin is exactly tight at the extremal family a,b=a+1,n=2a-1 where F(n)=2=(n+1)/a (no hidden slack). OPUS VERIFICATION: (1) both cases hand-checked, logically airtight; (2) computational: 0 violations of the main inequality, the step-1 lemma a*F(n)>=n+1, and the stronger F(m)/m<2F(n)/(n+1) over 2<=a<31, a<b<61, n in [b,4b], m up to ~a^2 (incl. the extremal m=a^2). SCOPE: this is the |A|=2 case only. Full #488 (arbitrary finite A, |A|>=3) remains OPEN (tight-constant sieve/analytic wall). Next: Codex Lean-formalize this elementary proof against formal-conjectures/488.lean.

#488 |A|=3 extremal pinned (Opus): same shape as |A|=2 -- consecutive A={a,a+1,a+2}, n=2a-1 (F=3), m=a^2 (F=3a-3), ratio=(a-1)(2a-1)/a^2=2-3/a+1/a^2 -> 2^-. The tight constant 2 holds at every fixed |A|=k via consecutive {a,...,a+k-1}, n=2a-1, m=a^2.

Empirical (exact Fraction, prefix-min): worst |A|=3 ratio 406/225~=1.8044 at A={15,16,17},n=29,m=225, and the consecutive family ratio (a-1)(2a-1)/a^2 ->2. So |A|=3 is the next rung with the SAME tight extremal as |A|=2; GPT's |A|=2 proof (stronger statement F(m)/m<2F(n)/(n+1) + divisibility case split) is the template, but F(m)/m<2/a no longer holds for |A|=3 (need F(m)/m<=1/a+1/b+1/c and a poset case split). Hard scope: |A|=3 next; general |A| is the tight-constant sieve wall.

PROVEN (#488, |A|=4 case): for any A={a<b<c<d} and all m>n>=d, F(m)/m<2F(n)/n. #488 now holds for |A|<=4. AND the natural general strategy is PROVABLY DEAD (GPT-Pro, Opus-verified): general |A|=k needs a fundamentally different bound.

Proof (GPT-Pro, Opus-verified 0 viol in 31,441 checks). Reduce nonprimitive 4-sets to |A|<=3; for primitive antichains prove 2F(n)>(n+1)S (S=sum 1/a_i) via a TWO-SHIFT injection: each x with nu(x)>=3 has smallest covering element alpha and x>3*alpha; x-alpha and x-2*alpha are not divisible by any OTHER covering element (primitivity); for nu=4 (no outside element) BOTH are alpha-only (2 singletons); for nu=3 (one outside element h) h can spoil at most one (else h|alpha), so >=1 singleton. Injection is injective + avoids the 4 base points => N1>=N3+2N4+4 (>=+5 when lcm(A)|n+1). With (n+1)S-M<=4 (eq iff lcm|n+1), get 2F(n)>(n+1)S; then F(m)/m<=S<2F(n)/(n+1)<2F(n)/n. GENERAL CASE IS A WALL (two proven obstructions, Opus-verified): (1) the S-lemma 2F(n)>(n+1)S is FALSE for large k -- A={primes<=277}, n=277: S=2.00235>2 so 2F=552<(n+1)S=556.65 (does NOT disprove #488, since F(m)/m<=1 saves it, but kills the F(m)/m<=S route). (2) the injection target N1-sum_{j>=3}(j-2)N_j>=k is FALSE -- same example gives N1-N3-2N4=23<k=59. (3) the two-shift injection itself breaks at k>=5: A={2,3,5,7,13}, x=30 has x-2=28 (|7) and x-4=26 (|13) BOTH spoiled by two outside elements. So a general proof must use the cap F(m)/m<=1 and the actual union density, NOT S=sum 1/a_i. STATUS: #488 proven for |A|<=4 (clean, verified, ours). General |A|=k OPEN and requiring a fundamentally different bound (the natural shifted-density approach is provably insufficient). Pushing |A|=5 would need a new injection handling 2 outside elements; general needs the union-density cap.

#488 CRITICAL RE-ASSESSMENT from page comments: small-|A| is considered DONE by the field (our |A|<=4 is likely NOT novel), and the general case is a Tao-confirmed ANALYTIC WALL. Stop the general swing; verify |A|<=4 novelty before any write-up.

erdosproblems.com/488 comments (read 2026): (1) TAO (06 Apr 2026): the problem stays nontrivial even with 4 'cheats' (m->inf asymptotic; max(A)=o(n); constant C instead of 2; A=all primes). Tao RESOLVED the cheating version (cheats 1,3,4) via EXACTLY the regime-split we proposed to GPT: A=primes, LHS=1-prod(1-1/p); when sum 1/p small RHS~sum 1/p by Bonferroni, when large RHS~1 by monotonicity. But 'I don't see a way to remove more cheats.' => our planned GENERAL SWING is aimed at precisely what Tao could not do without cheats. (2) TAO (30 Mar): the hard extremal is A=primes in [n^{1/3},n^{1/2}], ratio ~1.0311 (bounded from 1, far from 2); proving it concretely needs Granville-Soundararajan-style ALTERNATING SUMS OF INTEGRALS = analytic core. (3) MalekZ: deep pair-tail/Conjecture-4.8 framework (building on Chojecki's paper), PROVED the a=2 (min(A)=2) case, many special cases, reduced to 'F(s)>=5 on visible slab' endgame, verified 25,000+ systems, but '13 natural approaches killed with explicit counterexamples' -- stuck on the same analytic endgame. (4) CHOJECKI has a PAPER on #488 with Lean/Aristotle formalization of special cases. (5) Adenwalla gave a clean small-|A| IEP argument; StijnC confirmed 'for |A| small it indeed is [easy]' but it FAILS for clustered families (A={x+1..x+k}, n=2x: LHS=k, RHS~2k) -- the extremal case. (6) Aristotle/Harmonic auto-found the typo + counterexamples to the mis-stated non-multiples version. IMPLICATIONS (honest): (a) our |A|<=4 proof is CORRECT and verified but likely NOT NOVEL -- the field treats small-|A| as done (Adenwalla IEP + StijnC 'for small |A| it indeed is'); verify against Chojecki's paper before any claim/write-up. (b) the GENERAL case is a confirmed ANALYTIC WALL (Tao stuck-with-cheats; MalekZ 13 approaches killed; needs alternating-integral analysis) -- DO NOT send the general-swing GPT prompt expecting a solve. (c) #488 is well-mapped by Tao/Chojecki/MalekZ; realistic Vela contribution is ~nothing novel. STEP BACK. Same pattern as #699 (Bloom/Parthasarathy) and #700 (StijnC): the experts are ahead; reading comments is mandatory before claiming.

#488 HYBRID ROUTE DISPROVEN (GPT-Pro, Opus-verified counterexamples): there is NO positive S-threshold for 2F(n)>(n+1)S, large S does NOT force F(n)/n>1/2 (can be <1/3 with S->inf), even asymptotic density delta(A)>1/2 fails, and a single injection cannot dominate the overlap mass. The exact threshold is the LOCAL overlap inequality N1 - sum_{j>=3}(j-2)Nj > sum (r_i+1)/a_i, which fails badly for natural primitive antichains. General #488 needs ratio-peak control of the periodic correction (analytic).

GPT-Pro rigorously killed the hybrid (small-S use S-lemma / large-S use cap-and-1/2) I proposed. OPUS-VERIFIED exact counterexamples: (1) NO S-threshold: A0={pq: p<q in primes<=29} (|A0|=45, max=667), n0=1333: F=618, S0=0.9532<1, but 2F/(n0+1)=0.92654<S0 -> S-lemma fails WITH S<1; and A_K=K*A0 scales S0/K->0 with F unchanged, so no positive S threshold exists. (2) high-S sublemma FALSE: A_P={3p: p<=P}, n=3P: F(3P)=P-1, F/n<1/3, while S_P=(1/3)sum 1/p -> infinity. (3) even delta(A)>1/2 insufficient: A={pq: p<q in primes<=37} (|A|=66), n=1147: F=569<573.5 so F/n<1/2, but delta(A)=0.5002475>1/2. (4) single injection impossible: same A, N1=314, N3=226, N6=29 -> sum(j-2)Nj=342 > N1, so N1-342=-28<0 (not enough singletons). All four exact-verified by Opus sieve + Fraction. EXACT THRESHOLD (3): 2F(n)-(n+1)S = (N1 - sum_{j>=3}(j-2)Nj) - sum_i (r_i+1)/a_i; the |A|<=4 injection proved the local condition N1-sum>=k; for general k it fails badly. CONSEQUENCE: #488 general cannot be driven by S, by the cap 1, by delta, or by a singleton injection. A real proof must bound sup_m F(m)/m via the periodic/sieve structure -- a ratio-peak bound c_m/m - 2 c_n/n < delta on the periodic correction F(x)=delta*x+c_{x mod L} (Granville-Soundararajan territory, per Tao). This is a genuine ANALYTIC wall, now precisely mapped. Honest #488 deliverable = |A|<=4 (likely not novel) + this verified obstruction map.

Erdős #488 small-|A|: CORRECT but NOT a novel contribution — do-not-claim verdict, Opus-confirmed. The |A|=2 inequality F(m)/m < 2 F(n)/n (F(x)=floor(x/a)+floor(x/b)-floor(x/lcm(a,b)), all 2<=a<b, m>n>=b) is independently VERIFIED: 0 violations over 306,802,291 (a,b,m,n) tuples; sup ratio -> 2 but never reached. Codex overnight re-derived it (elementary case proof + claimed Lean kernel check); we already had |A|=2,3,4 banked. NOVELTY VERDICT (prior-art gate): the LIVE #488 forum shows Terence Tao actively working it (Apr 2026: 'a=2 case proved, Chojecki reduction fails for a>=3') with Janson/Bonferroni machinery and periodic-correction ratio-peak analysis; our prior re-assessment already flagged small-|A| as 'considered done by the field'. So |A|<=4 is a correct-but-known result, NOT a resolution toward the mission five. The real #488 frontier is the general / all-primes case (analytic, hard). MISSION IMPLICATION: demote/drop #488 from the resolution lane.

Independent verification: 306.8M checks, 0 violations, sup ratio<2 (strict). Live forum: erdosproblems.com/forum/thread/488 (Tao Apr 2026). Frontier = general/primes case with Janson bounds, not small cardinality.

Opus 306.8M-tuple check of |A|=2 inequality: 0 violations. Live-forum novelty check: Tao active on general/primes frontier; small-|A| not novel.

Erdős #488 (for finite A, B=multiples of A, is F(m)/m < 2F(n)/n for all m>n>=max(A)?) remains OPEN — OBSTRUCTION MAP, not a settlement. |A|<=4 proven; general case a Tao-confirmed analytic wall. TWO verified obstructions: (1) the consecutive-integer EXTREMAL-FAMILY REDUCTION IS FALSE — A={14,15,16,17,19} has sup-ratio R=1593/980 > the same-maximum consecutive 5-set {15,16,17,18,19} with R=551/340, so #488 does NOT reduce to consecutive A. (2) NO uniform positive margin: mu({a})=1/(a(2a-1))->0, and consecutive blocks {a,...,a+k-1} give mu=O_k(a^-2)->0 for every fixed k; so NO finite per-A computation (the density-shadow grind) can close #488 via a uniform slack — it is PROVABLY FINITE-COVERAGE-ONLY. The exact missing input is a SUFFIX-ENVELOPE/DELAY theorem: for all primitive A and hard n>=max(A), max_{m>n} c_{m mod P}/m < E_A(n)=2F(n)/n - delta_A, where c_r=F(r)-delta_A*r and P=lcm(A); separated oscillation bounds lose the a^-2 scale at the extremal pair (n,m)~(2a-1, a^2).

GPT-5 Pro analysis, Opus-verified. Refutes the extremal-family bypass and proves the computational route is finite-coverage-only. OPERATIONAL: the density-shadow exact-decision grind (per-fixed-A certificates) can certify individual/bounded A but CANNOT be turned into a global compactness/uniform-margin argument — so continued chunk-grinding does not advance #488 and should stop. Joint-coupling form: F_A(x)=delta_A*x + c_{x mod P}; #488 <=> U_A(n):=max_{m>n} c_{m mod P}/m < 2F(n)/n - delta_A for all hard n. The missing theorem is a two-point correlation between a low-density denominator n and future positive-correction residues — not an ordinary sieve estimate. Counterexample + margins reproduced exactly (independent inclusion-exclusion + brute-force sup).

depends on (the wall): MISSING THEOREM (suffix-envelope/delay): for all primitive A and hard n>=max(A), max_{m>n} (F_A(m)-delta_A*m)/m < 2F_A(n)/n - delta_A — a two-point correlation between a low-density n and future positive-correction residues; not an ordinary sieve-density estimate.; OPERATIONAL: no uniform margin exists, so the density-shadow per-A computational grind is finite-coverage-only and cannot close #488; stop grinding chunks.

R(A={14,15,16,17,19})=1593/980 > R(C={15,16,17,18,19})=551/340 (diff 41/8330); both true sup-ratios by independent inclusion-exclusion + brute-force over m,n. delta_A=439/1615. mu({a})=1/(a(2a-1))->0; consecutive-block gaps [(30, 0.019491525423728815), (100, 0.0017512562814070351), (300, 0.0002167130402522723)] all O(a^-2)->0.

Erdős #488 public-counterexample AUDIT (Opus-verified): the erdosproblems.com/488 forum comments (30 posts; Cambie, van Doorn, Alexeev, Koizumi) contain NO counterexample to the current MULTIPLES statement (B={n: a|n some a∈A}, is F(m)/m < 2F(n)/n for all m>n≥max A). Of the public claims: 2 are counterexamples to the OLD `a∤n` typo version (irrelevant), the rest are lemma/reduction obstructions, not #488 counterexamples; 204 named-structure sets (2∈A, split-core tripod, prime-window) and a bounded frontier hunt yield 0. Independently re-verified by exact inclusion-exclusion. #488 is NOT already-falsified; it remains genuinely OPEN.

Resolves Will's #1 #488 question: are the public comments a counterexample? No. Reconciles our zero-counterexample certificates with the live forum. Source: Codex audit draft erdos488-forum-counterexample-audit-draft.v1.json; Opus re-checked the 3 finite claims + named families from scratch (F_A(x)=Σ_{∅≠S⊆A}(-1)^{|S|+1}⌊x/lcm S⌋, exact Fraction). Complements the banked obstruction_map (no uniform margin): #488 is open and not refuted on the page.

Opus re-verify: 0 counterexamples across 3 finite public claims + 4 named families (exact inclusion-exclusion). Audit summary: {"finite_claims_verified": 3, "current_multiples_counterexamples": 0, "old_typo_counterexamples": 2, "non_counterexample_forum_items": 8, "named_structure_sets_checked": 204, "named_structure_bounded_counterexamples": 0}