Sorry. I clearly didn't read your question sufficiently carefully.

Yes. I had just come back to say that I was assuming that $k$ is countable (in fact in my mind I was thinking of $k$ as finite because that is the case that I think about most) and as you say I should have said 'can it possibly be non-zero'. Of course the countability of $k$ is not necessary for such an example it just makes it easy to see that a suitable $f$ exists.

Not true and deeply frustrating. Take a map from $k[[x,y,z]]$ to $k[[u,v]]$ that sends $x$ to $u$, $y$ to $uv$ and $z$ to $uf(v)$ for some $f\in k[[v]]$ and think about what the kernel is. It isn't hard to see that only for countably many choices of $f$ can it possibly be zero.

Yes. It does mean that.

Great! Permit me to rephrase this in algebra rather than geometry for the sake of algebraists. Pick $f$ in the Jacobson radical but non-zero and let $P$ be an ideal that is maximal amongst ideals disjoint from the set of powers of $f$. $P$ is prime but cannot be maximal so is (by condition 2) the intersection of the prime ideals that strictly contain it. But by definition of $P$ all these strictly bigger primes conatin $f$ thus $P$ contains $f$ a contradiction. Nice.

I have now realised that all I really wanted to know for my application has been established. Since I cannot really reasonably accept Kevin Buzzard's answer I am going to vote to close and see what happens.

The Grothendieck group of what?

Ah. I see. That's very helpful indeed. Thank you. Is it possible to say anything about which tuples of ords at the generic points of the special fibre actually arise from units in $A^\times$?

I am still trying to understand it but think it might be. Is the claim that if $A^\circ$ is a normal domain without idempotents top. f.g. over the valuation ring of $K$ with geometrically reduced special fibre (but with no other restrictions on $\overline{A}=A^\circ/A^{\circ\circ}$) then units in $A$ are all $K^\times$-multiples of elements that whose images are units in $\overline{A}$ and that if two units have the same unit image in $\overline{A}$ then they differ by a unit in $A^\circ$? How do the units of $\mathbb{Q_p}\langle x,p/x\rangle$ fit into this picture? Is that not normal?

Actually the second sentence of my comment above is not strictly accurate. It is standard to say a ring is prime if the zero ideal is prime but this is not equivalent to the ring being a domain in this case.

By prime ring I do mean domain. This is standard in non-commutative algebra. I suppose less so in commutative algebra. I am most interested in the case $K$ is a finite extension of $\mathbb{Q}_p$ however more general settings are also of interest.

The proof that a subspace of a vector space has dimension no bigger than that of the original space (ie all maximal linearly independent sets have the same cardinality) can be done by transfinite induction. I also don't think that there can be an easier Zorn-type proof of this result.