we-solve (beta)

Math-1880 · mathematics · Combinatorics

Goddyn's conjecture on thin spanning trees

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Let $G=(V,E)$ be a finite loopless undirected multigraph. For $X\subseteq V$, let $\delta_G(X)$ be the set of edges with exactly one endpoint in $X$, counting parallel copies separately. The graph is $k$-edge-connected if $|\delta_G(X)|\ge k$ for every nonempty proper subset $X$.

A spanning tree $T\subseteq G$ is $\varepsilon$-thin when \[ |\delta_T(X)|\le\varepsilon|\delta_G(X)| \quad(X\subseteq V). \] Goddyn's conjecture asks whether there exists a function $f:(0,1)\to\mathbb Z_{>0}$ such that, for each $\varepsilon\in(0,1)$, every $f(\varepsilon)$-edge-connected graph contains an $\varepsilon$-thin spanning tree.

The connectivity threshold depends only on the desired thinness and must be independent of the number of vertices, maximum degree, embedding genus, and all other graph parameters. The same tree must satisfy the inequality for all cuts simultaneously; choosing a different tree for each cut is insufficient. This is a cut-count condition and does not assume or demand a stronger spectral matrix inequality. The conjecture requests existence of some threshold function, without prescribing its rate of growth. A particular construction with a threshold that also depends on $|V|$ does not establish the stated uniform conclusion.

Short English statement

Does sufficiently high edge connectivity force a spanning tree using only a prescribed small fraction of the edges of every cut?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-1880-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-1880

Algorithmic strong thin trees: The uniform C/k cut ratio allows f(epsilon)=ceil(C/epsilon), proving Goddyn’s existential connectivity-threshold assertion with an explicit linear dependence; no simplicity hypothesis is needed.

Existence of strong thin trees: The uniform C/k cut ratio allows f(epsilon)=ceil(C/epsilon), proving Goddyn’s existential connectivity-threshold assertion with an explicit linear dependence; no simplicity hypothesis is needed.

The claimed result implies the stated question and also supplies the additional strength described above.

Goddyn's conjecture on thin spanning trees

OpenAI's claim

Algorithmic strong thin trees: The algorithmic manuscript claims a deterministic procedure polynomial in the binary input length that returns a $C/k$-thin spanning tree in a finite $k$-edge-connected loopless multigraph; binary-encoded parallel multiplicities and the one-vertex case are included.

Existence of strong thin trees: The existence paper claims one universal $C$ such that a $k$-edge-connected loopless finite multigraph has a spanning tree using at most a $C/k$ fraction of each cut; this assertion is simultaneous over all cuts of the graph.

Mathematical statement of the claimed result

Mathematical claim 1.
Given a finite $k$-edge-connected undirected multigraph $G$ and integer $k\ge1$, a deterministic algorithm is claimed to return a spanning tree $T$ using a number of bit operations polynomially bounded by the full input encoding length such that \[|\delta_T(S)|\le(C/k)|\delta_G(S)|\quad(\varnothing\ne S\subsetneq V(G)),\] where $C$ is absolute and $\delta_G(S)$ is the edge cut. The bound applies to explicitly listed edges and binary-encoded multiplicities; for one vertex the output is the empty tree.
Mathematical claim 2.
There is an absolute $C>0$ such that every finite loopless $k$-edge-connected undirected multigraph with at least two vertices, for every integer $k\ge1$, has a spanning tree $T$ with \[|\delta_T(S)|\le\frac Ck|\delta_G(S)|\quad\text{for every nonempty proper }S\subset V(G).\] The tree is chosen once and must satisfy all cuts simultaneously.

Outline of the argument

Algorithmic strong thin trees: An effective metric-cone hierarchy constructs a rational shortcut form and many low-resistance candidate edges. A second frame preserves the ranks needed for spanning-tree packing, and rational padding supplies signing certificates without irrational whitening. Iterated simultaneous sparsification controls every cut and packing inequality, with a separate reduction handling binary multiplicities.

Existence of strong thin trees: A shortcut quadratic form supplies a cut-sensitive representation of suitable edges, while an isotropic representation records the partition inequalities for tree packing. Rank-one signing selects the same edge subset in both representations. Iterated halving has a bounded product of relative losses, so the remaining tree retains uniform cut control.

Formal verification

Family 174 describes Lean coverage for thin-tree existence and the companion deterministic construction with binary multiplicities.

Algorithmic strong thin trees: The manuscript links AlgorithmicThinTrees.lean, StrongThinTree.lean (declaration OAI.StrongThinTree.strongThinTree).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

Existence of strong thin trees: The manuscript links AlgorithmicThinTrees.lean, StrongThinTree.lean (declaration OAI.StrongThinTree.strongThinTree).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →