Questions on Sipser's NP implying verifiability?

I've revisited trying to understand the proof to why NTM exists iff there is a verifier. I think I'm finally understanding the proof but I want to make sure and thus have some questions as follow up along with to check if I'm understanding.

1. For the forward implication (there exists a verifier $V$ and we want to show this implies the existence of an NTM $N$), we can, according to Sipser, "Nondeterministically select string $c$ of length at most $n^k$. Then we run $V$ on input $(w,c)$ and accept if $V$ accepts, otherwise reject." I'm wondering if $V$ would be run as part of the algorithm on each branch of $N$. In other words, for any node in the computation tree of $N$, the verifier will be run on the that current string, and the branch will produce a YES answer only if the verifier accepts that string. Am I understanding this correctly? So it would run concurrently, and since the verifier runs in $O(n^k)$ and the NTM runs in $O(n^q)$, then this still runs in polynomial time if the verifier is run at every step in the computation.

2. For the backward implication, we assume $A$ is decided by a polynomial time NTM and construct a polynomial time verifier $V$. When we say that $A$ "is decided by" $N$, does this mean that $N$ is correctly able to determine if any given branch of computation results in accept or reject? This feels a bit cyclic to me, since we are trying to construct the verifier $V$ given $N$. I don't see how $N$ could decide $A$ without $N$ having a verifier constructed already. In other words, without a verifier, how would the NTM know if it should accept/reject on any of its given branches?

2. We have a nondeterministic Turing machine $N$ and the guesses it makes lead it down some path of the tree of possible computations. If that path ends in an accepting state, the machine is defined to accept its input; if no path ends in an accepting state, it is defined to reject. There's no circularity: that's just the definition of what it means for a nondeterministic machine to accept or reject.
From this machine, we build a verifier. The input to the verifier is a description of a computation path, and the verifier checks that each action taken on that path is a thing that $N$ could do in that state, and that the path ends in an accepting state. If those conditions are met, the verifier has verified that $N$ really would accept the given input.
• Not necessarily. Consider, for example, 3-SAT. Suppose we have a formula $\phi$ and I tell you that, according to my nondeterministic Turing machine, $S$ is a satisfying assignment to that formula. You can verify that claim just by checking that it makes the formula true. You certainly don't need to know the details of my Turing machine or even believe that I really have a nondeterministic Turing machine in my office. There is a verifier based on the definition of the TM but there can be other verifiers, too. – David Richerby Apr 15 '18 at 11:23