Dead end: U51 (agent)

Lemma.erdos_65.parts.ii is a universal statement over finite graphs. It compares $\sum _{a\in \text{cycle lengths}}1/a$ of any $n$-vertex graph with $kn$ edges against a complete bipartite graph $K_{A,B}$ with $|A|+|B|=n$ and the same edge count. One small explicit graph would therefore disprove it. Candidates are graphs with $|A||B|$ edges whose cycle lengths are few and large, since $K_{a,b}$ has lengths $\{4,6,...,2min(a,b)\}$. Small cases I checked by hand ($n\le 6$) hold, but nobody has run an exhaustive search for $n\le 10$. Method: (1) Python, no external libraries (numpy is unavailable). For $n\le 9$, or $n\le 10$ with pruning, and each $a\le b$ with $a+b=n$, enumerate graphs with exactly $ab$ edges up to isomorphism, or search with pruning by girth and cycle-length sets. Compute each cycle-length set by DFS and compare $\sum 1/a$ against $K_{a,b}$. (2) If a counterexample turns up, write the disproof over Fin n with an explicit adjacency, using decide/simp to pin down the cycle lengths. Check early with check_candidate that cycleLengths of a concrete small graph is computable, because enumerating walks is the bottleneck. (3) Otherwise post the verified range to chat as a dead end. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U51 dead end for Lemma.erdos_65.parts.ii. statement = faithful: I printed SimpleGraph.cycleLengths (the set of lengths of IsCycle closed walks) and finsums over finite sets. There is no junk-value case, and a=1 holds trivially. Search: simulated annealing in C (bitmask-DP cycle lengths) over graphs with exactly ab edges, for n≤10 and every 2≤a≤b with a+b=n. Nothing beat K_{a,b}, though the heuristic is not exhaustive. Structural reasoning: for a=2 a counterexample needs 2n-4 edges with sum<1/4, which forces girth≥5 and a set of one or two large lengths, impossible by cactus/theta density bounds. For balanced a, the edge count is close to n^2/4 and forces triangles and pancyclicity. blocker = out-of-reach. unblock = a real proof of Erdős's minimisation conjecture (open), or an exhaustive nauty-style enumeration of n≤11 to rule out small counterexamples rigorously.

{"proofs":{}}