The states of the read machine for undirected connectivity are small

On the encoding of an instance on n vertices, every state of Cslib.USTCON.Reader.machine along its run keeps its numbers below n, the depth D and the walk length T of Reingold's graph, and B ^ T for the counters, where B = 257 ^ 8, its slot below n, and at most D + 1 labels and frames (Cslib.USTCON.Reader.inv_run). As D and T are O(log n), the encoded states have O(log n) bits, which is logarithmic in the length of the encoding (Cslib.USTCON.Reader.length_encState_run_le).

Main definitions

• Cslib.USTCON.Reader.Bounds, Cslib.USTCON.Reader.Inv: the bounds on the states, and the invariant of the run that keeps them.

Main results

• Cslib.USTCON.Reader.inv_run: the states along the run satisfy the invariant.
• Cslib.USTCON.Reader.length_encState_run_le: they have logarithmically many bits.

@[reducible, inline]

abbrev Cslib.USTCON.Reader.depthOf (I : Complexity.USTCONInstance) : ℕ

The depth of Reingold's graph for the instance.

@[reducible, inline]

abbrev Cslib.USTCON.Reader.lenOf (I : Complexity.USTCONInstance) : ℕ

The walk length for the instance.

structure Cslib.USTCON.Reader.Bounds (I : Complexity.USTCONInstance) (q : State) : Prop

The bounds on the states: numbers at most n, the depth, the walk length and B ^ T, the slot below n, and at most D + 1 labels and frames.

• cnt : q.cnt ≤ I.n
• n : q.n ≤ I.n
• s : q.s ≤ I.n
• t : q.t ≤ I.n
• depth : q.depth ≤ depthOf I
• len : q.len ≤ lenOf I
• c : q.c ≤ numLabels ^ lenOf I
• w : q.w ≤ numLabels ^ lenOf I
• j : q.j ≤ lenOf I
• v₁ : q.ev.vertex.1 < I.n
• v₂ : q.ev.vertex.2 < I.n
• lower : q.ev.lower.length ≤ depthOf I + 1
• frames : q.ev.frames.length ≤ depthOf I + 1

def Cslib.USTCON.Reader.WalkParams (I : Complexity.USTCONInstance) (q : State) : Prop

The parameters of the walks.

def Cslib.USTCON.Reader.Phase (I : Complexity.USTCONInstance) (q : State) : Prop

The facts of each phase that keep the bounds.

def Cslib.USTCON.Reader.Inv (I : Complexity.USTCONInstance) (q : State) : Prop

The invariant of the run: the bounds, and the facts of the phase.

The invariant is kept

theorem Cslib.USTCON.Reader.inv_run {I : Complexity.USTCONInstance} (k : ℕ) : Inv I (machine.run I.encode k).state

The states along the run satisfy the invariant.

The size of the states

def Cslib.USTCON.Reader.stateConst : ℕ

The constant of the size of the states.

theorem Cslib.USTCON.Reader.length_encState_run_le {I : Complexity.USTCONInstance} (k : ℕ) : (encState (machine.run I.encode k).state).length ≤ stateConst * (I.encode.length.log2 + 2)

The states along the run have logarithmically many bits.