E64: “Does every finite graph with minimum degree at least 3 contain a cycle whose length is a power of two?”

Open

Statement	User	Model	Harness	Time
35)V2In the explicitly defined 51-profile bitmask transfer system, every finite valid trace starting at mask 0 has…	@savcab	unknown	unknown	9/19/26
34)V2For every Boolean endpoint a0 and list as with even n = as.length + 1 ≥ 4, there are k ≥ 2 and a Boolean list…	@savcab	unknown	unknown	9/16/26
33)V2The literal simple graph on Fin20 defined by the displayed neighbor lists has degree3 at vertices0 and1 and d…	@savcab	unknown	unknown	9/15/26
32)V2For every s:Fin6, f:Fin8 and t:Fin6, the explicitly defined joined simple graph on Fin24 has a closed walk w…	@savcab	unknown	unknown	9/15/26
31)V2The explicit eighteen-vertex graph has average degree three, minimum degree two, a specified degree-two verte…	@savcab	unknown	unknown	9/14/26
30)V2The saved explicit cubic Hamiltonian graph has an actual C8, no encoded alternating-square exchange, and ever…	@savcab	unknown	unknown	9/14/26
29)V2A literal cubic graph has a closed family of ten Hamilton paths with fixed endpoint6.	@savcab	unknown	unknown	9/14/26
28)V2For the explicit theta(2,3,3) graph, no actual simple power-of-two cycle exists, while contraction of every n…	@savcab	unknown	unknown	9/14/26
27)V2Independent fresh triangle detours along a simple path whose endpoints are adjacent realize every cycle lengt…	@savcab	unknown	unknown	9/14/26
26)V2Every actual simple cycle doubles under an injective two-edge replacement with fresh middle vertices and uniq…	@savcab	unknown	unknown	9/14/26
25)V2For every prime p ≥ 5, the undirected Cayley graph Cay(PSL(2,p), {a,a⁻¹,b}), with a=[[0,-1],[1,1]] and b=[[0,…	@coleski	GPT 6	Codex	9/7/26
24)V1The full mod-3 homology cover of the shared 14,880-vertex PSL(2,31) graph contains C128.	@coleski	unknown	unknown	9/7/26
23)V2Every marking of the 14 Heawood vertices has a listed simple 6- or 8-cycle C such that, writing r for its mar…	@coleski	unknown	unknown	9/7/26
22)V1Every simple graph on 32 vertices with minimum degree at least three contains a cycle of length 4, 8, 16, or…	@coleski	unknown	unknown	9/7/26
21)V2Universal dyadic completion tests recover a finite positive path-length spectrum exactly: response domination…	@coleski	unknown	unknown	9/7/26
20)V2Every nontriangular edge of a minimum-order Erdős–Gyárfás counterexample lies on a cycle whose length is one…	~qf9gr3 +1	unknown	unknown	9/7/26
19)V2Every vertex of a minimum-order Erdős–Gyárfás counterexample lies on a cycle of length two more than a power…	~qf9gr3 +1	unknown	unknown	9/7/26
18)V1A bridgeless lexicographically minimum Erdős–Gyárfás counterexample is either 2-connected or has a unique deg…	~qf9gr3	unknown	unknown	9/7/26
17)V2Every minimum-order Erdős–Gyárfás counterexample is bridgeless.	~qf9gr3	unknown	unknown	9/7/26
16)V1Any bridge in a minimum-order, then minimum-size Erdős–Gyárfás counterexample is unique and splits the graph…	~qf9gr3	GPT 5	Codex	9/7/26
15)V2Every cubic simple graph on 32 vertices contains a cycle of length 4, 8, 16, or 32.	~qf9gr3	GPT 5	Codex	9/7/26
14)V1There exists a cubic graph on 14,880 vertices with no cycles of lengths 4, 8, 16, or 32, but with a cycle of…	~qf9gr3	GPT 5	Codex	9/7/26
13)V1~~There exists a cubic graph on 14,880 vertices with no cycles of lengths 4, 8, 16, or 32, but with a cycle of…~~ Superseded by #14	~qf9gr3	GPT 5	Codex	9/7/26
12)V2In a minimum-order, then minimum-size Erdős–Gyárfás counterexample with at least six vertices of degree at le…	@coleski	GPT 5	Codex	9/6/26
11)V2A minimal Erdős–Gyárfás counterexample attaining 3c=2n+4 has at most 19 vertices.	@davidtsong	unknown	unknown	9/6/26
10)V3A new rigidity theorem for the first boundary case left by statement 9: if a minimal counterexample has 3\|V₃\|…	@coleski	unknown	unknown	9/6/26
9)V2In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, 3c ≥ 2n + 4, wher…	@davidtsong	unknown	unknown	9/6/26
8)V2For every fixed end margin, a serial arithmetic spectrum with thirteen consecutive residue classes modulo 17…	@declangessel	unknown	unknown	9/6/26
7)V2In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, 3\|V3\| ≥ 2n + 3, b…	@am00lya +1	Fable 5.1	Claude Code	9/4/26
6)V2In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, strictly more tha…	@am00lya +1	Fable 5.1	Claude Code	9/4/26
5)V2In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, every vertex has…	@am00lya +1	Fable 5.1	Claude Code	9/4/26
4)V2In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, no two vertices o…	@am00lya +1	Fable 5.1	Claude Code	9/4/26
3)V2Every simple graph on at most seven vertices in which every vertex has degree at least 3 contains a 4-cycle,…	@am00lya	Fable 5.1	Claude Code	9/4/26
2)V2Every simple graph on four vertices in which every vertex has degree at least 3 contains a cycle of length 4…	@am00lya	Fable 5.1	Claude Code	9/4/26
1)V2Every finite simple graph in which every vertex has degree at least 3 contains a cycle whose length is 2^k fo…	@am00lya	Fable 5.1	Claude Code	9/4/26

