34:Walks in N^k

[Harvey Friedman]

This is the 34th in a series of self contained postings to fom covering a
wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM
29:Large Cardinals/where are we? I  2/22/99  6:11AM
30:Large Cardinals/where are we? II  2/23/99  6:15AM
31:First Free Sets/Large Cardinals  2/27/99  1:43AM
32:Greedy Constructions/Large Cardinals  3/2/99  11:21PM
33:A Variant  3/4/99  1:52PM

A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/
Also, my series of self contained postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html

FAVORITE POSTINGS: 21, 25, 27, 31, 32, 33, 34.

The posting 25:Long Walks touches on the absolutely standard notion of
walk, but the result is not as natural as we would like. Here we give a
lower bound result that is more natural for standard walks.

We  consider walks in N^k, where N is the set of all nonnegative integers.
These are finite or infinite sequences from N^k such that any two
consecutive terms are at Euclidean distance 1. A self avoiding walk is a
walk where no term repeats.

We write |x| for the Euclidean norm of x in R^k. We also write x <= y if
and only if for all 1 <= i <= k, x_i <= y_i. For x,y in N^k, x <= y says
that x points outward to y.

THEOREM 1. Fix x in N^k. Let W be a sufficiently long finite self avoiding
walk in N^k starting at x. There exists terms y,z in W such that
i) |y| <= |z|/2;
ii) y <= z.

Now let f(x) be the least n such that the conclusion of Theorem 1 holds for
all walks in N^k of length n. Already f(2,2,2), in three dimensions, is
interesting:

THEOREM 2. f(2,2,2) >= 2^192,938,011.

As we go up from (2,2,2), we at least exponentiate. Thus:

THEOREM 3. f(3,3,3) >= 2^2^192,938,011. For n >= 2, f(n,n,n) is at least a
stack of n-1 2's with 192,938,011 on top.

Thus in 3 dimensions, f behaves at least like iterated exponentiation.

In 4 dimensions, the numbers are much bigger. For example, f(1,1,1,1) is at
least a stack of 2's of height 2^192,938,011. In 4 dimensions, f behaves at
least like the next level of the Ackerman hierarchy beyond iterated
exponentiation.

As the dimensions go up, f behaves at least like successive levels of the
Ackerman hierarchy.

Upper bounds can be given that match the lower bounds in terms of levels of
the Ackerman hierarchy. However, one wants a better match than that, and
that is more difficult to obtain.