The witness enumerator's tape layout

⚠️ Unreviewed by Bolton

Two placements fix where every tape sits, and they have to agree. The pair emitter is TM.pairInputWorkTM on one work tape — the copy of the real input — wrapped so that it reads the witness as a virtual input and writes onto a work tape; those wrappers append their tapes, so the witness lands at index one and the emitted pair at index two. The matrix machine is TM.applyTM placed by TM.placeWorkTM 3 _, which puts its own k scratch tapes at 3 … k + 2, the input it reads at k + 3, and the verdict it writes at k + 4.

The emitted pair and the input the matrix machine reads are therefore different tapes — the two placements cannot be made to share one — and TM.copyToVirtualInputTM moves the pair from the first to the second, which is exactly the shape TM.retargetInputStartedCfg demands anyway.

Seven registers follow: the counter, the horizon it is compared against, scratch for that comparison, the two tallies the counting loop's state carries, a permanently blank tape to blank slots from, and the unary register that drives the wipe.

Main results

• PolyExists.enumTapes — the tape count, and the named indices into it
• PolyExists.enumIdx_distinct — the indices are pairwise distinct
• PolyExists.matrixTapes — the matrix machine's own scratch tapes
• PolyExists.scratchTargets, PolyExists.scratchTargets_nodup — the tapes the body blanks on its way out

@[reducible, inline]

abbrev Complexity.PolyExists.enumTapes (k : ℕ) : ℕ

The enumerator's tape count: three for the emitter, the matrix machine's k + 2, and six registers.

Equations

• Complexity.PolyExists.enumTapes k = 3 + (k + 2) + 7

def Complexity.PolyExists.xIdx (k : ℕ) : Fin (enumTapes k)

The copy of the real input, which the emitter reads as the pair's first component.

Equations

• Complexity.PolyExists.xIdx k = ⟨0, ⋯⟩

def Complexity.PolyExists.wIdx (k : ℕ) : Fin (enumTapes k)

The witness, which the emitter reads as the pair's second component.

Equations

• Complexity.PolyExists.wIdx k = ⟨1, ⋯⟩

def Complexity.PolyExists.y1Idx (k : ℕ) : Fin (enumTapes k)

The tape the emitter writes the pair onto.

Equations

• Complexity.PolyExists.y1Idx k = ⟨2, ⋯⟩

def Complexity.PolyExists.yIdx (k : ℕ) : Fin (enumTapes k)

The tape the matrix machine reads its input from.

Equations

• Complexity.PolyExists.yIdx k = ⟨3 + k, ⋯⟩

def Complexity.PolyExists.vIdx (k : ℕ) : Fin (enumTapes k)

The tape the matrix machine's verdict is redirected to.

Equations

• Complexity.PolyExists.vIdx k = ⟨3 + k + 1, ⋯⟩

def Complexity.PolyExists.cIdx (k : ℕ) : Fin (enumTapes k)

The counter, whose value denotes the witness.

Equations

• Complexity.PolyExists.cIdx k = ⟨3 + k + 2, ⋯⟩

def Complexity.PolyExists.nIdx (k : ℕ) : Fin (enumTapes k)

The horizon the counter is compared against.

Equations

• Complexity.PolyExists.nIdx k = ⟨3 + k + 3, ⋯⟩

def Complexity.PolyExists.resIdx (k : ℕ) : Fin (enumTapes k)

Scratch space for that comparison.

Equations

• Complexity.PolyExists.resIdx k = ⟨3 + k + 4, ⋯⟩

def Complexity.PolyExists.aIdx (k : ℕ) : Fin (enumTapes k)

The latched answer: 1 once some witness has been accepted.

Equations

• Complexity.PolyExists.aIdx k = ⟨3 + k + 5, ⋯⟩

def Complexity.PolyExists.zIdx (k : ℕ) : Fin (enumTapes k)

A permanently blank tape, read whenever a slot must be blanked.

Equations

• Complexity.PolyExists.zIdx k = ⟨3 + k + 6, ⋯⟩

def Complexity.PolyExists.regIdx (k : ℕ) : Fin (enumTapes k)

The unary register that drives the wipe.

Equations

• Complexity.PolyExists.regIdx k = ⟨3 + k + 7, ⋯⟩

def Complexity.PolyExists.rIdx (k : ℕ) : Fin (enumTapes k)

The count of witnesses that failed, which the counting loop's state carries alongside the count of those that succeeded.

Equations

• Complexity.PolyExists.rIdx k = ⟨3 + k + 8, ⋯⟩

def Complexity.PolyExists.matrixTapes (k : ℕ) : List (Fin (enumTapes k))

The matrix machine's own scratch tapes: the block TM.placeWorkTM 3 _ puts them in.

Equations