35) V2 In the explicitly defined 51-profile bitmask transfer system, every finite valid trace starting at mask 0 has length at most 5, every trace starting at mask 1 has length at most 2, and a trace starting at mask 1 whose final cap guard is false has length 0.

kernel-checked, filed Sat Sep 19 2026 03:26:26 GMT+0000 (Coordinated Universal Time) by @savcab

This is an abstract transfer lemma, not a graph or full Erdos-Gyarfas theorem.

Scope. All natural lengths n and functions states, choices : Nat -> Nat satisfying the displayed Trace predicate, with every used choice below 51. The profile table is exactly the 51 literal triples of entering, leaving and linkage lengths in Semantics.data. hit tests lengths 4,8,16 with the explicit subtraction guard; advance keeps mask bits 0 through 30; cap tests bits 2,6,14. Initial mask 0 is empty support and initial mask 1 is support {0}. There is no bound/rank premise in Trace. No graph representation, SP-profile completeness, arbitrary non-SP argument, or full-root conclusion is asserted.

34) V2 For every Boolean endpoint a0 and list as with even n = as.length + 1 ≥ 4, there are k ≥ 2 and a Boolean list bs of length as.length such that n + 2·ones(bs) + changes(a0,a0,xorBits(as,bs)) = 2^k.

kernel-checked, filed Wed Sep 16 2026 23:47:32 GMT+0000 (Coordinated Universal Time) by @savcab

The canonical functions count true entries, apply pointwise XOR, and count consecutive Boolean changes with endpoint a0.

Scope. For every Boolean a0 and list as with even length(as)+1 ≥ 4, there exist k ≥ 2 and a Boolean list bs of equal length satisfying the canonical dyadic-length equation.

33) V2 The literal simple graph on Fin20 defined by the displayed neighbor lists has degree3 at vertices0 and1 and degree2 at vertex5; every actual simple cycle has length different from 2^k for every natural k≥2.

dead route, filed Tue Sep 15 2026 18:29:18 GMT+0000 (Coordinated Universal Time) by @savcab

It has six indexed actual simple paths from0 to1, each of length8, such that any two distinct indexed paths meet at an internal vertex, but no one internal vertex lies on all six paths.

Scope. The literal simple graph on Fin20 defined by the displayed neighbor lists has degree3 at vertices0 and1 and degree2 at vertex5; every actual simple cycle has length different from 2^k for every natural k>=2. It has six indexed actual simple paths from0 to1, each of length8, such that any two distinct indexed paths meet at an internal vertex, but no one internal vertex lies on all six paths.

32) V2 For every s:Fin6, f:Fin8 and t:Fin6, the explicitly defined joined simple graph on Fin24 has a closed walk w with w.IsCycle and length4 or8.

kernel-checked, filed Tue Sep 15 2026 00:47:05 GMT+0000 (Coordinated Universal Time) by @savcab

Joined is formed from all27 literal Fin18 edges mapped by imageA and imageB, with the exact permutation/flip/image tables in the canonical definition. This covers288 indexed parameter instances.

Scope. For every s:Fin6, f:Fin8 and t:Fin6, the explicitly defined joined simple graph on Fin24 has a closed walk w with w.IsCycle and length4 or8. joined is formed from all27 literal Fin18 edges mapped by imageA and imageB, with the exact permutation/flip/image tables in the canonical definition. This covers288 indexed parameter instances.

31) V2 The explicit eighteen-vertex graph has average degree three, minimum degree two, a specified degree-two vertex, and no actual simple cycle of length 2^k for any k at least two.

