I think you are correct that the Mathias forcing is a red herring, the same lemma should apply to any ground model not just a Mathias extension. (The lemma was placed in the middle of a proof in the text, so I can see why they might not have been concerned with the extra generality). It also looks like the proof is, if not incorrect, at least a bit misleading. The problem is that the $\dot{a_n}$ are sequences of reals which may not belong to the ground model at all, so there's no hope of using the Laver property to get slaloms literally covering them (or finite sequences of them). To correct this, we can replace the $\dot{a_n}$ with dyadic rationals that very closely approximate them. Let me go into the details. Instead of getting $n^2$ exactly I'll get a different upperbound, but getting basically any ground model bound you like is possible by slightly modifying the proof, which I'll leave to you.

Proposition. If $\mathbb{P}$ is a forcing with the Laver property, $f\in V\cap\omega^\omega$ and $\langle \dot{a_n} :n<\omega\rangle$ is a sequence of names for positive real numbers satisfying $\Vdash\sum_{j=1}^{f(n)}\dot{a_j}\leq n$ then there is some ground model sequence $\langle b_n:n<\omega\rangle$ of real numbers with $\Vdash\dot{a_n}\leq\dot{b_n}$ and $\sum_{j=1}^{f(n)}b_j\leq n^2(n+1)$.

Proof: Working in $V^\mathbb{P}$, for each $n<\omega$ and each $i < f(n)$ let $c^n_i$ be the rational of the form $\frac{j+1}{f(n)}$ where $\frac{j}{f(n)} < a_i < \frac{j+1}{f(n)}$. Since $\sum_{j=1}^{f(n)}a_j\leq n$ we easily see $\sum_{j=1}^{f(n)}c^n_j\leq n+1$.

By considering the function which maps $n$ to the sequence $\langle c^n_i:i < f(n)\rangle$ as a function from $\omega$ into $\omega$, we may apply the Laver property to get a slalom $C$ covering it. That is, $C$ is some function in the ground model with domain $\omega$, with $|C(n)|\leq n$ and so that

(1) $C(n)$ contains the sequence $\langle c^n_i:i < f(n)\rangle$.

(2) all the elements of $C(n)$ are sequences of dyadic rationals of length $f(n)$ which sum to at most $n+1$.

(We can assume we have (2) because we may, within the ground model, remove all other types of objects from $C(n)$ and maintain the relevant properties of $C$). Modify $C$ to $C'$ in the obvious way so that (1) and (2) hold and also $C'$ is increasing: $i < j$ implies $C'(i)\subseteq C'(j)$. Now $C'(n)$ might contain sequences shorter than $f(n)$, but just pad those with $0$s. We have for each $n$ that $|C'(n)|\leq n^2$.

Now for $i\in [f(n),f(n+1)]$ define $b_i$ to be equal to the max of $s(i)$ over all possible $s$ in $C'(n+1)$. Then $b_i$ must be larger than $c^{n+1}_i$ which is larger than $a_i$. And, for each fixed $n$, the sum over each $s$ in $C'(n)$ is at most $n+1$, so the sum over ALL such $s$ is at most $n^2$ times $n+1$, and thus $\sum_{j=1}^{f(n)}b_j\leq n^2(n+1)$ since each $b_j$ appears as $s(j)$ for some $s\in C'(n)$. (For small $j$ we know this because we increased to $C'$).