What the enumerator's tapes rest in between iterations

⚠️ Unreviewed by Bolton

The counting loop's state names three registers; every other tape has to be back at a known resting value when an iteration ends, or the next one cannot be entered. For the witness enumerator that bank is not the same at every index: the witness tape advances with the counter, which is why the loop rule this machine uses is the indexed one.

Everything else rests where it started — the input copy rewound, the horizon in place, the wipe's height register loaded, and every scratch tape blank.

Main results

• PolyExists.strTape — a rewound tape holding a bitstring, and that it is parked
• PolyExists.enumRest — the resting bank at a given count, and its values at the named indices
• PolyExists.enumRest_parked, PolyExists.enumRest_head — what the loop rule asks of it

def Complexity.PolyExists.strTape (l : List Bool) : Tape

A rewound tape holding a bitstring.

Equations

• Complexity.PolyExists.strTape l = (Complexity.Tape.init (List.map Complexity.Γ.ofBool l)).move Complexity.Dir3.right

@[simp]

theorem Complexity.PolyExists.strTape_head (l : List Bool) : (strTape l).head = 1

theorem Complexity.PolyExists.strTape_hasBinaryString (l : List Bool) : (strTape l).HasBinaryString l

theorem Complexity.PolyExists.strTape_parked (l : List Bool) : TM.Parked (strTape l)

A tape holding a bitstring is parked: its head is off the left marker and no cell past the marker holds one.

theorem Complexity.PolyExists.strTape_startInvariant (l : List Bool) : (strTape l).StartInvariant

theorem Complexity.PolyExists.regTape_parked (v : ℕ) : TM.Parked (TM.regTape v)

theorem Complexity.PolyExists.regTape_startInvariant (v : ℕ) : (TM.regTape v).StartInvariant

def Complexity.PolyExists.enumRest (k : ℕ) (x : List Bool) (N H v : ℕ) : Fin (enumTapes k) → Tape

The resting bank at a given count. The input copy and the horizon are where the prologue put them, the wipe's height register is loaded, the witness is the one the count denotes, and every scratch tape is blank.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.PolyExists.enumRest_x (k : ℕ) (x : List Bool) (N H v : ℕ) : enumRest k x N H v (xIdx k) = strTape x

@[simp]

theorem Complexity.PolyExists.enumRest_w (k : ℕ) (x : List Bool) (N H v : ℕ) : enumRest k x N H v (wIdx k) = strTape (dropTop v)

@[simp]

theorem Complexity.PolyExists.enumRest_n (k : ℕ) (x : List Bool) (N H v : ℕ) : enumRest k x N H v (nIdx k) = natTape N

theorem Complexity.PolyExists.enumRest_parked (k : ℕ) (x : List Bool) (N H v : ℕ) (i : Fin (enumTapes k)) : TM.Parked (enumRest k x N H v i)

The bank is parked at every index, which is what the loop rule asks of the tapes its state does not name.

theorem Complexity.PolyExists.enumRest_head (k : ℕ) (x : List Bool) (N H v : ℕ) (i : Fin (enumTapes k)) : (enumRest k x N H v i).head ≤ 1

Every resting tape is at cell one, which is what makes the loop's window one iteration wide.