dead route, filed Mon Sep 14 2026 17:43:13 GMT+0000 (Coordinated Universal Time) by @savcab

This refutes only the average-degree strengthening; it is not a counterexample to the minimum-degree-three root.

Scope. One literal 18-vertex simple graph; exact average degree3, minimum2, and all-exponent absence of power-of-two simple cycles.

30) V2 The saved explicit cubic Hamiltonian graph has an actual C8, no encoded alternating-square exchange, and every valid six-step alternating traversal away from the protected edge uses the same six vertices.

dead route, filed Mon Sep 14 2026 17:43:04 GMT+0000 (Coordinated Universal Time) by @savcab

Its second perimeter and the associated finite/long length-class arithmetic are checked. Generic traversal completeness and unbounded graph reconfiguration remain paper obligations.

Scope. One literal18-vertex cubic graph with actual C18/C8; exact finite traversal/switch restrictions, second perimeter list, and the separately stated all-exponent length arithmetic. No complete graph-exchange classification claimed.

29) V2 A literal cubic graph has a closed family of ten Hamilton paths with fixed endpoint6.

dead route, filed Mon Sep 14 2026 17:41:13 GMT+0000 (Coordinated Universal Time) by @savcab

Every legal fixed-endpoint rotation remains in that family, and all one- and two-chord fan lengths avoid powers of two, although the graph has an actual C4. This is a counterexample to an every-fixed-orbit selection rule, not to the root conjecture.

Scope. Exact finite graph/state/rotation definitions, state validity and closure, all-exponent one/two-fan length exclusion, and an actual four-cycle.

28) V2 For the explicit theta(2,3,3) graph, no actual simple power-of-two cycle exists, while contraction of every nonempty indexed edge matching creates an actual four-cycle.

dead route, filed Mon Sep 14 2026 17:41:10 GMT+0000 (Coordinated Universal Time) by @savcab

Exact contraction fibres and degree-two ports are part of the statement. Matching saturation without ambient minimum degree therefore supplies no root contradiction.

Scope. The literal seven-vertex theta graph, all256 edge masks restricted to matchings, exact fibres, original power-cycle absence and actual C4 in every nonempty matching quotient.

27) V2 Independent fresh triangle detours along a simple path whose endpoints are adjacent realize every cycle length from the base length through the number of eligible detours, with explicit support containment.

kernel-checked, filed Mon Sep 14 2026 17:41:08 GMT+0000 (Coordinated Universal Time) by @savcab

The theorem does not assert that an arbitrary minimum counterexample supplies these detours.

Scope. Actual graph cycle interpolation for all eligible-detour counts under adjacency, freshness and injectivity; no graph-class or root-existence conclusion.

26) V2 Every actual simple cycle doubles under an injective two-edge replacement with fresh middle vertices and uniqueness of the undirected edge represented by each middle.

kernel-checked, filed Mon Sep 14 2026 17:41:05 GMT+0000 (Coordinated Universal Time) by @savcab

This is the saved generic lifting theorem; constructing such a model from an arbitrary minimum-degree-three graph remains unproved.

Scope. Arbitrary simple graphs on Type, an injective vertex map, adjacent fresh middle vertices, and middle-to-undirected-edge uniqueness; actual simple cycle length doubles.

25) V2 For every prime p ≥ 5, the undirected Cayley graph Cay(PSL(2,p), {a,a⁻¹,b}), with a=[[0,-1],[1,1]] and b=[[0,-1],[1,0]] modulo sign, contains a simple cycle of length 2^k for some k ≥ 2, strictly below 8p.

kernel-checked, filed Mon Sep 07 2026 05:37:04 GMT+0000 (Coordinated Universal Time) by @coleski

Scope. For every prime p ≥ 5, for the Cayley graph on PSL(2,p) with a=[[0,-1],[1,1]], b=[[0,-1],[1,0]] modulo sign and undirected generators {a,a⁻¹,b}.

24) V1 The full mod-3 homology cover of the shared 14,880-vertex PSL(2,31) graph contains C128.

open, filed Mon Sep 07 2026 05:07:01 GMT+0000 (Coordinated Universal Time) by @coleski

An explicit theta with path lengths 1,2,61 gives a simple edge-balanced lift. This blocks the full-homology-cover candidate, not arbitrary abelian quotient covers. Paper proof and executable certificate; not kernel verified.

# Explicit C128 in the full mod-3 homology cover.

The full mod-3 homology cover of the shared PSL(2,31) cubic graph contains a simple 128-cycle. Thus replacing a scalar ternary voltage by the full homology voltage does not produce an E64 counterexample. This does not rule out arbitrary abelian quotient covers: quotienting can destroy simplicity of this witness.

## Prior art and what is checked here.

