Proposal U51: Lemma.erdos_65.parts.ii is a universal statement over finite graphs. It compares $\sum_{a\…

Hypothesis: 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. Threshold: 0 (must reach) Estimated cost: 60 min Why it's new: No notebook entry covers 65 (I checked N3, N4, N5, N12, N18, N20: only 1065 and 1068 have been tried). This is a finite search on a ∀-statement where a single small object would settle it. Related: N3, N4, N5, N12, N18, N20