• Complexity.PolyExists.matrixTapes k = List.filter (fun (j : Fin (Complexity.PolyExists.enumTapes k)) => decide (3 ≤ ↑j ∧ ↑j < 3 + k)) (List.finRange (Complexity.PolyExists.enumTapes k))

@[simp]

theorem Complexity.PolyExists.mem_matrixTapes_iff (k : ℕ) (j : Fin (enumTapes k)) : j ∈ matrixTapes k ↔ 3 ≤ ↑j ∧ ↑j < 3 + k

theorem Complexity.PolyExists.matrixTapes_nodup (k : ℕ) : (matrixTapes k).Nodup

def Complexity.PolyExists.scratchTargets (k : ℕ) : List (Fin (enumTapes k))

The tapes one pass of the body leaves dirty, and must blank before the next: the emitted pair, the matrix machine's scratch and its two placed tapes, and the verdict slot.

Equations

• Complexity.PolyExists.scratchTargets k = Complexity.PolyExists.y1Idx k :: Complexity.PolyExists.matrixTapes k ++ [Complexity.PolyExists.yIdx k, Complexity.PolyExists.vIdx k]

theorem Complexity.PolyExists.scratchTargets_nodup (k : ℕ) : (scratchTargets k).Nodup

The scratch block has no repeats, which the wipe requires of its targets.

theorem Complexity.PolyExists.scratchTargets_val (k : ℕ) (j : Fin (enumTapes k)) (h : j ∈ scratchTargets k) : 2 ≤ ↑j ∧ ↑j < 3 + k + 2

Every tape the body wipes lies in the block between the emitter's target and the verdict tape — which is exactly the part of the layout that rests blank.

theorem Complexity.PolyExists.enumIdx_distinct (k : ℕ) : xIdx k ≠ wIdx k ∧ xIdx k ≠ y1Idx k ∧ xIdx k ≠ yIdx k ∧ xIdx k ≠ vIdx k ∧ xIdx k ≠ cIdx k ∧ xIdx k ≠ nIdx k ∧ xIdx k ≠ resIdx k ∧ xIdx k ≠ aIdx k ∧ xIdx k ≠ zIdx k ∧ xIdx k ≠ regIdx k ∧ wIdx k ≠ y1Idx k ∧ wIdx k ≠ yIdx k ∧ wIdx k ≠ vIdx k ∧ wIdx k ≠ cIdx k ∧ wIdx k ≠ nIdx k ∧ wIdx k ≠ resIdx k ∧ wIdx k ≠ aIdx k ∧ wIdx k ≠ zIdx k ∧ wIdx k ≠ regIdx k ∧ y1Idx k ≠ yIdx k ∧ y1Idx k ≠ vIdx k ∧ y1Idx k ≠ cIdx k ∧ y1Idx k ≠ nIdx k ∧ y1Idx k ≠ resIdx k ∧ y1Idx k ≠ aIdx k ∧ y1Idx k ≠ zIdx k ∧ y1Idx k ≠ regIdx k ∧ yIdx k ≠ vIdx k ∧ yIdx k ≠ cIdx k ∧ yIdx k ≠ nIdx k ∧ yIdx k ≠ resIdx k ∧ yIdx k ≠ aIdx k ∧ yIdx k ≠ zIdx k ∧ yIdx k ≠ regIdx k ∧ vIdx k ≠ cIdx k ∧ vIdx k ≠ nIdx k ∧ vIdx k ≠ resIdx k ∧ vIdx k ≠ aIdx k ∧ vIdx k ≠ zIdx k ∧ vIdx k ≠ regIdx k ∧ cIdx k ≠ nIdx k ∧ cIdx k ≠ resIdx k ∧ cIdx k ≠ aIdx k ∧ cIdx k ≠ zIdx k ∧ cIdx k ≠ regIdx k ∧ nIdx k ≠ resIdx k ∧ nIdx k ≠ aIdx k ∧ nIdx k ≠ zIdx k ∧ nIdx k ≠ regIdx k ∧ resIdx k ≠ aIdx k ∧ resIdx k ≠ zIdx k ∧ ⋯

The named indices are pairwise distinct. Every frame lemma the assembly uses asks for some of these disequalities; this states all of them at once.

theorem Complexity.PolyExists.not_mem_scratchTargets (k : ℕ) : xIdx k ∉ scratchTargets k ∧ wIdx k ∉ scratchTargets k ∧ cIdx k ∉ scratchTargets k ∧ nIdx k ∉ scratchTargets k ∧ resIdx k ∉ scratchTargets k ∧ aIdx k ∉ scratchTargets k ∧ zIdx k ∉ scratchTargets k ∧ regIdx k ∉ scratchTargets k ∧ rIdx k ∉ scratchTargets k

The registers and the input copy are outside the scratch block, so the wipe leaves them alone.