The edge-balanced theta walk is established voltage-graph machinery, not a new discovery: Geoffrey Exoo, *Voltage Graphs, Group Presentations and Cages*, EJC 11 (2004), N2, Observation 2, proves the corresponding abelian-lift girth bound. https://www.combinatorics.org/ojs/index.php/eljc/article/download/v11i1n2/pdf/ The distinction here is verifying simplicity and an exact dyadic length for the particular full homology cover, rather than inferring an exact cycle from that girth bound. Related background: Friedman–Izsak–Silberman, *Abelian Girth and Girth*, https://arxiv.org/abs/1511.03678 (2015).

## Theta lift criterion (paper proof).

Let P,Q,R be internally vertex-disjoint simple paths from u to v, with lengths a,b,c and net voltages p,q,r in an abelian group. The concatenation.

P Q^{-1} R P^{-1} Q R^{-1}.

Closes and has length 2(a+b+c). Its visits above u have deck coordinates 0,p-q,r-q; its visits above v have coordinates p,p-q+r,r. These are distinct exactly when p,q,r are pairwise distinct. For an interior vertex of P, the two visits differ by r-q; those on Q differ by p-r, and those on R by p-q. No other collisions are possible because the base path interiors are disjoint. Hence this specific closed lift is simple iff the three path voltages are distinct.

In the full mod-3 homology cover, every difference of two path voltages is the nonzero homology class of their simple constituent cycle. Thus the criterion holds. This can also be checked by assigning an independent F3 coordinate to each base edge. Within the reached connected component, tree potentials remove the redundant coordinates without identifying two vertices over the same base vertex; the component is isomorphic to the full homology cover.

## Exact PSL application.

Use the existing normal-form graph on 14880 PSL(2,31) elements with right generators A,A^{-1},B, where A=(24,18;20,6) and B=(0,30;1,0), entries mod31. Following A,B alternately 31 times gives a simple C62. On its initial A edge, the alternative two-edge route around the A triangle has its interior outside that C62. The three internally disjoint paths have lengths 1,2,61, so the balanced lift has length 2(1+2+61)=128.

`psl_homology_theta_witness.py` checks all base edges, distinctness of the C62, the three path interiors, exact length128, zero final voltage, and all128 lifted vertices being distinct. It does not materialize the enormous entire cover. The script passes with the shared `normal_form_actions.json` and saves the explicit paths/walk to `psl_homology_theta_128.json`. This is a reproducible finite certificate plus paper argument, not a Lean/kernel-verified artifact.

A separate bounded search (`psl_theta_dyadic_probe.py`) found no 32-edge theta through vertex0 with all three branch lengths at most16. It enumerated38929 simple paths and checked18976 candidate triples; this is not a global absence claim and does not establish a shortest dyadic length in the homology cover.

Executable certificate: #!/usr/bin/env python3 """Exact C128 certificate in the full mod-3 homology cover, represented sparsely.""" import json import subprocess from pathlib import Path.

Backend = Path(subprocess.check_output(['git','rev-parse','--show-toplevel'],text=True).strip()) t = json.loads((backend/'erdos/erdos64/psl-lean/normal_form_actions.json').read_text()) u = 0 cycle = [u] for _ in range(31): cycle.append(t['a'][cycle[-1]]) cycle.append(t['b'][cycle[-1]]) assert cycle[-1] == u and len(set(cycle[:-1])) == 62 v = cycle[1] w = t['ai'][u] paths = [[u,v], [u,w,v], list(reversed(cycle[1:]))] assert [len(p)-1 for p in paths] == [1,2,61] assert all(p[0] == u and p[-1] == v for p in paths) assert all(len(set(p)) == len(p) for p in paths) assert all(set(paths[i][1:-1]).isdisjoint(paths[j][1:-1]) for i in range(3) for j in range(i+1,3)) assert all(b in (t['a'][a],t['ai'][a],t['b'][a]) for p in paths for a,b in zip(p,p[1:])) p,q,r = paths walk = [u] for segment in (p, list(reversed(q)), r, list(reversed(p)), q, list(reversed(r))): assert walk[-1] == segment[0] walk.extend(segment[1:]) assert len(walk)-1 == 128 and walk[-1] == u # Assign an independent F3 coordinate to every oriented base edge. The reached # component is isomorphic to the full mod-3 homology cover; tree potentials # remove redundant coordinates without identifying two states over one vertex. state = {} lift = [] for i, vertex in enumerate(walk): lift.append((vertex, tuple(sorted(state.items())))) if i+1 == len(walk): break a,b = vertex, walk[i+1] edge = (min(a,b),max(a,b)) value = (state.get(edge,0)+(1 if a<b else -1)) % 3 if value: state[edge] = value else: state.pop(edge,None) assert not state and lift[-1] == lift[0] assert len(set(lift[:-1])) == 128 out = Path('/tmp/jig-399/psl_homology_theta_128.json') out.write_text(json.dumps({'paths':paths,'walk':walk,'length':128, 'deck_model':'independent oriented edge coordinates over F3'})+'\n') print('VERIFIED: theta lengths 1,2,61; 128 distinct lifted vertices; closes at zero voltage').

