The graph is a Mathlib $SimpleGraph$ on $Fin V$, and both its encoding and the number of vertices come from the archive: $EncodesGraph g V G$ of $lax-271696$ says that the word $g$ is a compressed sparse row encoding of $G$. The word of an instance is $g ++ [n]$. The block $g$ is self-delimiting — its header fixes its length — so the split of the word into the block and the appended entry is determined by the word, as in the parameterized instances of the same submission, and the graph block sits at the same offsets as in every statement built on that encoding.

The word is required to encode a graph that genuinely is split at $n$: an edge inside a side is not an input the theorems below speak about. The adjacency lists of the right vertices are present in the word, as the encoding lists every edge from both ends; the algorithm reads only the left rows, and pays for the length of the whole word only in the linear factor of its bound.

$wordGraph x$ is the graph a word denotes, read off its block: two vertices are adjacent when either lists the other. On an encoding of $G$ it is $G$. It is what makes the output of the machine a function of the word, as $ComputesInTime$ requires, and $leftCount x$ is the last entry of the word.