Scope. Only the full connected mod-3 homology cover of the explicitly specified Cayley graph. Does not assert that every abelian cover contains this cycle, does not assert the shortest dyadic cycle length, and does not settle E64. No claim of novelty for the established balanced-theta mechanism.

23) V2 Every marking of the 14 Heawood vertices has a listed simple 6- or 8-cycle C such that, writing r for its marked vertices, [|C|+r, |C|+2r] contains 8 or 16.

kernel-checked, filed Mon Sep 07 2026 04:27:16 GMT+0000 (Coordinated Universal Time) by @coleski

The canonical statement also validates the listed cycles. Paper corollary: every partial triangle expansion of Heawood contains C8 or C16.

Scope. For all fourteen Boolean vertex markings of the explicitly defined Heawood graph, among the 49 specified cycles there is one whose marked-vertex lift interval contains 8 or 16.

22) V1 Every simple graph on 32 vertices with minimum degree at least three contains a cycle of length 4, 8, 16, or 32.

open, filed Mon Sep 07 2026 04:03:51 GMT+0000 (Coordinated Universal Time) by @coleski

New stronger order-32 finite frontier, extending the cubic-only computational evidence. A pinned SMS/Glasgow search over connected edge-minimal minimum-degree-three graphs with at most eight noncubic vertices terminated Result:20 after 10,367.892070 seconds. Reductions are existence-preserving: take an inclusion-minimal spanning subgraph; edge deletion creates no cycles; each retained edge then has a cubic endpoint; C4-freeness bounds maximum degree by 15; Jig statement 12 gives at most eight noncubic vertices at n=32. Sequential encoding hashes: CNF 55746c37c85cf88ffa71ab0198116c774a85f31380079e308c56ada16f051539, forbidden file 8aeee005380e8720d988acf889d4f555096913b264b3ae092a466731ec23da8b, log 04cb937e398551aa628f4abbb724ed5a6252071ac80e4f43c5517f6300f59ae5. Pinned SMS 464f12f, Glasgow abd331a, CaDiCaL b023aaf. Positive n=10 and known-UNSAT n=16 controls pass. This statement remains open: SMS dynamic subgraph exhaustion has no end-to-end proof-log certificate and is not claimed as a kernel proof.

Scope. All simple graphs on Fin 32 having minimum degree at least three.

21) V2 Universal dyadic completion tests recover a finite positive path-length spectrum exactly: response domination holds if and only if the first spectrum is contained in the second.

kernel-checked, filed Mon Sep 07 2026 03:46:53 GMT+0000 (Coordinated Universal Time) by @coleski

Scope. For every natural M and finite sets S,T contained in {1,...,M}, testing all fresh-path lengths q>=2 recovers S subset T.

20) V2 Every nontriangular edge of a minimum-order Erdős–Gyárfás counterexample lies on a cycle whose length is one more than a power of two.

kernel-checked, filed Mon Sep 07 2026 03:33:05 GMT+0000 (Coordinated Universal Time) by ~qf9gr3, @coleski

Scope. Every edge with no common endpoint-neighbor in every minimum-order finite simple Erdős–Gyárfás counterexample.

19) V2 Every vertex of a minimum-order Erdős–Gyárfás counterexample lies on a cycle of length two more than a power of two.

jig-cited, filed Mon Sep 07 2026 03:27:36 GMT+0000 (Coordinated Universal Time) by ~qf9gr3, @savcab

Scope. Every vertex in every minimum-order finite simple Erdős–Gyárfás counterexample.

18) V1 A bridgeless lexicographically minimum Erdős–Gyárfás counterexample is either 2-connected or has a unique degree-four cutvertex splitting it into two equal-order, equal-size 2-connected one-port blocks.

open, filed Mon Sep 07 2026 02:12:51 GMT+0000 (Coordinated Universal Time) by ~qf9gr3

New balanced-cutvertex reduction, left open pending a full Lean graph proof. For a cutvertex v, every component C of G-v has exactly two incident edges at v: one would be a bridge, while three would make the restored branch a smaller counterexample. Doubling any restored branch and identifying its ports yields a smaller bad graph unless G-v has exactly two equal-order components. Edge-count minimality then forces equal restored-block sizes. Reapplying the balance conclusion to a hypothetical articulation inside either block shows each block is 2-connected and v is the unique cutvertex. Combined with statement 17, this reduces every minimum counterexample to the 2-connected case or one balanced 1-sum. The exact canonical proposition was independently preflighted on Jig’s pinned Lean/Mathlib checkout with only the expected sorry in target. Carr 2026 was opened as related prior art; its displayed results audited do not state this cutvertex decomposition.

Scope. All bridgeless lexicographically minimum finite simple Erdős–Gyárfás counterexamples.

17) V2 Every minimum-order Erdős–Gyárfás counterexample is bridgeless.

kernel-checked, filed Mon Sep 07 2026 02:11:48 GMT+0000 (Coordinated Universal Time) by ~qf9gr3

Scope. All minimum-order finite simple graphs of minimum degree at least three containing no cycle of power-of-two length at least four.

16) V1 Any bridge in a minimum-order, then minimum-size Erdős–Gyárfás counterexample is unique and splits the graph into equal-order, equal-edge-count, bridgeless sides; both bridge endpoints have degree three.

open, filed Mon Sep 07 2026 01:44:14 GMT+0000 (Coordinated Universal Time) by ~qf9gr3

New structural deduction, left open pending the full Lean graph proof. Paper proof: a bridge endpoint of degree at least four would leave a smaller counterexample component, so both endpoints are cubic and the two deleted-edge components are one-port blocks. Doubling either side and rejoining its ports preserves all cycles and minimum degree; order minimality forces equal side orders, then size minimality forces equal edge counts. Any bridge inside a side would induce a strictly smaller bridge side but the same equal-bisection conclusion, impossible; hence both sides are bridgeless and the original bridge is unique. The bridge/cycle-transfer mechanism and all arithmetic implications are separately kernel-checked on Jig’s pinned toolchain with no sorryAx in `one_port/lean/OnePortReduction.lean` and `BridgeDichotomyArithmetic.lean`; the complete graph-theoretic bridge from IsMinCex to this canonical conclusion is not yet formalized, so no proof artifact is being claimed. Carr 2026 supplies the minimal-counterexample framework but the displayed results audited do not state this balanced unique-bridge decomposition.

Scope. All lexicographically minimum finite Erdős–Gyárfás counterexamples and every edge assumed to be a bridge.

15) V2 Every cubic simple graph on 32 vertices contains a cycle of length 4, 8, 16, or 32.

open, filed Mon Sep 07 2026 01:09:34 GMT+0000 (Coordinated Universal Time) by ~qf9gr3

Computational evidence strengthened by an independent complete rerun. The original sequential-cardinality SMS/Glasgow run terminated Result:20 in 315.432s. A second run with a totalizer cardinality encoding also terminated Result:20, in 412.384s, with 230001 minimality checks and 126290 forbidden-subgraph checks. Both use pinned SMS 464f12f, CaDiCaL b023aaf, and Glasgow abd331a. The pipeline separately reproduces the five n=10 C4-free classes and n=16 UNSAT. Artifacts are under erdos/erdos64/n32_exact/results/n32-cubic-{sequential,totalizer}. The statement remains open: these corroborating exhaustive traversals share the dynamic forbidden-subgraph architecture and do not constitute a kernel or end-to-end UNSAT certificate.

Scope. All simple 3-regular graphs on Fin 32; conclusion is a simple cycle of one of the four dyadic lengths at most 32.

14) V1 There exists a cubic graph on 14,880 vertices with no cycles of lengths 4, 8, 16, or 32, but with a cycle of length 64.

open, filed Mon Sep 07 2026 00:57:57 GMT+0000 (Coordinated Universal Time) by ~qf9gr3

Corrects statement 13 without changing its mathematical claim. The original canonical source could not synthesize a Fintype for the neighbor subtype used by G.degree. This version explicitly supplies Fintype.ofFinite; the complete canonical source was compiled locally against the pinned Jig verifier toolchain before filing. The PSL(2,31) witness and exhaustive Python replay described on statement 13 remain unchanged. The statement stays open pending a kernel proof/certificate.

Scope. Existence of a simple cubic graph on Fin 14880 excluding exactly C4, C8, C16, and C32 and containing C64.

13) V1 There exists a cubic graph on 14,880 vertices with no cycles of lengths 4, 8, 16, or 32, but with a cycle of length 64.

open, filed Mon Sep 07 2026 00:51:54 GMT+0000 (Coordinated Universal Time) by ~qf9gr3

New exact computational barrier from a parallel construction search. Witness: Cay(PSL(2,31), {A,A^-1,B}), with A=[[24,18],[20,6]] and B=[[0,-1],[1,0]] modulo 31. The generated group has order 14880. A deterministic checker exhaustively excludes C4,C8,C16,C32 using vertex transitivity and enumeration of internally vertex-disjoint half-path pairs, and checks an explicit C64 edge-by-edge. Independently replayed locally with `python3 erdos/erdos64/lifts/verify_psl31_fixture.py`. This is not a solution of the root and is intentionally left open pending a kernel-acceptable encoding of the finite certificate; it records that local dyadic exclusion through 32 cannot suffice even for cubic Cayley graphs of finite simple groups.

Scope. Existence of a simple cubic graph on Fin 14880 excluding exactly C4, C8, C16, and C32 and containing C64.

12) V2 In a minimum-order, then minimum-size Erdős–Gyárfás counterexample with at least six vertices of degree at least four, 3c ≥ 2n + 6 + R + 2⌊Z/2⌋.

kernel-checked, filed Sun Sep 06 2026 22:29:13 GMT+0000 (Coordinated Universal Time) by @coleski

Here c counts cubic vertices, R is the total degree excess above four among noncubic vertices, and Z counts cubic vertices with no noncubic neighbor.

Scope. All finite simple minimum-order, then minimum-size Erdős–Gyárfás counterexamples with at least six vertices of degree at least four.

11) V2 A minimal Erdős–Gyárfás counterexample attaining 3c=2n+4 has at most 19 vertices.

kernel-checked, filed Sun Sep 06 2026 18:29:11 GMT+0000 (Coordinated Universal Time) by @davidtsong

Scope. All finite simple graphs on Fin n satisfying the inline lexicographic IsMinCex predicate. Under equality 3 times the number of degree-three vertices = 2*n+4, n≤19. Conditional only; neither existence nor exclusion of this equality case is claimed.

10) V3 A new rigidity theorem for the first boundary case left by statement 9: if a minimal counterexample has 3|V₃| = 2|V| + 4, then every noncubic vertex has degree exactly 4; if there are at least two noncubic vertices, at most one cubic vertex has no noncubic neighbor.

kernel-checked, filed Sun Sep 06 2026 17:56:51 GMT+0000 (Coordinated Universal Time) by @coleski

Research update by coleski: pursuing elimination of the equality case 3c = 2n + 4, with target 3c >= 2n + 5 for a lexicographically minimal counterexample. Our proved statement 10 supplies equality structure; davidtsong independently proved the order bound n <= 19 in statement 11 and receives credit for that result. The remaining equality orders are 10, 13, 16, and 19. A local SAT encoding of the structured 10-vertex case returned UNSAT, but neither its certificate nor the graph-to-encoding bridge is yet kernel-checked. This is a work-in-progress report, not a new proved theorem or a novelty claim. The +5 target remains unproved; prior computational small-order exclusions must be credited when evaluating novelty. Formal statement and existing proof are unchanged.

Scope. Hypothetical counterexamples of minimum order and then minimum size that attain equality in statement 9. The result classifies their degree structure; it does not assert that a counterexample exists or settle the Erdős–Gyárfás conjecture.

9) V2 In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, 3c ≥ 2n + 4, where c is the number of vertices of degree three.

kernel-checked, filed Sun Sep 06 2026 17:26:46 GMT+0000 (Coordinated Universal Time) by @davidtsong

Equality in the +3 bound would force odd total degree.

Scope. For every n and simple graph G on Fin n satisfying IsMinCex G as defined here (nonempty, minimum degree at least three, no power-of-two cycle, lexicographically minimal in order then size), 2*n+4 ≤ 3*#{v : degree v = 3}. Hypothetical counterexamples only; no existence asserted and vacuous if the root conjecture is true.

8) V2 For every fixed end margin, a serial arithmetic spectrum with thirteen consecutive residue classes modulo 17 can span a power of two yet contain no power of two, even though its residue classes meet the doubling orbit.

kernel-checked, filed Sun Sep 06 2026 00:33:10 GMT+0000 (Coordinated Universal Time) by @declangessel

The increment count and both margins can be arbitrarily large.

Scope. For every natural end-margin bound B, spectra S_d={17(12d+t)+r: t≤8d, r≤12} with d≥1 and doubling modulus 17.

7) V2 In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, 3|V3| ≥ 2n + 3, because the contraction graph on the high-degree vertices must be 2-degenerate.

jig-cited, filed Fri Sep 04 2026 23:02:58 GMT+0000 (Coordinated Universal Time) by @am00lya, @davidtsong

Scope. Hypothetical minimal counterexamples only: graphs G on Fin n with IsMinCex G as defined in the statement; conclusion 2n + 3 ≤ 3|{v : deg v = 3}|, sharpening the strict bound 2n + 1 ≤ 3|V3| (?s=6) by the empty-3-core property of the contraction graph H on V4; vacuous if the conjecture is true.

6) V2 In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, strictly more than two thirds of the vertices have degree exactly 3.

prior art, filed Fri Sep 04 2026 23:02:50 GMT+0000 (Coordinated Universal Time) by @am00lya, @davidtsong

Scope. Hypothetical minimal counterexamples only: graphs G on Fin n with IsMinCex G as defined in the statement (0 < n, all degrees ≥ 3, no cycle of length 2^k with k ≥ 2, lexicographically minimal in (order, number of edges) over all Fin m); conclusion 2n < 3|{v : deg v = 3}|, which strengthens Bisch's 2n ≤ 3|V3| and Carr's 4/7; vacuous if the conjecture is true.

5) V2 In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, every vertex has a neighbour of degree exactly 3.

prior art, filed Fri Sep 04 2026 22:36:34 GMT+0000 (Coordinated Universal Time) by @am00lya, @davidtsong

Scope. Hypothetical minimal counterexamples only: graphs G on Fin n with IsMinCex G as defined in the statement (0 < n, all degrees ≥ 3, no cycle of length 2^k with k ≥ 2, lexicographically minimal in (order, number of edges) among all such graphs on any Fin m); conclusion: every vertex is adjacent to a cubic vertex; vacuous if the conjecture is true.

4) V2 In a counterexample to the Erdős–Gyárfás conjecture of minimum order and then minimum size, no two vertices of degree at least 4 are adjacent.

prior art, filed Fri Sep 04 2026 22:36:32 GMT+0000 (Coordinated Universal Time) by @am00lya, @coleski

Scope. Hypothetical minimal counterexamples only: graphs G on Fin n with IsMinCex G as defined in the statement (0 < n, all degrees ≥ 3, no cycle of length 2^k with k ≥ 2, and lexicographically minimal in (order, number of edges) among all such graphs on any Fin m); conclusion: vertices of degree ≥ 4 form an independent set; vacuous if the conjecture is true.

3) V2 Every simple graph on at most seven vertices in which every vertex has degree at least 3 contains a 4-cycle, hence a cycle of length 2^2.

kernel-checked, filed Fri Sep 04 2026 22:36:29 GMT+0000 (Coordinated Universal Time) by @am00lya

Scope. Simple graphs on Fin n with 1 ≤ n ≤ 7 and every vertex of degree at least 3 (any DecidableRel instance); conclusion: an IsCycle closed walk of length exactly 4, which is the root conclusion with k = 2; says nothing for n ≥ 8 (every graph with δ ≥ 3 on n ≤ 9 vertices still has a 4-cycle by ex(n, C4), but that is not formalised here; from n = 10 the Petersen graph has no 4-cycle).

2) V2 Every simple graph on four vertices in which every vertex has degree at least 3 contains a cycle of length 4 = 2^2; this is the n = 4 instance of the root statement.

kernel-checked, filed Fri Sep 04 2026 22:04:01 GMT+0000 (Coordinated Universal Time) by @am00lya

Scope. The n = 4 instance of the root: simple graphs on Fin 4 (any DecidableRel instance) in which every vertex has degree at least 3, which forces the complete graph K4; conclusion exactly as in the root (an IsCycle closed walk of length 2^k, k ≥ 2); says nothing about n ≠ 4.

1) V2 Every finite simple graph in which every vertex has degree at least 3 contains a cycle whose length is 2^k for some k ≥ 2 (the Erdős–Gyárfás conjecture, Erdős problem #64).

open, filed Fri Sep 04 2026 22:03:07 GMT+0000 (Coordinated Universal Time) by @am00lya

Citation update only: the Markström 2004 paper listed as unopened is online at the author page and was read; it confirms the 24-vertex and below-29 cubic search records and Royle's search below 16 vertices. No change to formal, scope or effect.

Scope. All finite simple graphs on n ≥ 1 vertices, modelled as SimpleGraph (Fin n) with an arbitrary DecidableRel instance, in which every vertex has degree at least 3 (∀ v, 3 ≤ G.degree v, equivalently 3 ≤ G.minDegree); conclusion: some closed walk c with c.IsCycle (a simple cycle in Mathlib's sense, so length ≥ 3) and c.length = 2^k for some k ≥ 2, i.e. a cycle of length 4, 8, 16, …; no assumption of regularity, connectivity, planarity, bipartiteness, bounded order or bounded maximum degree; infinite graphs excluded (the infinite cubic tree is a counterexample there); the empty graph excluded by 0 < n, as required (without it the statement is false at n = 0).

E64:Erdős Problem #64 “Does every finite graph with minimum degree at least 3 contain a cycle whose length is a power of two?”

E64: “Does every finite graph with minimum degree at least 3 contain a cycle whose length is a power of two?”